diff --git a/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean b/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean index a8c71a4883..703aaa5fc9 100644 --- a/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean +++ b/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean @@ -83,7 +83,8 @@ lemma num_spec : (G.residual (x.take h.num)).ExistsWinning (p.residual (x.take h rw [← _root_.not_imp_self (a := _ ≤ _)] --change after update intro hn; apply Nat.find_le have h' := h.num_spec - rwa [List.take_of_length_le] at * <;> omega + simpa only [List.take_of_length_le (by omega : x.length ≤ h.num), + List.take_length] using h' --the choices of Exists.choose here just depend on x|n, not x lemma take_num {y} : (x ++ y).take h.num = x.take h.num := by simp lemma extend (y : List A) (h : WinningPrefix G p x) : WinningPrefix G p (x ++ y) := diff --git a/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean b/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean index cd7e4d1cab..7340d53252 100644 --- a/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean +++ b/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean @@ -66,8 +66,8 @@ lemma ψ_kills_gen : ψHom ((X 0) ^ 2 - (X 1) * (X 2)) = 0 := by ring lemma conjI_le_ker_ψ : conjI ≤ RingHom.ker ψHom.toRingHom := by - rw [show conjI = Ideal.span {(X (0 : Fin 3) : MvPowerSeries (Fin 3) ℂ) ^ 2 - - X 1 * X 2} from rfl, Ideal.span_le] + rw [show conjI = Ideal.span {((X (0 : Fin 3) : MvPowerSeries (Fin 3) ℂ) ^ 2 - + X 1 * X 2)} from rfl, Ideal.span_le] intro x hx simp only [Set.mem_singleton_iff] at hx subst hx diff --git a/LeanPool/BrauerGroupNew/BrauerOverR.lean b/LeanPool/BrauerGroupNew/BrauerOverR.lean index d795ef631c..d273329c1c 100644 --- a/LeanPool/BrauerGroupNew/BrauerOverR.lean +++ b/LeanPool/BrauerGroupNew/BrauerOverR.lean @@ -151,7 +151,7 @@ lemma BrauerOverR (A : CSA.{0, 0} ℝ) : rw [← e'.symm_apply_apply d, ← e'.symm_apply_apply d'] conv_lhs => rw [← _root_.map_mul e'.symm, mul_comm, map_mul] rw [this] - exact SetLike.lt_iff_le_and_exists.2 ⟨fun _ _ ↦ ⟨⟩, ⟨e'.symm Complex.I, ⟨⟨⟩, by + exact IsConcreteLE.lt_iff_le_and_exists.2 ⟨fun _ _ ↦ ⟨⟩, ⟨e'.symm Complex.I, ⟨⟨⟩, by by_contra! mem change ∃(_ : _), _ = _ at mem obtain ⟨r, eq⟩ := mem diff --git a/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean b/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean index f9af49dbbb..a2ae8b58fc 100644 --- a/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean +++ b/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean @@ -327,7 +327,7 @@ lemma of_mul_incl (σ : Gal(K, F)) (c : K) : of f σ * incl f c = incl f (σ c) simp only [incl_apply, val_mul, val_of_val, val_smul, val_one, Finsupp.smul_single, smul_eq_mul, mulLinearMap_single_single, mul_one, map_mul, map_inv₀, one_mul, map_one_snd_of_isMulCocycle₂ Fact.out σ, AlgEquiv.smul_units_def, Units.coe_map, - MonoidHom.coe_coe, ne_eq, EmbeddingLike.map_eq_zero_iff, Units.ne_zero, not_false_eq_true, + MonoidHom.coe_ofClass, ne_eq, EmbeddingLike.map_eq_zero_iff, Units.ne_zero, not_false_eq_true, inv_mul_cancel_right₀, smul_one_mul] lemma sum_of (x : CrossProductAlgebra f) : x.val.sum (fun σ c ↦ c • (of f σ).val) = x := by diff --git a/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean b/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean index 5758d004da..dd0f699a30 100644 --- a/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean +++ b/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean @@ -301,7 +301,7 @@ abbrev e01 (M : TensorModule R A C) : · exact AddHom.id _ · intro a m change a • m = (moduleAux R A C M (a ⊗ₜ[R] (1 : C))) m - simp + rw [moduleAux_apply, map_one, Module.End.one_apply] · exact id · exact congrFun rfl · exact congrFun rfl)) fun c ↦ by diff --git a/LeanPool/BrauerGroupNew/Subfield/Defs.lean b/LeanPool/BrauerGroupNew/Subfield/Defs.lean index 082db8715d..4920c0ef4d 100644 --- a/LeanPool/BrauerGroupNew/Subfield/Defs.lean +++ b/LeanPool/BrauerGroupNew/Subfield/Defs.lean @@ -43,7 +43,7 @@ instance : SetLike (SubField R A) A where coe L := L.1 coe_injective := SetLike.coe_injective.comp toSubalgebra_injective -instance : PartialOrder (SubField R A) := .ofSetLike (SubField R A) A +instance : PartialOrder (SubField R A) := .ofSetLike (SubField R A) lemma mem_carrier : a ∈ L.carrier ↔ a ∈ L := .rfl @[simp] lemma mem_toSubalgebra : a ∈ L.toSubalgebra ↔ a ∈ L := .rfl diff --git a/LeanPool/BrauerGroupNew/ToSecond.lean b/LeanPool/BrauerGroupNew/ToSecond.lean index 5a378816ac..2f23d0d335 100644 --- a/LeanPool/BrauerGroupNew/ToSecond.lean +++ b/LeanPool/BrauerGroupNew/ToSecond.lean @@ -254,7 +254,7 @@ lemma conjFactorCompCoeff_inv (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A A.ι ((conjFactorCompCoeff x y z)⁻¹) = z.1 * (y.1⁻¹ * x.1⁻¹) := by suffices eq : Units.map A.ι (conjFactorCompCoeffAsUnit x y z)⁻¹ = z.1 * (y.1⁻¹ * x.1⁻¹) by rw [Units.ext_iff] at eq - simp only [conjFactorCompCoeffAsUnit, Units.inv_mk, Units.coe_map, MonoidHom.coe_coe, + simp only [conjFactorCompCoeffAsUnit, Units.inv_mk, Units.coe_map, MonoidHom.coe_ofClass, AlgEquiv.mul_apply, Units.val_mul] at eq rw [← eq] congr 1 @@ -854,7 +854,7 @@ noncomputable def fromSnd : congr 1 specialize hc σ τ simp only [AlgEquiv.smul_units_def, Pi.div_apply, Units.ext_iff, Units.val_mul, - Units.val_div_eq_div_val, Units.coe_map, MonoidHom.coe_coe] at hc + Units.val_div_eq_div_val, Units.coe_map, MonoidHom.coe_ofClass] at hc simp only [_root_.mul_assoc] congr 1 rw [mul_comm (c σ).1, _root_.mul_assoc] diff --git a/LeanPool/BruhatTits/Graph/GroupAction.lean b/LeanPool/BruhatTits/Graph/GroupAction.lean index d7273b5061..f6fa2eb88a 100644 --- a/LeanPool/BruhatTits/Graph/GroupAction.lean +++ b/LeanPool/BruhatTits/Graph/GroupAction.lean @@ -268,8 +268,8 @@ lemma _root_.BruhatTits.Lattice.valuation_det_eq_one_of_mem_stabilizer obtain ⟨h, rfl⟩ := MulAction.exists_smul_eq (GL (Fin 2) K) (Lattice.standard R) L rw [stabilizer_smul_standard_eq_map_conj_subtype_range] at hg obtain ⟨k, ⟨k, rfl⟩, rfl⟩ := hg - simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conj_apply, map_mul, map_inv, - mul_inv_cancel_comm, Matrix.GeneralLinearGroup.val_det_apply, + simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply, map_mul, + map_inv, mul_inv_cancel_comm, Matrix.GeneralLinearGroup.val_det_apply, Matrix.GeneralLinearGroup.val_map_apply, Subring.coe_subtype, Subring.coe_det] rw [← valuation_eq_one_iff] exact Matrix.isUnits_det_units k diff --git a/LeanPool/BruhatTits/Lattice/Distance.lean b/LeanPool/BruhatTits/Lattice/Distance.lean index 37dcb539f0..18557c739c 100644 --- a/LeanPool/BruhatTits/Lattice/Distance.lean +++ b/LeanPool/BruhatTits/Lattice/Distance.lean @@ -426,15 +426,15 @@ lemma unit_smul_eq (u : Rˣ) (M : BruhatTits.Lattice R) : (Units.map R.subtype u · intro hx simp only [Lattice.smul_module] at hx obtain ⟨y, hy, rfl⟩ := hx - simp only [Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype, + simp only [Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype, DistribSMul.toLinearMap_apply] exact Submodule.smul_mem _ u.val hy · intro hx simp only [Lattice.smul_module] refine ⟨u⁻¹ • x, ?_, ?_⟩ · exact Submodule.smul_mem _ u.inv hx - · simp only [Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype, LinearMap.map_smul_of_tower, - DistribSMul.toLinearMap_apply] + · simp only [Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype, + LinearMap.map_smul_of_tower, DistribSMul.toLinearMap_apply] rw [← Subring.smul_def, Units.smul_def, smul_smul] simp diff --git a/LeanPool/BruhatTits/Lattice/Quotient.lean b/LeanPool/BruhatTits/Lattice/Quotient.lean index f77fabf112..e1bcb8bcdd 100644 --- a/LeanPool/BruhatTits/Lattice/Quotient.lean +++ b/LeanPool/BruhatTits/Lattice/Quotient.lean @@ -300,7 +300,8 @@ lemma _root_.BruhatTits.Lattice.mapIntermediateSubmodule_inj_of apply Submodule.comap_mono exact hge₂ have h' : Q₁.map p.mkQ = Q₂.map p.mkQ := by - rwa [← SetLike.coe_set_eq] at h ⊢ + rw [← SetLike.coe_set_eq] at h ⊢ + assumption have h'' : p.comapMkQRelIso.symm ⟨Q₁, hQ₁⟩ = p.comapMkQRelIso.symm ⟨Q₂, hQ₂⟩ := h' have h1 := p.comapMkQRelIso.symm.injective h'' replace h1 : Q₁ = Q₂ := congrArg Subtype.val h1 diff --git a/LeanPool/BruhatTits/Utils/RingHom.lean b/LeanPool/BruhatTits/Utils/RingHom.lean index cb9738fb95..d79db7fc18 100644 --- a/LeanPool/BruhatTits/Utils/RingHom.lean +++ b/LeanPool/BruhatTits/Utils/RingHom.lean @@ -55,7 +55,7 @@ lemma GL.map_det (g : GL α R) : Matrix.GeneralLinearGroup.det (GL.map f g) = Units.map f (Matrix.GeneralLinearGroup.det g) := by ext simp only [map, RingHom.mapMatrix_apply, Units.inv_eq_val_inv, Matrix.coe_units_inv, - Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe] + Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_ofClass] symm apply RingHom.map_det diff --git a/LeanPool/BruhatTits/Utils/ValuationRings.lean b/LeanPool/BruhatTits/Utils/ValuationRings.lean index 5f35c88354..1f2916ad27 100644 --- a/LeanPool/BruhatTits/Utils/ValuationRings.lean +++ b/LeanPool/BruhatTits/Utils/ValuationRings.lean @@ -285,7 +285,7 @@ lemma zaddVal'_eq_iff (n : ℤ) (x : Kˣ) : obtain ⟨y, hy⟩ := zaddVal'_spec ϖ hϖ x nth_rw 1 [← hu] at hy rw [Units.ext_iff] at hy - simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype, + simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype, Units.val_zpow_eq_zpow_val, Units.val_mk0] at hy apply unit_mul_zpow_congr_zpow hϖ hϖ y u exact hy.symm @@ -306,7 +306,7 @@ lemma zaddVal_eq_iff (n : ℤ) (x : Kˣ) : obtain ⟨p, hp, y, hy⟩ := zaddVal_spec (R := R) x nth_rw 1 [← hu] at hy rw [Units.ext_iff] at hy - simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype, + simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype, Units.val_zpow_eq_zpow_val, Units.val_mk0] at hy apply unit_mul_zpow_congr_zpow hp hϖ y u exact hy.symm diff --git a/LeanPool/CircuitComplexity/Internal/NF.lean b/LeanPool/CircuitComplexity/Internal/NF.lean index 19ba20acc4..548201787b 100644 --- a/LeanPool/CircuitComplexity/Internal/NF.lean +++ b/LeanPool/CircuitComplexity/Internal/NF.lean @@ -323,7 +323,7 @@ theorem card_true_of_flip_sensitive {N : Nat} (hN : 1 ≤ N) rw [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin]] at h convert h using 2 simp only [S_false] - congr 1; ext x; cases f x <;> simp + congr 1 -- 2 * S_true.card = 2^N, so S_true.card = 2^{N-1} have : 2 ^ N = 2 * 2 ^ (N - 1) := by cases N with diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean b/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean index 4950395476..f60091694a 100644 --- a/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean +++ b/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean @@ -1676,8 +1676,8 @@ theorem resolvedSegment_inter_of_succ_eq (i j : Fin B.resolvedWalk.length) ext x simp [] rw [himage, convexHull_singleton] - change {B.arrangementMesh.toPlaneComplex.position - (B.resolvedWalk.getVert (i.val + 1))} = {B.resolvedVertex i.succ} + change {(B.arrangementMesh.toPlaneComplex.position + (B.resolvedWalk.getVert (i.val + 1)))} = {B.resolvedVertex i.succ} rfl /-- The shifted affine edge parameters agree wherever two selected path edges meet. -/ diff --git a/LeanPool/Computability/Oracle.lean b/LeanPool/Computability/Oracle.lean index 4b1cdbcf40..d8dc09cc29 100644 --- a/LeanPool/Computability/Oracle.lean +++ b/LeanPool/Computability/Oracle.lean @@ -129,7 +129,10 @@ If a function is partial recursive, then it is recursive in every partial functi -/ lemma recursiveIn_of_partrec (pF : Nat.Partrec f) : RecursiveIn O f := by induction pF with - | zero | succ | left | right => constructor + | zero => exact RecursiveIn.zero + | succ => exact RecursiveIn.succ + | left => exact RecursiveIn.left + | right => exact RecursiveIn.right | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂ | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂ | prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂ @@ -252,7 +255,10 @@ theorem recursiveIn_mono {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂) RecursiveIn O₁ g → RecursiveIn O₂ g := by intro hg induction hg with - | zero | succ | left | right => constructor + | zero => exact RecursiveIn.zero + | succ => exact RecursiveIn.succ + | left => exact RecursiveIn.left + | right => exact RecursiveIn.right | oracle g hg => exact RecursiveIn.oracle g (hsub hg) | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂ | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂ @@ -262,7 +268,10 @@ theorem recursiveIn_mono {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂) theorem RecursiveIn_subst {O O' : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : RecursiveIn O f) (hO : ∀ g, g ∈ O → RecursiveIn O' g) : RecursiveIn O' f := by induction hf with - | zero | succ | left | right => constructor + | zero => exact RecursiveIn.zero + | succ => exact RecursiveIn.succ + | left => exact RecursiveIn.left + | right => exact RecursiveIn.right | oracle g hg => exact hO g hg | pair _ _ ihf ihg => exact .pair ihf ihg | comp _ _ ihf ihg => exact .comp ihf ihg diff --git a/LeanPool/Computability/TuringDegree.lean b/LeanPool/Computability/TuringDegree.lean index e9605431da..76294de98e 100644 --- a/LeanPool/Computability/TuringDegree.lean +++ b/LeanPool/Computability/TuringDegree.lean @@ -91,7 +91,10 @@ instance : Std.Refl TuringReducible where refl _ := .rfl theorem TuringReducible.trans (hg : f ≤ᵀ g) (hh : g ≤ᵀ h) : f ≤ᵀ h := by induction hg with - | zero | succ | left | right => constructor + | zero => exact RecursiveIn.zero + | succ => exact RecursiveIn.succ + | left => exact RecursiveIn.left + | right => exact RecursiveIn.right | oracle g' hg => rw [hg]; exact hh | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂ | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂ diff --git a/LeanPool/DemazureProduct/Avoiding321.lean b/LeanPool/DemazureProduct/Avoiding321.lean index 739fb4aafb..67f90a17ef 100644 --- a/LeanPool/DemazureProduct/Avoiding321.lean +++ b/LeanPool/DemazureProduct/Avoiding321.lean @@ -785,7 +785,7 @@ theorem eq_s_of_lel rw [v_eq_x]; simp suffices ⟨x, v⟩ ∈ invSet β ↔ ⟨x, v⟩ ∈ invSet τ by rw [β.inv_iff_le x_lt_v, τ.inv_iff_le x_lt_v] at this - constructor <;> (intro h; contrapose! h; rwa [this] at *) + constructor <;> (intro h; contrapose! h; rw [this] at *; assumption) have nested : ⟨x, v⟩ ≼ ⟨u, v⟩ := by constructor <;> linarith exact inv_of_lel_iff h_321a h_L uv_inv nested @@ -808,7 +808,7 @@ lemma eq_s'_of_lel constructor <;> (intro h; linarith) suffices ⟨u, x⟩ ∈ invSet β ↔ ⟨u, x⟩ ∈ invSet τ by rw [β.inv_iff_lt u_le_x, τ.inv_iff_lt u_le_x] at this - constructor <;> (intro h; contrapose! h; rwa [this] at *) + constructor <;> (intro h; contrapose! h; rw [this] at *; assumption) have nested : ⟨u, x⟩ ≼ ⟨u, v⟩ := by constructor <;> linarith exact inv_of_lel_iff h_321a h_L uv_inv nested diff --git a/LeanPool/Dilatations/IteratedRings.lean b/LeanPool/Dilatations/IteratedRings.lean index 7b45c2e589..1f4d91aab8 100644 --- a/LeanPool/Dilatations/IteratedRings.lean +++ b/LeanPool/Dilatations/IteratedRings.lean @@ -187,8 +187,8 @@ lemma hgen_rho (i : M.index) : rw [Ideal.map_span, Set.image_singleton] · have h : Ideal.map (algebraMap B224 C224) ((Multicenter.complement M K).ideal (⟨i, hi⟩ : (Kᶜ : Set M.index))) ≤ - Ideal.span {(algebraMap B224 C224) - ((Multicenter.complement M K).elem (⟨i, hi⟩ : (Kᶜ : Set M.index)))} := + Ideal.span {((algebraMap B224 C224) + ((Multicenter.complement M K).elem (⟨i, hi⟩ : (Kᶜ : Set M.index))))} := (gen_iff_le (Multicenter.complement M K) (⟨i, hi⟩ : (Kᶜ : Set M.index))).mp (reciprocal_for_univ (Multicenter.complement M K) (AlgHom.id B224 C224) (⟨i, hi⟩ : (Kᶜ : Set M.index))) diff --git a/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean b/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean index d329142ca7..372aa0a9d7 100644 --- a/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean +++ b/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean @@ -67,8 +67,7 @@ theorem continuous_preservesDirectedSup {f : D → D'} (Topology.IsScott.scottContinuousOn_iff_continuous (α := WithScott D) (D := univ) (fun _ _ _ => trivial)).2 hf' intro S hS hSdir - have h := hsc hS hSdir (isLUB_sSup S) - simp only [Function.comp_def, WithScott.toScott, WithScott.ofScott] at h + have h : IsLUB (f '' S) (f (sSup S)) := hsc hS hSdir (isLUB_sSup S) exact h.sSup_eq.symm /-- **Scott 1972, Proposition 2.5.** Scott continuity ↔ preservation of directed diff --git a/LeanPool/DomainTheory/Neighborhood/Exercise221.lean b/LeanPool/DomainTheory/Neighborhood/Exercise221.lean index f75aa6f6d8..64066d85fe 100644 --- a/LeanPool/DomainTheory/Neighborhood/Exercise221.lean +++ b/LeanPool/DomainTheory/Neighborhood/Exercise221.lean @@ -113,9 +113,9 @@ theorem singleton_cone_nd (σ τ : Str) : theorem singleton_singleton_nd (σ τ : Str) : ({σ} : Set Str) ⊆ ({τ} : Set Str) ∨ ({τ} : Set Str) ⊆ ({σ} : Set Str) ∨ ({σ} : Set Str) ∩ ({τ} : Set Str) = ∅ := by - rcases (inferInstance : Decidable (σ = τ)) with h | h - · simp_all + by_cases h : σ = τ · subst h; exact Or.inl subset_rfl + · simp_all /-- **`𝒞` is pairwise nested-or-disjoint.** Cone/cone is the `𝔹` trichotomy; the mixed and diff --git a/LeanPool/DomainTheory/Neighborhood/Recursive.lean b/LeanPool/DomainTheory/Neighborhood/Recursive.lean index f3a2c10e48..a0d58c39d8 100644 --- a/LeanPool/DomainTheory/Neighborhood/Recursive.lean +++ b/LeanPool/DomainTheory/Neighborhood/Recursive.lean @@ -431,9 +431,9 @@ theorem RecDecidable.not {p : ℕ → Prop} (hp : RecDecidable p) : RecDecidable equality on `ℕ`); useful for choice-free De Morgan. -/ theorem RecDecidable.em {p : ℕ → Prop} (hp : RecDecidable p) (n : ℕ) : p n ∨ ¬ p n := by obtain ⟨f, _, hfe⟩ := hp - rcases Nat.decEq (f n) 1 with h | h - · exact Or.inr (fun hp => h ((hfe n).mp hp)) + by_cases h : f n = 1 · exact Or.inl ((hfe n).mpr h) + · exact Or.inr (fun hp => h ((hfe n).mp hp)) /-- **Disjunction.** Recursive decidability is closed under `∨`, via choice-free De Morgan diff --git a/LeanPool/DomainTheory/Neighborhood/Theorem74.lean b/LeanPool/DomainTheory/Neighborhood/Theorem74.lean index 260bd6487f..9aceb55ada 100644 --- a/LeanPool/DomainTheory/Neighborhood/Theorem74.lean +++ b/LeanPool/DomainTheory/Neighborhood/Theorem74.lean @@ -241,11 +241,11 @@ master. -/ /-- Choice-free three-way split of a tag `n ∈ {0, 1, ≥2}` (via `Nat.decEq`, not classical `em`). -/ theorem tag_trichotomy (n : ℕ) : n = 0 ∨ n = 1 ∨ (n ≠ 0 ∧ n ≠ 1) := by - rcases Nat.decEq n 0 with h | h - · rcases Nat.decEq n 1 with h' | h' - · exact Or.inr (Or.inr ⟨h, h'⟩) - · exact Or.inr (Or.inl h') + by_cases h : n = 0 · exact Or.inl h + · by_cases h' : n = 1 + · exact Or.inr (Or.inl h') + · exact Or.inr (Or.inr ⟨h, h'⟩) section Sum diff --git a/LeanPool/Duality/LinearProgramming.lean b/LeanPool/Duality/LinearProgramming.lean index fdb455acf9..d8703c0166 100644 --- a/LeanPool/Duality/LinearProgramming.lean +++ b/LeanPool/Duality/LinearProgramming.lean @@ -623,7 +623,8 @@ lemma ValidELP.unbounded_of_feasible_of_neg (P : ValidELP I J F) (hP : P.IsFeasi | ⊥ => refine ⟨⊥, ⟨xₚ, hxₚ, ?_⟩, bot_le⟩ change hcx₀ to P.c ᵥ⬝ x₀ = ⊥ - rwa [←dotWeig_eq_bot] at hcx₀ ⊢ + rw [←dotWeig_eq_bot] at hcx₀ ⊢ + assumption | ⊤ => exfalso rw [hcx₀] at hx₀ diff --git a/LeanPool/FelConjecture/Solution.lean b/LeanPool/FelConjecture/Solution.lean index de79238aec..6400a3e828 100644 --- a/LeanPool/FelConjecture/Solution.lean +++ b/LeanPool/FelConjecture/Solution.lean @@ -188,17 +188,18 @@ lemma partition_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S ∑ k ∈ (Finset.range (n + 1)).filter (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide), (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) := by - have h := @Finset.sum_filter_add_sum_filter_not _ _ _ (Finset.range (n + 1)) - (fun k => k ∈ S.carrier) (Classical.decPred _) (fun x => Classical.dec _) - (fun k => (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k))) - rw [← h] - congr 1 - · congr 1 + classical + have hmem : (Finset.range (n + 1)).filter + (fun k => (Classical.propDecidable (k ∈ S.carrier)).decide) = + (Finset.range (n + 1)).filter (fun k => k ∈ S.carrier) := by ext k simp only [Finset.mem_filter, decide_eq_true_eq] - · congr 1 + have hnotmem : (Finset.range (n + 1)).filter + (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide) = + (Finset.range (n + 1)).filter (fun k => k ∉ S.carrier) := by ext k simp only [Finset.mem_filter, Bool.not_eq_true', decide_eq_false_iff_not] + rw [hmem, hnotmem, Finset.sum_filter_add_sum_filter_not] lemma filter_not_carrier_eq_gaps {S : NumericalSemigroup} (n : ℕ) : (Finset.range (n + 1)).filter (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide) = diff --git a/LeanPool/Flean/Subnorm.lean b/LeanPool/Flean/Subnorm.lean index e71aa628ef..fa761ac529 100644 --- a/LeanPool/Flean/Subnorm.lean +++ b/LeanPool/Flean/Subnorm.lean @@ -119,7 +119,6 @@ lemma subnormal_round_coe (r : IntRounder) [rh : ValidRounder r] · exact this nth_rw 4 [show m = r false m by symm; apply ValidRounder.leftInverse] congr - · simp_all have hprec : (C.prec : ℚ) ≠ 0 := by norm_cast; linarith [C.prec_pos] rw [abs_of_nonneg (by positivity), mul_assoc, mul_assoc, <-mul_assoc (2 ^ _), diff --git a/LeanPool/FltRegular/CaseII/AuxLemmas.lean b/LeanPool/FltRegular/CaseII/AuxLemmas.lean index 9c17ce7a23..bd58c23c09 100644 --- a/LeanPool/FltRegular/CaseII/AuxLemmas.lean +++ b/LeanPool/FltRegular/CaseII/AuxLemmas.lean @@ -90,7 +90,6 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDedekindDomain · exact hx.ne_zero · rw [Ne, Ideal.span_singleton_eq_bot] exact hx.ne_zero - · rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_zero] rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb rw [isPrincipal_iff] at h obtain ⟨a, ha⟩ := h diff --git a/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index 25e5d494d1..a2b3f0ee6a 100644 --- a/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -71,8 +71,8 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (h let _ := IsCyclotomicExtension.Rat.isCMField (S := {p}) K ⟨p, rfl, hp⟩ have hmap := Units.coe_map_inv (N := 𝓞 K ⧸ I) (algebraMap (𝓞 K) (𝓞 K ⧸ I)) (unitsComplexConj K u) - rw [unitsMulComplexConjInv_apply, Units.val_mul, map_mul, ← MonoidHom.coe_coe, ← hmap, - Units.mul_inv_eq_one, Units.coe_map, MonoidHom.coe_coe] + rw [unitsMulComplexConjInv_apply, Units.val_mul, map_mul, ← MonoidHom.coe_ofClass, ← hmap, + Units.mul_inv_eq_one, Units.coe_map, MonoidHom.coe_ofClass] exact (RingHom.congr_fun (quotient_zero_sub_one_comp_aut hζ (ringOfIntegersComplexConj K).toRingEquiv.toRingHom) (u : 𝓞 K)).symm diff --git a/LeanPool/FltRegular/NumberTheory/Hilbert92.lean b/LeanPool/FltRegular/NumberTheory/Hilbert92.lean index 71b96db19e..b00c9a8da4 100644 --- a/LeanPool/FltRegular/NumberTheory/Hilbert92.lean +++ b/LeanPool/FltRegular/NumberTheory/Hilbert92.lean @@ -122,7 +122,7 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G s) (hs : S.IsFundamental) have := S'.isMaximal p hp G hf suffices Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units) by exact (hs.maximal' _ _ _ S').not_gt <| AddSubgroup.index_strictAnti ‹_› - rw [SetLike.lt_iff_le_and_exists] + rw [IsConcreteLE.lt_iff_le_and_exists] constructor · rw [Submodule.span_le] rintro _ ⟨j, rfl⟩ @@ -226,8 +226,8 @@ def relativeUnitsMap (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits ((QuotientGroup.mk' _).comp (Units.map (galRestrictHom (𝓞 k) k K (𝓞 K) σ))) rintro _ ⟨i, rfl⟩ simp only [MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply, - QuotientGroup.eq_one_iff, MonoidHom.mem_range, Units.ext_iff, Units.coe_map, MonoidHom.coe_coe, - AlgHom.commutes, exists_apply_eq_apply] + QuotientGroup.eq_one_iff, MonoidHom.mem_range, Units.ext_iff, Units.coe_map, + MonoidHom.coe_ofClass, AlgHom.commutes, exists_apply_eq_apply] lemma relativeUnitsMap_mk (σ : K →ₐ[k] K) (x : (𝓞 K)ˣ) : relativeUnitsMap σ (QuotientGroup.mk x) = @@ -307,8 +307,8 @@ lemma isTors' [IsGalois k K] : Module.IsTorsionBySet ℤ[X] rw [sum_ofMul_quotient_mk_eq_zero_iff, QuotientGroup.eq_one_iff] use Units.map (RingOfIntegers.norm k) x ext - simp only [Units.coe_map, MonoidHom.coe_coe, RingOfIntegers.coe_algebraMap_norm, Units.coe_prod, - Algebra.norm_eq_prod_automorphisms] + simp only [Units.coe_map, MonoidHom.coe_ofClass, RingOfIntegers.coe_algebraMap_norm, + Units.coe_prod, Algebra.norm_eq_prod_automorphisms] rw [← hKL, ← IsGalois.card_aut_eq_finrank, ← orderOf_eq_card_of_forall_mem_zpowers hσ, ← Fin.prod_univ_eq_prod_range, ← (finEquivZPowers <| isOfFinOrder_of_finite _).symm.prod_comp] @@ -522,7 +522,7 @@ lemma Hilbert92_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ν : (𝓞 k simp only [toMul_sum, toMul_zsmul, zpow_neg, Units.val_mul, Units.coe_prod, map_mul, map_prod, Units.coe_zpow, map_mul, map_prod, Algebra.norm_zpow] rw [← map_zpow, Units.coe_map_inv] - simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe] + simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_ofClass] have hcoe1 : algebraMap (𝓞 k) k (((ν ^ p) ^ a)⁻¹).1 = ((((ν : 𝓞 k) : k) ^ p) ^ a)⁻¹ := by change ((Units.map (algebraMap (𝓞 k) k : (𝓞 k) →* k)) _).1 = _ @@ -589,7 +589,7 @@ lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : congr rw [eq_div_iff_mul_eq'] ext - simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, map_mul, + simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_ofClass, map_mul, algebraMap_galRestrictHom_apply, hu] exact div_mul_cancel₀ _ (by simp) @@ -687,7 +687,7 @@ lemma almostHilbert92 (hpodd : p ≠ 2) : ∃ η : (𝓞 K)ˣ, Algebra.norm k ( obtain ⟨S, hS⟩ := Hilbert91 p (K := K) (k := k) hp hKL σ hσ have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ p := by ext - simp only [RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, + simp only [RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_ofClass, RingOfIntegers.coe_eq_algebraMap, Units.val_pow_eq_pow_val, map_pow] rw [← map_pow] at hE refine Hilbert92_aux2 p hp hKL σ hσ E _ hE ?_ hpodd @@ -751,7 +751,7 @@ lemma almostHilbert92 (hpodd : p ≠ 2) : ∃ η : (𝓞 K)ˣ, Algebra.norm k ( ← mul_pow] at NE_p_pow apply_fun ((↑) : (𝓞 K)ˣ → K) at NE_p_pow simp only [RingHom.toMonoidHom_eq_coe, Units.val_pow_eq_pow_val, Units.val_mul, - Units.coe_map_inv, MonoidHom.coe_coe, Units.val_one] at NE_p_pow + Units.coe_map_inv, MonoidHom.coe_ofClass, Units.val_one] at NE_p_pow have : NeZero p := ⟨hp.pos.ne'⟩ obtain ⟨i, -, e⟩ := hν''.eq_pow_of_pow_eq_one NE_p_pow use ((ν ^ p ^ h) ^ i * ε') @@ -762,7 +762,7 @@ lemma almostHilbert92 (hpodd : p ≠ 2) : ∃ η : (𝓞 K)ˣ, Algebra.norm k ( ((algebraMap (𝓞 k) (𝓞 K) (ε'' : 𝓞 k) : 𝓞 K) : K) = algebraMap k K (ε'' : k) := rfl simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, ← map_pow, hε'', - RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, + RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_ofClass, hε''coe, AlgEquiv.commutes] at hE replace hE : (algebraMap k K) (((ν : 𝓞 k) : k) ^ p ^ h) = 1 := by rwa [div_self (by simp)] at hE diff --git a/LeanPool/FormalLearningTheory/Theorem/Separation.lean b/LeanPool/FormalLearningTheory/Theorem/Separation.lean index 70d300ce74..34e28dd4c3 100644 --- a/LeanPool/FormalLearningTheory/Theorem/Separation.lean +++ b/LeanPool/FormalLearningTheory/Theorem/Separation.lean @@ -565,7 +565,7 @@ private lemma majority_error_le_seven_rate_of_good_fraction simp only [Finset.card_univ, Fintype.card_fin] at hcomp2 have hfilt_false : (Finset.univ.filter (fun j : Fin k => ¬hs j x = true)).card = (Finset.univ.filter (fun j : Fin k => hs j x = false)).card := by - congr 1; ext j; simp [Bool.not_eq_true] + simp only [Bool.not_eq_true] rw [hwrongAll_def, hfilt_ne] omega have hwrong_split : wrongAll ≤ wrongGood + (k - good.card) := by diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean b/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean index 4c4761dd5a..75056918ff 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean @@ -105,7 +105,7 @@ theorem mp {L : Language} {α β} {m : ℕ} {φ : L.BoundedFormula α m} by induction φ with | falsum => - constructor + apply IsQF.falsum | equal lhs rhs => simp only [relabelEquiv, mapTermRelEquiv, Equiv.coe_refl, Equiv.refl_symm, Equiv.coe_fn_mk, mapTermRel, Term.relabelEquiv_apply] @@ -328,7 +328,7 @@ end of_notfalsum theorem neq {a n} (t1 t2 : L.Term (a ⊕ Fin n)) : (t1 ≠' t2).IsDelta0 := by - constructor + apply IsDelta0.imp · apply equal · apply bot @@ -353,15 +353,15 @@ by induction h generalizing b with | bdEx t hphi ih => rw [iBdEx'.relabelEquiv] - constructor + apply IsDelta0.bdEx exact ih (g.sumCongr (_root_.Equiv.refl _)) | bdAll t hphi ih => rw [iBdAll'.relabelEquiv] - constructor + apply IsDelta0.bdAll exact ih (g.sumCongr (_root_.Equiv.refl _)) | imp pre post ihpre ihpost => rw [relabelEquiv.imp] - constructor + apply IsDelta0.imp · exact ihpre g · exact ihpost g | of_isQF f => diff --git a/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean b/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean index 2b2eda6f5d..2d6f37636d 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean @@ -59,7 +59,7 @@ by rw [IsDelta0.of_open.not] constructor; constructor; constructor constructor; constructor - · constructor + · apply IsDelta0.bdEx rw [IsDelta0.flip] rw [IsDelta0.display2] constructor; constructor; constructor @@ -103,13 +103,13 @@ by unfold ind3 ind2 ind1 at ind specialize ind (by rw [IsDelta0.display2] - constructor + apply IsDelta0.bdEx rw [IsDelta0.flip] rw [IsDelta0.display3] - constructor - · constructor + apply IsDelta0.imp + · apply IsDelta0.imp · constructor; constructor; constructor - · constructor; constructor + · constructor; apply IsQF.falsum · constructor; constructor; constructor ) simpInduction at ind @@ -452,7 +452,7 @@ by specialize ind (by rw [IsDelta0.display3] unfold ind1 - constructor + apply IsDelta0.imp · apply IsDelta0.of_isQF apply IsQF.inf · constructor; constructor diff --git a/LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean b/LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean index 004b1851f6..9a91380610 100644 --- a/LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean +++ b/LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean @@ -43,7 +43,7 @@ theorem isSheaf_of_isColimit_of_isSheaf obtain ⟨t, ht⟩ := (NoetherianSpace.isCompact (↑(iSup U) : Set X)).elim_finite_subcover (fun i ↦ ↑(U i)) (fun i ↦ (U i).isOpen) (by simp [Opens.coe_iSup]) have hsup_le : iSup U ≤ ⨆ i ∈ t, U i := by - rw [SetLike.le_def] + rw [IsConcreteLE.le_iff] intro x hx obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx) exact Opens.mem_iSup.mpr ⟨i, Opens.mem_iSup.mpr ⟨hi, hxi⟩⟩ diff --git a/LeanPool/GrothendieckVanishing/PresheafFilteredColimitGeneral.lean b/LeanPool/GrothendieckVanishing/PresheafFilteredColimitGeneral.lean index ec4ff1088e..4bc7efa036 100644 --- a/LeanPool/GrothendieckVanishing/PresheafFilteredColimitGeneral.lean +++ b/LeanPool/GrothendieckVanishing/PresheafFilteredColimitGeneral.lean @@ -381,7 +381,7 @@ theorem colimit_restrict_eq_of_eq_on_finite_subcover ?_ (c.pt.map (Opens.leSupr U i).op s - sf i) ?_ - · rw [SetLike.le_def] + · rw [IsConcreteLE.le_iff] intro x hx obtain ⟨k, hk⟩ := Opens.mem_iSup.mp (hsup_le (le_iSup U i hx)) obtain ⟨hkt, hxk⟩ := Opens.mem_iSup.mp hk diff --git a/LeanPool/HopfProblem/Foundations/Core3.lean b/LeanPool/HopfProblem/Foundations/Core3.lean index bed632e360..3c593eb206 100644 --- a/LeanPool/HopfProblem/Foundations/Core3.lean +++ b/LeanPool/HopfProblem/Foundations/Core3.lean @@ -83,7 +83,7 @@ private theorem (hgf : ContMDiff I L ω (g ∘ f)) : ContMDiff J L ω g := by intro y obtain ⟨x, rfl⟩ := hsurj y - have h := hgf.contMDiffAt.comp (f x) (hf x).localInverse_contMDiffAt + have h := hgf.contMDiffAt.comp (f x) (hf x).contMDiffAt_localInverse apply h.congr_of_eventuallyEq filter_upwards [(hf x).localInverse_eventuallyEq_right] with z hz change g z = g (f ((hf x).localInverse z)) diff --git a/LeanPool/HopfProblem/Foundations/LocalOrbitQuotient.lean b/LeanPool/HopfProblem/Foundations/LocalOrbitQuotient.lean index ffab0192b9..808c7e9081 100644 --- a/LeanPool/HopfProblem/Foundations/LocalOrbitQuotient.lean +++ b/LeanPool/HopfProblem/Foundations/LocalOrbitQuotient.lean @@ -46,7 +46,7 @@ private theorem BranchedQuotientAtlas.project_localInverse_eventuallyEq {E M Q : rw [← hcoord] exact hf.localInverse_left_inv hf.localInverse_mem_target have hcont : ContinuousAt (q ∘ hf.localInverse) z := by - have h := hq.continuousAt.comp hf.localInverse_contMDiffAt.continuousAt + have h := hq.continuousAt.comp hf.contMDiffAt_localInverse.continuousAt simpa only [hcoord] using h have hsource : ∀ᶠ w in 𝓝 z, q (hf.localInverse w) ∈ e.source := hcont @@ -76,7 +76,7 @@ private theorem exact hf.localInverse_left_inv hf.localInverse_mem_target have hfirst : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ E) ω hf.localInverse z := by - simpa only [hcoord] using hf.localInverse_contMDiffAt + simpa only [hcoord] using hf.contMDiffAt_localInverse have hsecond : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ E) ω (f ∘ q) a := hhol.contMDiffAt ((f.open_source.preimage hq).mem_nhds diff --git a/LeanPool/HopfProblem/HomologyTheory/FirstHurewicz3.lean b/LeanPool/HopfProblem/HomologyTheory/FirstHurewicz3.lean index 2853db8f51..5d22dbec72 100644 --- a/LeanPool/HopfProblem/HomologyTheory/FirstHurewicz3.lean +++ b/LeanPool/HopfProblem/HomologyTheory/FirstHurewicz3.lean @@ -553,7 +553,8 @@ private theorem SingularMayerVietoris.coverRestriction_ambient {X Y : Type} [Top FirstHurewicz.singularChainMap (coverRestriction f A B hf) ≫ FirstHurewicz.singularChainMap (subtypeInclusion B) = FirstHurewicz.singularChainMap (subtypeInclusion A) ≫ FirstHurewicz.singularChainMap f := by - let F := ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) + let F := + ((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) have h₁ := F.map_comp (TopCat.ofHom (coverRestriction f A B hf)) (TopCat.ofHom (subtypeInclusion B)) have h₂ := F.map_comp (TopCat.ofHom (subtypeInclusion A)) (TopCat.ofHom f) @@ -566,7 +567,8 @@ private theorem intersectionToLeft U V ≫ FirstHurewicz.singularChainMap (coverRestriction f U U' hfU) = FirstHurewicz.singularChainMap (intersectionRestriction f U V U' V' hfU hfV) ≫ intersectionToLeft U' V' := by - let F := ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) + let F := + ((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) have h₁ := F.map_comp (TopCat.ofHom (ContinuousMap.inclusion (Set.inter_subset_left : U ∩ V ⊆ U))) (TopCat.ofHom (coverRestriction f U U' hfU)) @@ -581,7 +583,8 @@ private theorem SingularMayerVietoris.coverRestriction_intersection_right {X Y : intersectionToRight U V ≫ FirstHurewicz.singularChainMap (coverRestriction f V V' hfV) = FirstHurewicz.singularChainMap (intersectionRestriction f U V U' V' hfU hfV) ≫ intersectionToRight U' V' := by - let F := ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) + let F := + ((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) have h₁ := F.map_comp (TopCat.ofHom (ContinuousMap.inclusion (Set.inter_subset_right : U ∩ V ⊆ V))) (TopCat.ofHom (coverRestriction f V V' hfV)) diff --git a/LeanPool/HopfProblem/HomologyTheory/SingularMayerVietoris.lean b/LeanPool/HopfProblem/HomologyTheory/SingularMayerVietoris.lean index fd5e025cd4..12d8a29618 100644 --- a/LeanPool/HopfProblem/HomologyTheory/SingularMayerVietoris.lean +++ b/LeanPool/HopfProblem/HomologyTheory/SingularMayerVietoris.lean @@ -1079,7 +1079,8 @@ private theorem private theorem FirstHurewicz.inducedHomology_id {X : Type} [TopologicalSpace X] : inducedHomology (ContinuousMap.id X) = LinearMap.id := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ)).map_id + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) 1).obj (ModuleCat.of ℤ ℤ)).map_id (TopCat.of X) exact congrArg ModuleCat.Hom.hom h @@ -1087,7 +1088,8 @@ private theorem FirstHurewicz.inducedHomology_comp {X Y Z : Type} [TopologicalSp [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) : inducedHomology (g.comp f) = (inducedHomology g).comp (inducedHomology f) := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ)).map_comp + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) 1).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom f) (TopCat.ofHom g) exact congrArg ModuleCat.Hom.hom h @@ -1559,7 +1561,7 @@ private theorem SingularMayerVietoris.intersectionToLeft_ambient {X : Type} [Top intersectionToLeft U V ≫ FirstHurewicz.singularChainMap (subtypeInclusion U) = FirstHurewicz.singularChainMap (subtypeInclusion (U ∩ V)) := by have h := - ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj + ((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom (ContinuousMap.inclusion (Set.inter_subset_left : U ∩ V ⊆ U))) (TopCat.ofHom (subtypeInclusion U)) @@ -1570,7 +1572,7 @@ private theorem SingularMayerVietoris.intersectionToRight_ambient {X : Type} [To intersectionToRight U V ≫ FirstHurewicz.singularChainMap (subtypeInclusion V) = FirstHurewicz.singularChainMap (subtypeInclusion (U ∩ V)) := by have h := - ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj + ((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom (ContinuousMap.inclusion (Set.inter_subset_right : U ∩ V ⊆ V))) (TopCat.ofHom (subtypeInclusion V)) diff --git a/LeanPool/HopfProblem/Prelude.lean b/LeanPool/HopfProblem/Prelude.lean index b8d8797c32..3c59455bb7 100644 --- a/LeanPool/HopfProblem/Prelude.lean +++ b/LeanPool/HopfProblem/Prelude.lean @@ -102,7 +102,7 @@ public import Mathlib.Topology.Sheaves.EtaleSpace public import Mathlib.Topology.Subpath public import Mathlib.Topology.UniformSpace.Ascoli public import Mathlib.Topology.UniformSpace.Uniformizable -public import Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult +public import Std.Tactic.BVDecide.LRAT.Internal.Rup /-! # Hopf problem: prelude diff --git a/LeanPool/HopfProblem/Recognition/Degree1.lean b/LeanPool/HopfProblem/Recognition/Degree1.lean index 23e5d7e460..eadd668301 100644 --- a/LeanPool/HopfProblem/Recognition/Degree1.lean +++ b/LeanPool/HopfProblem/Recognition/Degree1.lean @@ -4472,7 +4472,7 @@ private theorem obtain ⟨t, rfl⟩ := Circle.exp_surjective z let h := circleExp_localDiffeomorph t have hs : ContMDiffAt (𝓡 1) J ∞ ((γ ∘ Circle.exp) ∘ h.localInverse) (Circle.exp t) := - (hγ.contMDiffAt (x := h.localInverse (Circle.exp t))).comp _ h.localInverse_contMDiffAt + (hγ.contMDiffAt (x := h.localInverse (Circle.exp t))).comp _ h.contMDiffAt_localInverse apply hs.congr_of_eventuallyEq filter_upwards [h.localInverse_eventuallyEq_right] with y hy exact (congrArg γ hy).symm diff --git a/LeanPool/HopfProblem/Recognition/Degree2.lean b/LeanPool/HopfProblem/Recognition/Degree2.lean index 7441cfb88d..8af979efad 100644 --- a/LeanPool/HopfProblem/Recognition/Degree2.lean +++ b/LeanPool/HopfProblem/Recognition/Degree2.lean @@ -2193,14 +2193,10 @@ private theorem Degree.FlowSuspension.native_field_transition_pushforward {D B E unfold Smale.FlowConstruction.partialChartField rw [VectorField.mpullback_apply] exact hinv.self_apply_inverse _ - rw [← mfderiv_eq_fderiv, - mfderiv_comp p (C.symm.mdifferentiableAt (by simp) hpC) (A.mdifferentiableAt (by simp) hpA)] - change - (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, B) C.symm (A p)) - ((mfderiv 𝓘(ℝ, D) 𝓘(ℝ, E) A p) ((NormedSpace.fromTangentSpace p).symm (WA p))) = - _ - rw [hpushA] - exact hpushC + have hchain := mfderiv_comp_apply p (C.symm.mdifferentiableAt (by simp) hpC) + (A.mdifferentiableAt (by simp) hpA) ((NormedSpace.fromTangentSpace p).symm (WA p)) + rw [hpushA] at hchain + simpa only [mfderiv_eq_fderiv] using! hchain.trans hpushC private theorem Degree.FlowSuspension.native_vertical_transition_derivative {E M : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace M] [ChartedSpace E M] {Z : Type*} diff --git a/LeanPool/HopfProblem/Recognition/Degree3.lean b/LeanPool/HopfProblem/Recognition/Degree3.lean index 111fb7ee51..b592d60e11 100644 --- a/LeanPool/HopfProblem/Recognition/Degree3.lean +++ b/LeanPool/HopfProblem/Recognition/Degree3.lean @@ -5253,12 +5253,13 @@ private theorem MorseCancel.fderiv_retimed_trace_parameter {U H X N : Type*} [No rw [hcenter] exact hG change fderiv ℝ (G ∘ Ψ) 0 = _ - rw [← mfderiv_eq_fderiv, mfderiv_comp 0 hG' (Ψ.mdifferentiableAt (by simp) hΨ), hcenter] + have hderiv := mfderiv_comp 0 hG' (Ψ.mdifferentiableAt (by simp) hΨ) + rw [hcenter] at hderiv rw [show (mfderiv (𝓘(ℝ, ℝ).prod I) 𝓘(ℝ, N) G (σ, x) : (ℝ × U) →L[ℝ] N) = mfderiv (𝓘(ℝ, ℝ).prod I) 𝓘(ℝ, N) F (τ, x) - from mfderiv_retime_unit_rate hF hD hpoint] - rfl + from mfderiv_retime_unit_rate hF hD hpoint] at hderiv + simpa only [mfderiv_eq_fderiv] using! hderiv private theorem MorseCancel.exists_shared_passage_frames {N : Type} [NormedAddCommGroup N] [NormedSpace ℝ N] [FiniteDimensional ℝ N] diff --git a/LeanPool/HopfProblem/Recognition/Smale1.lean b/LeanPool/HopfProblem/Recognition/Smale1.lean index 086ecd6c0a..c223214c4b 100644 --- a/LeanPool/HopfProblem/Recognition/Smale1.lean +++ b/LeanPool/HopfProblem/Recognition/Smale1.lean @@ -1092,10 +1092,10 @@ private theorem Smale.ManifoldMorse.mem_criticalPoints_iff {E M : Type*} [Normed have hcomp : fderiv ℝ (f ∘ e.symm) (e x) = (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, ℝ) f x).comp (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) e.symm (e x)) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp (e x) (hf.mdifferentiableAt (by simp)) - (he'.mdifferentiableAt_symm (e.map_source hx))] - rw [e.left_inv hx] + ext v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq (e x) (hf.mdifferentiableAt (by simp)) + (he'.mdifferentiableAt_symm (e.map_source hx)) (e.left_inv hx) v) rw [hcomp] change mfderiv 𝓘(ℝ, E) 𝓘(ℝ, ℝ) f x = 0 ↔ _ constructor @@ -1210,10 +1210,10 @@ private theorem Smale.FlowConstruction.mvfderiv_chartDirection {E M : Type*} [No have hc : fderiv ℝ (f ∘ e.symm) (e x) = (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, ℝ) f x).comp (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) e.symm (e x)) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp (e x) (hf.mdifferentiableAt (by simp)) - (he'.mdifferentiableAt_symm (e.map_source hx))] - rw [e.left_inv hx] + ext v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq (e x) (hf.mdifferentiableAt (by simp)) + (he'.mdifferentiableAt_symm (e.map_source hx)) (e.left_inv hx) v) unfold chartDirection rw [VectorField.mpullback_apply, hi] exact (congrArg (fun A : E →L[ℝ] ℝ => A w) hc).symm @@ -1484,10 +1484,10 @@ private theorem have hc : fderiv ℝ (f ∘ e'.symm) (e' x) = (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, ℝ) f x).comp (mfderiv 𝓘(ℝ, F) 𝓘(ℝ, E) e'.symm (e' x)) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp (e' x) (hf.mdifferentiableAt (by simp)) - (he.mdifferentiableAt_symm (e'.map_source hx))] - rw [e'.left_inv hx] + ext v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq (e' x) (hf.mdifferentiableAt (by simp)) + (he.mdifferentiableAt_symm (e'.map_source hx)) (e'.left_inv hx) v) unfold partialChartField rw [VectorField.mpullback_apply] change diff --git a/LeanPool/HopfProblem/Recognition/Smale11.lean b/LeanPool/HopfProblem/Recognition/Smale11.lean index 3fbd4f0423..4dc83e6b54 100644 --- a/LeanPool/HopfProblem/Recognition/Smale11.lean +++ b/LeanPool/HopfProblem/Recognition/Smale11.lean @@ -2632,8 +2632,8 @@ private theorem Smale.CoverNaturality.chainMap_comp {X Y Z : Type} [TopologicalS [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) : FirstHurewicz.singularChainMap f ≫ FirstHurewicz.singularChainMap g = FirstHurewicz.singularChainMap (g.comp f) := - (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)).map_comp - (TopCat.ofHom f) (TopCat.ofHom g)).symm + (((AlgebraicTopology.singularChainComplexFunctor.{0} (ModuleCat.{0} ℤ)).obj + (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom f) (TopCat.ofHom g)).symm public theorem Smale.CoverNaturality.map_intersection {X Y : Type} [TopologicalSpace X] diff --git a/LeanPool/HopfProblem/Recognition/Smale2.lean b/LeanPool/HopfProblem/Recognition/Smale2.lean index 22afd697ca..f468fa2a89 100644 --- a/LeanPool/HopfProblem/Recognition/Smale2.lean +++ b/LeanPool/HopfProblem/Recognition/Smale2.lean @@ -5047,10 +5047,11 @@ private theorem Smale.exists_partialDiffeomorph_into_manifold {D E M : Type*} [N have hcinv : (mfderiv 𝓘(ℝ, E) 𝓘(ℝ, E) c (f x)).IsInvertible := isInvertible_mfderiv_extChartAt (mem_extChartAt_source (f x)) have hderiv : (fderiv ℝ (c ∘ f) x).IsInvertible := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp x (c.mdifferentiableAt (by simp) hc) + have hmanifold : (mfderiv 𝓘(ℝ, D) 𝓘(ℝ, E) (c ∘ f) x).IsInvertible := by + rw [mfderiv_comp x (c.mdifferentiableAt (by simp) hc) ((hf.contMDiffAt (hU.mem_nhds hx)).mdifferentiableAt (by simp))] - exact hcinv.comp hinv + exact hcinv.comp hinv + simpa only [mfderiv_eq_fderiv] using! hmanifold obtain ⟨d, hd, hdV, hdf⟩ := NoExotic.exists_partialDiffeomorph_of_contDiffOn hV hxV hcf hderiv have hdx : d x ∈ c.target := by rw [hdf] @@ -5260,8 +5261,9 @@ private theorem Smale.CollarHeight.mfderiv_height_zero {D H X : Type*} [NormedAd rw [mfderiv_eq_fderiv, htime.hasFDerivAt.fderiv] apply ContinuousLinearMap.ext intro t - simp only [ContinuousLinearMap.toSpanSingleton_apply, ContinuousLinearMap.id_apply, - smul_eq_mul, mul_one] + change ℝ at t + change t * (1 : ℝ) = t + exact mul_one t apply ContinuousLinearMap.ext intro v rw [mfderiv_prod_eq_add_apply ((hh.contMDiffAt (hU.mem_nhds hx)).mdifferentiableAt (by simp)), diff --git a/LeanPool/HopfProblem/Recognition/Smale3.lean b/LeanPool/HopfProblem/Recognition/Smale3.lean index d35db593c9..48e3f836e3 100644 --- a/LeanPool/HopfProblem/Recognition/Smale3.lean +++ b/LeanPool/HopfProblem/Recognition/Smale3.lean @@ -1213,9 +1213,9 @@ private theorem Smale.NativeEuclideanEmbedding.fderiv_comp_eq {E M D : Type*} [N (hf : ContMDiff 𝓘(ℝ, D) 𝓘(ℝ, E) ∞ f) (x : D) : fderiv ℝ (e.toFun ∘ f) x = (mvfderiv 𝓘(ℝ, E) e.toFun (f x)).comp (mfderiv 𝓘(ℝ, D) 𝓘(ℝ, E) f x) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp x (e.smooth.mdifferentiableAt (by simp)) (hf.mdifferentiableAt (by simp))] - rfl + simpa only [mvfderiv_eq_fderiv] using! + (mvfderiv_comp x (e.smooth.mdifferentiableAt (by simp)) + (hf.mdifferentiableAt (by simp))) private theorem Smale.NativeEuclideanEmbedding.diskTangentImage_le {E M D : Type*} [NormedAddCommGroup E] diff --git a/LeanPool/HopfProblem/Recognition/Smale4.lean b/LeanPool/HopfProblem/Recognition/Smale4.lean index ab61f703a9..228258fdcb 100644 --- a/LeanPool/HopfProblem/Recognition/Smale4.lean +++ b/LeanPool/HopfProblem/Recognition/Smale4.lean @@ -4380,8 +4380,8 @@ private theorem Smale.NativeSubmersion.surjective_fderiv_sourceChart_iff {E F H let A : E →L[ℝ] F := mfderiv I 𝓘(ℝ, F) f (c.symm z) let B : E →L[ℝ] E := mfderiv 𝓘(ℝ, E) I c.symm z have hd : fderiv ℝ (f ∘ c.symm) z = A.comp B := by - rw [← mfderiv_eq_fderiv] - exact mfderiv_comp z hf (c.symm.mdifferentiableAt (by simp) hz) + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp z hf (c.symm.mdifferentiableAt (by simp) hz)) have hB : Function.Surjective B := (Smale.PartialChart.bijective_mfderiv c.symm hz).surjective rw [hd] change Function.Surjective (A.comp B) ↔ Function.Surjective A @@ -4521,12 +4521,13 @@ private theorem Smale.RegularValues.exists_null_exceptional_values_in_chart {E F have hinner : MDifferentiableAt 𝓘(ℝ, F) I (c.symm ∘ L.symm) z := (c.symm.mdifferentiableAt (by simp) (hcoord z hz).1).comp z L.symm.toContinuousLinearMap.differentiableAt.mdifferentiableAt - rw [← mfderiv_eq_fderiv] at hbij - change Function.Bijective (mfderiv 𝓘(ℝ, F) 𝓘(ℝ, F) (f ∘ (c.symm ∘ L.symm)) z) at hbij - rw [mfderiv_comp z hfx' hinner] at hbij + have hbijManifold : + Function.Bijective (mfderiv 𝓘(ℝ, F) 𝓘(ℝ, F) (f ∘ (c.symm ∘ L.symm)) z) := by + simpa only [mfderiv_eq_fderiv] using! hbij + rw [mfderiv_comp z hfx' hinner] at hbijManifold have hsurj : Function.Surjective (mfderiv I 𝓘(ℝ, F) f (c.symm (L.symm z))) := by intro w - obtain ⟨v, hv⟩ := hbij.surjective w + obtain ⟨v, hv⟩ := hbijManifold.surjective w exact ⟨mfderiv 𝓘(ℝ, F) I (c.symm ∘ L.symm) z v, hv⟩ exact hpoint ▸ hsurj diff --git a/LeanPool/HopfProblem/Recognition/Smale5.lean b/LeanPool/HopfProblem/Recognition/Smale5.lean index 87c75c2531..5448a0231a 100644 --- a/LeanPool/HopfProblem/Recognition/Smale5.lean +++ b/LeanPool/HopfProblem/Recognition/Smale5.lean @@ -2113,7 +2113,8 @@ private theorem Smale.ManifoldImmersion.injective_fderiv_chart_iff {E G F H N : {x : E} (hf : MDifferentiableAt 𝓘(ℝ, E) J f x) (hx : f x ∈ c.source) : Function.Injective (fderiv ℝ (c ∘ f) x) ↔ Function.Injective (mfderiv 𝓘(ℝ, E) J f x) := by have hderiv : fderiv ℝ (c ∘ f) x = (mfderiv J 𝓘(ℝ, F) c (f x)).comp (mfderiv 𝓘(ℝ, E) J f x) := by - rw [← mfderiv_eq_fderiv, mfderiv_comp x (c.mdifferentiableAt (by simp) hx) hf] + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp x (c.mdifferentiableAt (by simp) hx) hf) have hc : Function.Injective (mfderiv J 𝓘(ℝ, F) c (f x)) := ((c.isLocalDiffeomorphAt J 𝓘(ℝ, F) ∞ hx).mfderivToContinuousLinearEquiv (by simp)).injective rw [hderiv] @@ -2129,7 +2130,8 @@ private theorem Smale.ManifoldImmersion.fderiv_chart_eq_zero_iff {E G F H N : Ty {x : E} (hf : MDifferentiableAt 𝓘(ℝ, E) J f x) (hx : f x ∈ c.source) (v : E) : fderiv ℝ (c ∘ f) x v = 0 ↔ mfderiv 𝓘(ℝ, E) J f x v = 0 := by have hderiv : fderiv ℝ (c ∘ f) x = (mfderiv J 𝓘(ℝ, F) c (f x)).comp (mfderiv 𝓘(ℝ, E) J f x) := by - rw [← mfderiv_eq_fderiv, mfderiv_comp x (c.mdifferentiableAt (by simp) hx) hf] + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp x (c.mdifferentiableAt (by simp) hx) hf) have hc : Function.Injective (mfderiv J 𝓘(ℝ, F) c (f x)) := ((c.isLocalDiffeomorphAt J 𝓘(ℝ, F) ∞ hx).mfderivToContinuousLinearEquiv (by simp)).injective rw [hderiv] diff --git a/LeanPool/HopfProblem/Recognition/Smale6.lean b/LeanPool/HopfProblem/Recognition/Smale6.lean index 1eb84947d9..44acdb156f 100644 --- a/LeanPool/HopfProblem/Recognition/Smale6.lean +++ b/LeanPool/HopfProblem/Recognition/Smale6.lean @@ -3903,15 +3903,17 @@ private theorem Smale.NativeEuclideanEmbedding.SmoothRetraction.mfderiv_sheetCoo fderiv ℝ (e.toFun ∘ f) 0 = (mfderiv 𝓘(ℝ, E) (𝓡 e.ambientDimension) e.toFun (f 0)).comp (mfderiv 𝓘(ℝ, D) 𝓘(ℝ, E) f 0) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp 0 (e.smooth.mdifferentiableAt (by simp)) (hf.mdifferentiableAt (by simp))] + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp 0 (e.smooth.mdifferentiableAt (by simp)) (hf.mdifferentiableAt (by simp))) have hdg : fderiv ℝ (e.toFun ∘ g) 0 = (mfderiv 𝓘(ℝ, E) (𝓡 e.ambientDimension) e.toFun (f 0)).comp (mfderiv 𝓘(ℝ, Z) 𝓘(ℝ, E) g 0) := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp 0 (e.smooth.mdifferentiableAt (by simp)) (hg.mdifferentiableAt (by simp))] - rw [hzero] + apply ContinuousLinearMap.ext + intro v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq 0 (e.smooth.mdifferentiableAt (by simp)) + (hg.mdifferentiableAt (by simp)) hzero v) rw [sheetCoordinates, mfderiv_comp (0, 0) hr hsum.differentiableAt.mdifferentiableAt, mfderiv_eq_fderiv, hsum.fderiv, hbase, hdf, hdg] apply ContinuousLinearMap.ext @@ -5239,20 +5241,16 @@ private theorem Smale.StripNormalData.injective_normalFrame_of_strip_germ {A B Z have hnormal := (Smale.TransverseCoordinates.contMDiffOn_normalCoordinate Ψ).contMDiffAt (Ψ.open_target.mem_nhds htarget) - have hnormal' : - ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, Z) ∞ (Smale.TransverseCoordinates.normalCoordinate Ψ) - (d.chart (Smale.StripCoordinates.center t)) := by - rw [← hfp] - exact hnormal have htransition : fderiv ℝ (Smale.TransverseCoordinates.normalCoordinate Ψ ∘ d.chart) (Smale.StripCoordinates.center t) = Q.comp T := by - rw [← mfderiv_eq_fderiv, - mfderiv_comp (Smale.StripCoordinates.center t) (hnormal'.mdifferentiableAt (by simp)) - (d.chart.mdifferentiableAt (by simp) (d.line ht))] - rw [← hfp] - rfl + apply ContinuousLinearMap.ext + intro v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq (Smale.StripCoordinates.center t) + (hnormal.mdifferentiableAt (by simp)) + (d.chart.mdifferentiableAt (by simp) (d.line ht)) hfp.symm v) change Function.Injective ((fderiv ℝ (Smale.TransverseCoordinates.normalCoordinate Ψ ∘ d.chart) diff --git a/LeanPool/HopfProblem/Recognition/Smale7.lean b/LeanPool/HopfProblem/Recognition/Smale7.lean index b42b1ceb6c..97b14a7b6c 100644 --- a/LeanPool/HopfProblem/Recognition/Smale7.lean +++ b/LeanPool/HopfProblem/Recognition/Smale7.lean @@ -3979,12 +3979,16 @@ private theorem Smale.StripNormalData.bijective_tubularTransitionDerivative {A B (htarget : d.chart (Smale.StripCoordinates.center t) ∈ Ψ.target) : Function.Bijective (d.tubularTransitionDerivative Ψ t) := by unfold tubularTransitionDerivative - rw [← mfderiv_eq_fderiv, - mfderiv_comp (Smale.StripCoordinates.center t) (Ψ.symm.mdifferentiableAt (by simp) htarget) + have hmanifold : Function.Bijective + (mfderiv 𝓘(ℝ, Smale.StripCoordinates.Space A B) 𝓘(ℝ, (ℝ × ℝ) × Z) + (Ψ.symm ∘ d.chart) (Smale.StripCoordinates.center t)) := by + rw [mfderiv_comp (Smale.StripCoordinates.center t) + (Ψ.symm.mdifferentiableAt (by simp) htarget) (d.chart.mdifferentiableAt (by simp) (d.line ht))] - exact - (Smale.PartialChart.bijective_mfderiv Ψ.symm htarget).comp - (Smale.PartialChart.bijective_mfderiv d.chart (d.line ht)) + exact + (Smale.PartialChart.bijective_mfderiv Ψ.symm htarget).comp + (Smale.PartialChart.bijective_mfderiv d.chart (d.line ht)) + simpa only [mfderiv_eq_fderiv] using! hmanifold private theorem Smale.StripNormalData.sheet_coprod_complement_eq {A B Z E M : Type*} [NormedAddCommGroup A] [NormedSpace ℝ A] [NormedAddCommGroup B] [NormedSpace ℝ B] @@ -4085,13 +4089,13 @@ private theorem Smale.StripNormalData.normalDetector_eq_native {A B Z E M N : Ty Ψ (Ψ.symm (d.chart (Smale.StripCoordinates.center t))) = d.chart (Smale.StripCoordinates.center t) := Ψ.right_inv' htarget - have hq' : - MDifferentiableAt 𝓘(ℝ, E) 𝓘(ℝ, N) q - (Ψ (Ψ.symm (d.chart (Smale.StripCoordinates.center t)))) := - hinv.symm ▸ hq.mdifferentiableAt (by simp) unfold normalDetector - rw [← mfderiv_eq_fderiv, - mfderiv_comp _ hq' (Ψ.mdifferentiableAt (by simp) (Ψ.map_target' htarget)), hinv] + apply ContinuousLinearMap.ext + intro v + simpa only [mfderiv_eq_fderiv] using! + (mfderiv_comp_apply_of_eq (Ψ.symm (d.chart (Smale.StripCoordinates.center t))) + (hq.mdifferentiableAt (by simp)) + (Ψ.mdifferentiableAt (by simp) (Ψ.map_target' htarget)) hinv v) private theorem Smale.StripNormalData.surjective_normalDetector {A B Z E M N : Type*} [NormedAddCommGroup A] [NormedSpace ℝ A] [NormedAddCommGroup B] [NormedSpace ℝ B] diff --git a/LeanPool/HopfProblem/Recognition/Smale8.lean b/LeanPool/HopfProblem/Recognition/Smale8.lean index 35c6a91b96..66014986b6 100644 --- a/LeanPool/HopfProblem/Recognition/Smale8.lean +++ b/LeanPool/HopfProblem/Recognition/Smale8.lean @@ -691,9 +691,11 @@ private theorem Smale.TransverseCoordinates.bijective_normalDerivative_transvers have hnormal := (contMDiffOn_normalCoordinate Φ).contMDiffAt (Φ.open_target.mem_nhds hy) have hg : ContMDiffAt 𝓘(ℝ, Z) 𝓘(ℝ, B) ∞ (normalCoordinate Φ ∘ G) (c z) := hnormal.comp (c z) hG.contMDiffAt - rw [← mfderiv_eq_fderiv, - mfderiv_comp z (hg.mdifferentiableAt (by simp)) (c.mdifferentiableAt (by simp) hz)] - exact hb.comp (Smale.PartialChart.bijective_mfderiv c hz) + have hmanifold : Function.Bijective + (mfderiv 𝓘(ℝ, Z') 𝓘(ℝ, B) ((normalCoordinate Φ ∘ G) ∘ c) z) := by + rw [mfderiv_comp z (hg.mdifferentiableAt (by simp)) (c.mdifferentiableAt (by simp) hz)] + exact hb.comp (Smale.PartialChart.bijective_mfderiv c hz) + simpa only [mfderiv_eq_fderiv] using! hmanifold private def Smale.NativeParametrization.line {D : Type*} [NormedAddCommGroup D] [NormedSpace ℝ D] (u : D) : ℝ →L[ℝ] D := diff --git a/LeanPool/HopfProblem/Recognition/Smale9.lean b/LeanPool/HopfProblem/Recognition/Smale9.lean index c9a4b7c342..9ca5131e57 100644 --- a/LeanPool/HopfProblem/Recognition/Smale9.lean +++ b/LeanPool/HopfProblem/Recognition/Smale9.lean @@ -1403,6 +1403,9 @@ private theorem MorseCancel.nativeBeltLevelArc_transverse {E M : Type*} [NormedA have hnormalDerivative : mfderiv 𝓘(ℝ, ℝ) 𝓘(ℝ, d.chart.NegativeCoordinates) (d.beltNormal ∘ γ) 0 = L := by rw [hgerm.mfderiv_eq', mfderiv_eq_fderiv, L.fderiv] + apply ContinuousLinearMap.ext + intro s + rfl have hγ := (nativeBeltLevelArc_contMDiffOn S hf q u v).contMDiffAt (Ioo_mem_nhds (show (-1 : ℝ) < 0 by norm_num) (show (0 : ℝ) < 1 by norm_num)) diff --git a/LeanPool/HopfProblem/Threefold/SpecialPeriods11.lean b/LeanPool/HopfProblem/Threefold/SpecialPeriods11.lean index 0f4270887f..13fc480d4d 100644 --- a/LeanPool/HopfProblem/Threefold/SpecialPeriods11.lean +++ b/LeanPool/HopfProblem/Threefold/SpecialPeriods11.lean @@ -1696,7 +1696,7 @@ private theorem SpecialPeriods.Threefold.VerticalAction.Gluing.holomorphic_of_co ContMDiff (((modelWithCornersSelf ℂ (ℂ × ComplexPlane₂))).prod (modelWithCornersSelf ℂ ℂ)) (modelWithCornersSelf ℂ (ℂ × ComplexPlane₂)) ω (f ∘ q) := hf i - have hh := hc.contMDiffAt.comp (q (x, s)) hq.localInverse_contMDiffAt + have hh := hc.contMDiffAt.comp (q (x, s)) hq.contMDiffAt_localInverse apply hh.congr_of_eventuallyEq filter_upwards [hq.localInverse_eventuallyEq_right] with z hz change f z = f (q (hq.localInverse z)) @@ -3635,7 +3635,7 @@ private theorem SpecialPeriods.Threefold.VerticalAction.Factor.AdditiveFlow.act_ let e := SpecialPeriods.Threefold.VerticalAction.Exponential.normalizedExponential_isLocalDiffeomorph s have hlog : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω e.localInverse p.2 := by - simpa only [hs] using e.localInverse_contMDiffAt + simpa only [hs] using e.contMDiffAt_localInverse have hpair : ContMDiffAt (I.prod 𝓘(ℂ)) (I.prod 𝓘(ℂ)) ω (fun q : M × ℂˣ => (q.1, e.localInverse q.2)) p := contMDiffAt_fst.prodMk (hlog.comp p contMDiffAt_snd) diff --git a/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology1.lean b/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology1.lean index e384ba6a4d..4a376bbb19 100644 --- a/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology1.lean +++ b/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology1.lean @@ -38,7 +38,8 @@ private theorem PeriodTorusHigherHomology.singularHomologyMap_id (X : Type) [TopologicalSpace X] (n : ℕ) : SingularMayerVietoris.singularHomologyMap (ContinuousMap.id X) n = LinearMap.id := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_id + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_id (TopCat.of X) exact congrArg ModuleCat.Hom.hom h @@ -49,7 +50,8 @@ theorem PeriodTorusHigherHomology.singularHomologyMap_comp {X Y Z : Type} [Topol (SingularMayerVietoris.singularHomologyMap g n).comp (SingularMayerVietoris.singularHomologyMap f n) := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom f) (TopCat.ofHom g) exact congrArg ModuleCat.Hom.hom h diff --git a/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology2.lean b/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology2.lean index 9c7a028a95..4f213c285f 100644 --- a/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology2.lean +++ b/LeanPool/HopfProblem/TorusHomology/PeriodTorusHigherHomology2.lean @@ -489,7 +489,8 @@ private theorem PeriodTorusHigherHomology.sumElim_homology_inl_mo1973_4520 {X : (SingularMayerVietoris.singularHomologyMap (sumInlMap X Y) n a) = SingularMayerVietoris.singularHomologyMap f n a := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom (sumInlMap X Y)) (TopCat.ofHom (sumElimMap f g)) exact (LinearMap.congr_fun (congrArg ModuleCat.Hom.hom h) a).symm @@ -500,7 +501,8 @@ private theorem PeriodTorusHigherHomology.sumElim_homology_inr_mo1973_4521 {X : (SingularMayerVietoris.singularHomologyMap (sumInrMap X Y) n a) = SingularMayerVietoris.singularHomologyMap g n a := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_comp (TopCat.ofHom (sumInrMap X Y)) (TopCat.ofHom (sumElimMap f g)) exact (LinearMap.congr_fun (congrArg ModuleCat.Hom.hom h) a).symm @@ -508,7 +510,8 @@ private theorem PeriodTorusHigherHomology.disjointHomology_id_apply_mo1973_4522 [TopologicalSpace X] (n : ℕ) (a : SingularMayerVietoris.SingularHomology X n) : SingularMayerVietoris.singularHomologyMap (ContinuousMap.id X) n a = a := by have h := - ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_id + ((AlgebraicTopology.singularHomologyFunctor.{0} + (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).map_id (TopCat.of X) exact LinearMap.congr_fun (congrArg ModuleCat.Hom.hom h) a diff --git a/LeanPool/HopfProblem/Uniformization/SpecialPeriods5.lean b/LeanPool/HopfProblem/Uniformization/SpecialPeriods5.lean index e592079bf9..8783379bf9 100644 --- a/LeanPool/HopfProblem/Uniformization/SpecialPeriods5.lean +++ b/LeanPool/HopfProblem/Uniformization/SpecialPeriods5.lean @@ -2677,7 +2677,7 @@ private theorem filter_upwards [V.isOpen.mem_nhds hz] with w hw exact descend_project V f hV hInv hw have h := - hcomp.comp_of_eq hp.localInverse_contMDiffAt + hcomp.comp_of_eq hp.contMDiffAt_localInverse (hp.localInverse_left_inv hp.localInverse_mem_target) apply h.congr_of_eventuallyEq filter_upwards [hp.localInverse_eventuallyEq_right] with r hr @@ -4573,7 +4573,7 @@ private theorem SpecialPeriods.MuTorsor.compactExtension_holomorphicAt_openInclu ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω (compactExtension f c ∘ SpecialPeriods.triangleOpenInclusion) q := hf q have h := - hcomp.comp_of_eq hp.localInverse_contMDiffAt + hcomp.comp_of_eq hp.contMDiffAt_localInverse (hp.localInverse_left_inv hp.localInverse_mem_target) apply h.congr_of_eventuallyEq filter_upwards [hp.localInverse_eventuallyEq_right] with x hx diff --git a/LeanPool/HopfProblem/Uniformization/TriangleUniformizationGluing.lean b/LeanPool/HopfProblem/Uniformization/TriangleUniformizationGluing.lean index 76cfd7daa8..5541392abb 100644 --- a/LeanPool/HopfProblem/Uniformization/TriangleUniformizationGluing.lean +++ b/LeanPool/HopfProblem/Uniformization/TriangleUniformizationGluing.lean @@ -1079,7 +1079,7 @@ private theorem TriangleUniformizationGluing.BoundaryMap.quotientMap_holomorphic obtain ⟨z, rfl⟩ := SpecialPeriods.triangleOrbitProjection_surjective q have hp := SpecialPeriods.triangleOrbitProjection_isLocalDiffeomorphAt_of_not_elliptic h₁ h₂ have h := - hup.contMDiffAt.comp (SpecialPeriods.triangleOrbitProjection z) hp.localInverse_contMDiffAt + hup.contMDiffAt.comp (SpecialPeriods.triangleOrbitProjection z) hp.contMDiffAt_localInverse apply h.congr_of_eventuallyEq filter_upwards [hp.localInverse_eventuallyEq_right] with y hy change @@ -1141,7 +1141,7 @@ private theorem hfinite.comp hq have hi := SpecialPeriods.triangleOpenInclusion_isLocalDiffeomorph q have h := - hcomp.contMDiffAt.comp (SpecialPeriods.triangleOpenInclusion q) hi.localInverse_contMDiffAt + hcomp.contMDiffAt.comp (SpecialPeriods.triangleOpenInclusion q) hi.contMDiffAt_localInverse apply h.congr_of_eventuallyEq filter_upwards [hi.localInverse_eventuallyEq_right] with z hz change diff --git a/LeanPool/Incompleteness/Foundation/Logic/HilbertStyle/Basic.lean b/LeanPool/Incompleteness/Foundation/Logic/HilbertStyle/Basic.lean index 6c427b161e..534443dab7 100644 --- a/LeanPool/Incompleteness/Foundation/Logic/HilbertStyle/Basic.lean +++ b/LeanPool/Incompleteness/Foundation/Logic/HilbertStyle/Basic.lean @@ -67,7 +67,7 @@ def imply₁' [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (h : 𝓢 ⊢ φ) : lemma «imply₁'!» [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (d : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ ==> φ := ⟨imply₁' d.some⟩ /-- Imported declaration from the Incompleteness formalization. -/ -@[deprecated imply₁' (since := "2026-05-27")] +@[deprecated "Use `imply₁' (ψ := ψ)`; the replacement takes ψ implicitly." (since := "2026-05-27")] def dhyp [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (ψ : F) (b : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ ==> φ := imply₁' b diff --git a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean index 8d7ef5e10c..e4cc49aed5 100644 --- a/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean +++ b/LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean @@ -30,6 +30,16 @@ import Mathlib.Topology.Metrizable.Urysohn noncomputable section +-- `instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent` applies to `F = ZMod 2` and, winning instance +-- search for `AddCommGroup F`, yields an `AddCommMonoid F` that does not match the one carried by +-- `Module F F`; that breaks `AddCommGroup (V →ₗ[F] F)` and everything built on it. +attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent + +-- Likewise `AddSubgroupClass.instZModModule` applies to any `AddSubgroupClass` of a `ZMod n`-module +-- and would take precedence over `Submodule.module` for `↥B`, whose `Module F ↥B` is the one the +-- `Module.Free`/`Module.Projective` instances are stated for. +attribute [local instance low] AddSubgroupClass.instZModModule + namespace ConnesRigidity section @@ -4655,7 +4665,7 @@ private theorem quadraticRestriction_epsilon (n : ℕ) (v : V) : /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem quadraticPairing_range_le_quadraticRestriction_range (n : ℕ) : - quadraticPairing.range ≤ (quadraticRestriction n).range := by + AddMonoidHom.range (G := B) quadraticPairing ≤ (quadraticRestriction n).range := by rintro _ ⟨b, rfl⟩ rcases b with ⟨b, hb⟩ change b ∈ Submodule.span F (Set.range square) at hb @@ -4828,8 +4838,11 @@ theorem sigma_characterization (n : ℕ) (η : E n) (q : Y) : ZMod.toCircle (q (sigma n η)) = Additive.toMul η (Multiplicative.ofAdd (⟨0, q⟩ : CarryGroup n)) := by - exact pointwisePontryaginDualEquiv_apply_character B - (quadraticRestriction n η) q + have hsigma : sigma n η = + pointwisePontryaginDualEquiv B (quadraticRestriction n η) := rfl + rw [hsigma, pointwisePontryaginDualEquiv_apply_character B + (quadraticRestriction n η) q] + rfl @@ -4837,7 +4850,7 @@ theorem sigma_characterization (n : ℕ) (η : E n) (q : Y) : public theorem sigma_surjective (n : ℕ) : Function.Surjective (sigma n) := by intro b - have hb : quadraticPairing b ∈ quadraticPairing.range := ⟨b, rfl⟩ + have hb : quadraticPairing b ∈ AddMonoidHom.range (G := B) quadraticPairing := ⟨b, rfl⟩ obtain ⟨η, hη⟩ := quadraticPairing_range_le_quadraticRestriction_range n hb refine ⟨η, ?_⟩ @@ -5770,6 +5783,8 @@ private theorem splitPontryaginCharacter_apply (d : D) (z : X × Y) : private theorem splitPontryaginCharacter_injective : Function.Injective splitPontryaginCharacter := by intro d d' h + have : Module.Free F B := Module.Free.of_divisionRing F B + have : Module.Projective F B := Module.Projective.of_free apply Prod.ext · apply Module.eval_apply_injective F apply LinearMap.ext diff --git a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean index 9e30dedc75..26c787eaa6 100644 --- a/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean +++ b/LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean @@ -21,6 +21,11 @@ import LeanPool.InfiniteConnesRigidity.GroupConstruction noncomputable section +-- `instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent` applies to `F = ZMod 2` and, winning instance +-- search for `AddCommGroup F`, yields an `AddCommMonoid F` that does not match the one carried by +-- `Module F F`; that breaks `AddCommGroup (X × Y)` and everything built on it. +attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent + namespace ConnesRigidity section @@ -517,7 +522,7 @@ private noncomputable def shiftedQuotientToKernelEquiv rw [hshift, ← LinearMap.range_toAddSubgroup, shiftVector_range] let e : ShiftedQuotient n ≃+ (V ⧸ D.shift.range) := QuotientAddGroup.congr (shiftedSubmodule n).toAddSubgroup D.shift.range - (AddEquiv.refl V) (by simpa only [AddEquiv.coe_addMonoidHom_refl, + (AddEquiv.refl V) (by simpa only [AddEquiv.toAddMonoidHom_refl, AddSubgroup.map_id] using hrange.symm) exact e.trans D.quotientIotaKernelEquiv @@ -621,11 +626,12 @@ private theorem mulEquiv_map_torsionSquareGenerated (e : G ≃* H) : · rintro ⟨x, hx, rfl⟩ rcases hx with ⟨z, hz, rfl⟩ exact ⟨e z, e.toMonoidHom.isOfFinOrder hz, by simp only [MulEquiv.toMonoidHom_eq_coe, - MonoidHom.coe_coe, map_pow]⟩ + MonoidHom.coe_ofClass, map_pow]⟩ · rintro ⟨z, hz, rfl⟩ refine ⟨(e.symm z) ^ (2 : ℕ), ?_, ?_⟩ · exact ⟨e.symm z, e.symm.toMonoidHom.isOfFinOrder hz, rfl⟩ - · simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, map_pow, MulEquiv.apply_symm_apply] + · simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, map_pow, + MulEquiv.apply_symm_apply] /-- Cross-module support for the infinite Connes-rigidity construction. -/ private theorem involutionGenerated_characteristic (G : Type u) [Group G] : diff --git a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean index 26544070d0..86b7d70bcb 100644 --- a/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean +++ b/LeanPool/InfiniteConnesRigidity/GroupConstruction.lean @@ -24,6 +24,11 @@ public import LeanPool.InfiniteConnesRigidity.SpectralAndPropertyT noncomputable section +-- `instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent` applies to `F = ZMod 2` and, winning instance +-- search for `AddCommGroup F`, yields an `AddCommMonoid F` that does not match the one carried by +-- `Module F F`; that breaks `AddCommGroup (X × Y)` and everything built on it. +attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent + namespace ConnesRigidity section diff --git a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean index 2e230d9c2d..52aed8891c 100644 --- a/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean +++ b/LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean @@ -29,6 +29,11 @@ import Mathlib.Topology.Algebra.LinearMapCompletion noncomputable section +-- `instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent` applies to `F = ZMod 2` and, winning instance +-- search for `AddCommGroup F`, yields an `AddCommMonoid F` that does not match the one carried by +-- `Module F F`; that breaks `AddCommGroup (X × Y)` and everything built on it. +attribute [local instance low] instAddCommGroupOfIsSimpleAddGroupOfIsNilpotent + namespace ConnesRigidity section diff --git a/LeanPool/JacobianDiffgeo/CanonicalForms/Existence.lean b/LeanPool/JacobianDiffgeo/CanonicalForms/Existence.lean index 8080f170e3..0f6fe9916a 100644 --- a/LeanPool/JacobianDiffgeo/CanonicalForms/Existence.lean +++ b/LeanPool/JacobianDiffgeo/CanonicalForms/Existence.lean @@ -225,7 +225,7 @@ theorem exists_nonconstant_mero : ∃ f : ℳ X, ∀ c : ℂ, f ≠ algebraMap rw [heq] rw [hl0] at hleq omega - obtain ⟨f, hfD, hf0⟩ := SetLike.exists_of_lt (lt_of_le_of_ne hle hne) + obtain ⟨f, hfD, hf0⟩ := IsConcreteLE.exists_of_lt (lt_of_le_of_ne hle hne) rw [linSys_zero_eq_span_one] at hf0 refine ⟨f, fun c hc => hf0 ?_⟩ rw [hc, Algebra.algebraMap_eq_smul_one] diff --git a/LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean b/LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean index b7ab58180d..6af3aed4a6 100644 --- a/LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean +++ b/LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean @@ -28,7 +28,7 @@ note). Assembles the two already-built halves: connected, hence has vanishing holomorphic 1-forms). * **Forward** (`genus X = 0 ⇒ X ≃ₜ S²`): riemann-roch's `riemann_inequality` at `D := single P 1` under `genus X = 0` forces `l(single P 1) ≥ 2 > 1 = l(0)`, so `L(0) = span{1}` is a PROPER - subspace of `L(single P 1)` (`SetLike.exists_of_lt`, the `CanonicalForms/Existence.lean` + subspace of `L(single P 1)` (`IsConcreteLE.exists_of_lt`, the `CanonicalForms/Existence.lean` pattern) — any witness `φ` outside `L(0)` has `φ.ord ≥ -1` at `P`, `φ.ord ≥ 0` elsewhere (`mem_linSys_iff`), and `φ.ord P < 0` (else `φ` would be holomorphic everywhere, hence in `L(0) = span{1}` by `linSys_zero_eq_span_one`, contradiction); combined with `φ.ord P ≥ -1` this @@ -78,7 +78,7 @@ theorem exists_simple_pole_of_genus_eq_zero (hg : genus X = 0) : rw [heq] rw [hl0] at hleq omega - obtain ⟨φ, hφD, hφ0⟩ := SetLike.exists_of_lt (lt_of_le_of_ne hle hne) + obtain ⟨φ, hφD, hφ0⟩ := IsConcreteLE.exists_of_lt (lt_of_le_of_ne hle hne) rw [RS.linSys_zero_eq_span_one] at hφ0 have hreg0 : ∀ x, x ≠ P → 0 ≤ φ.ord x := by intro x hx diff --git a/LeanPool/JacobianDiffgeo/JacobianConstruction/Basic.lean b/LeanPool/JacobianDiffgeo/JacobianConstruction/Basic.lean index ed751ea2f7..fb97fa7351 100644 --- a/LeanPool/JacobianDiffgeo/JacobianConstruction/Basic.lean +++ b/LeanPool/JacobianDiffgeo/JacobianConstruction/Basic.lean @@ -110,7 +110,7 @@ example (h : genus X = 0) : Subsingleton (Jacobian X) := by (fun z => ULift.up (QuotientAddGroup.mk z) : (Fin (genus X) → ℂ) → Jacobian X) := by intro q obtain ⟨z, hz⟩ := QuotientAddGroup.mk_surjective q.down - exact ⟨z, ULift.ext _ _ hz⟩ + exact ⟨z, ULift.ext hz⟩ exact hsurj.subsingleton /-! ### Gated instances (§4–§6): hooks for period-lattice-rank -/ diff --git a/LeanPool/KaltonRoberts/Recombination.lean b/LeanPool/KaltonRoberts/Recombination.lean index 79a1730fae..262239e305 100644 --- a/LeanPool/KaltonRoberts/Recombination.lean +++ b/LeanPool/KaltonRoberts/Recombination.lean @@ -320,9 +320,18 @@ lemma targetSet_freq_source_count_bound (b := (Finset.image (fun v : sourceVertices C i => perItemMatch edge C threshold hexp hfreq i v) Finset.univ).card) (Finset.card_le_card ?_) ?_ - · intro w hw; simp_all +decide [ targetSet ]; - obtain ⟨ a, b, hw ⟩ := hw; split_ifs at hw <;> simp_all +decide [ edgePiece ]; - grind +suggestions; + · intro w hw + simp only [Finset.mem_filter, Finset.mem_univ, true_and, targetSet, + Finset.mem_biUnion] at hw + obtain ⟨⟨a, e⟩, -, hw⟩ := hw + split_ifs at hw with hedge + · simp only [edgePiece, Finset.mem_filter] at hw + obtain ⟨-, hi, hlabel⟩ := hw + refine Finset.mem_image.mpr + ⟨⟨a, Finset.mem_filter.mpr ⟨Finset.mem_univ a, hi⟩⟩, Finset.mem_univ _, ?_⟩ + rw [← assignLabel_spec edge C threshold hexp hfreq a i hi, hlabel] + exact hedge + · simp at hw · exact Finset.card_image_le.trans ( by simp +decide ) /- diff --git a/LeanPool/LeanQuantumAlg/Algorithms/BernsteinVazirani.lean b/LeanPool/LeanQuantumAlg/Algorithms/BernsteinVazirani.lean index 77bf4ddbe0..430e030866 100644 --- a/LeanPool/LeanQuantumAlg/Algorithms/BernsteinVazirani.lean +++ b/LeanPool/LeanQuantumAlg/Algorithms/BernsteinVazirani.lean @@ -103,8 +103,6 @@ theorem bit_flipBit (x : Fin (2 ^ n)) (k k' : Fin n) : change (x.val ^^^ 2 ^ k.val).testBit k'.val = (bit x k' ^^ decide (k = k')) rw [Nat.testBit_xor, Nat.testBit_two_pow] congr 1 - rw [decide_eq_decide] - exact Fin.val_inj theorem flipBit_flipBit (x : Fin (2 ^ n)) (k : Fin n) : flipBit (flipBit x k) k = x := by diff --git a/LeanPool/LeanQuantumAlg/Primitives/QKernel/Fourier.lean b/LeanPool/LeanQuantumAlg/Primitives/QKernel/Fourier.lean index 3614387ab6..883ec564ca 100644 --- a/LeanPool/LeanQuantumAlg/Primitives/QKernel/Fourier.lean +++ b/LeanPool/LeanQuantumAlg/Primitives/QKernel/Fourier.lean @@ -138,7 +138,7 @@ theorem tpVecPhase_eval (lam : Fin d → ℝ) (k : Fin N) = Complex.exp (-Complex.I * ((x k * lam m : ℝ) : ℂ)) * (V m).eval x := by rw [tpVecPhase, TrigPolynomial.eval_expMul] congr 1 - rw [freqDot_comm, freqDot_smul_single]; push_cast; ring + rw [freqDot_comm, freqDot_smul_single]; push_cast; ring_nf /-- The constructive feature component after `j` layers: an explicit `Fin d`-indexed family of trigonometric polynomials mirroring `featState`. -/ diff --git a/LeanPool/LeanQuantumAlg/Primitives/QNN/FullDLABasis.lean b/LeanPool/LeanQuantumAlg/Primitives/QNN/FullDLABasis.lean index 2d564b903b..2f91774645 100644 --- a/LeanPool/LeanQuantumAlg/Primitives/QNN/FullDLABasis.lean +++ b/LeanPool/LeanQuantumAlg/Primitives/QNN/FullDLABasis.lean @@ -94,7 +94,7 @@ local macro "hsFinish" : tactic => hsInner_sub_left, hsInner_sub_right, hsInner_single, starRingEnd_apply, rt2inv_conj, star_I_eq] all_goals - (split_ifs <;> (try (exfalso; omega)) <;> (try ring) <;> + (split_ifs <;> (try (exfalso; omega)) <;> (try (first | ring1 | ring_nf)) <;> (try (rw [rt2inv_sq]; norm_num)) <;> (try (rw [rt2inv_sq, Complex.I_sq]; norm_num))))) diff --git a/LeanPool/LeanQuantumAlg/Primitives/WalshHadamard.lean b/LeanPool/LeanQuantumAlg/Primitives/WalshHadamard.lean index 291be969e1..5d6b2a410c 100644 --- a/LeanPool/LeanQuantumAlg/Primitives/WalshHadamard.lean +++ b/LeanPool/LeanQuantumAlg/Primitives/WalshHadamard.lean @@ -149,8 +149,6 @@ theorem bit_flipBit (x : Fin (2 ^ n)) (k k' : Fin n) : change (x.val ^^^ 2 ^ k.val).testBit k'.val = (bit x k' ^^ decide (k = k')) rw [Nat.testBit_xor, Nat.testBit_two_pow] congr 1 - rw [decide_eq_decide] - exact Fin.val_inj theorem flipBit_flipBit (x : Fin (2 ^ n)) (k : Fin n) : flipBit (flipBit x k) k = x := by diff --git a/LeanPool/LocalComplexGeometry/Nullstellensatz/GenericFiber.lean b/LeanPool/LocalComplexGeometry/Nullstellensatz/GenericFiber.lean index 2d5a3d2978..310e1968d2 100644 --- a/LeanPool/LocalComplexGeometry/Nullstellensatz/GenericFiber.lean +++ b/LeanPool/LocalComplexGeometry/Nullstellensatz/GenericFiber.lean @@ -460,6 +460,9 @@ theorem genericFractionField_finiteDimensional {d : ℕ} FiniteDimensional (ContractedFractionField P) (AmbientFractionField P) := by let : Module.Finite (ContractedGermQuotient P) (AmbientGermQuotient P) := ambientQuotient_moduleFinite a ha ha0 P hmem + let : Module.IsTorsionFree (ContractedGermQuotient P) (AmbientGermQuotient P) := + Module.isTorsionFree_iff_algebraMap_injective.mpr + (contractedQuotientMap_injective P) infer_instance /-- In particular, the generic last-coordinate class is algebraic (integral, diff --git a/LeanPool/LowWeightPauliDynamics/Pauli/LayerWitness.lean b/LeanPool/LowWeightPauliDynamics/Pauli/LayerWitness.lean index c09093fe00..2323c5bb10 100644 --- a/LeanPool/LowWeightPauliDynamics/Pauli/LayerWitness.lean +++ b/LeanPool/LowWeightPauliDynamics/Pauli/LayerWitness.lean @@ -200,6 +200,28 @@ def reachable : (layers : List (List (PauliString n))) → (p : PauliString n) (p : PauliString n) : reachable (L :: Ls) p = (oneLayer L p).biUnion (reachable Ls) := rfl +/-- A string can always sit out a layer: every generator's `branch` retains its input, so `p` +itself survives the whole layer unbranched. -/ +theorem self_mem_oneLayer (L : List (PauliString n)) (p : PauliString n) : p ∈ oneLayer L p := by + induction L with + | nil => simp + | cons G Gs ih => exact Finset.mem_biUnion.2 ⟨p, self_mem_branch G p, ih⟩ + +/-- **Inserting a layer only enlarges the reachable set**, by `self_mem_oneLayer`. -/ +theorem reachable_subset_cons (L : List (PauliString n)) (Ls : List (List (PauliString n))) + (p : PauliString n) : reachable Ls p ⊆ reachable (L :: Ls) p := by + intro q hq + rw [reachable_cons] + exact Finset.mem_biUnion.2 ⟨p, self_mem_oneLayer L p, hq⟩ + +/-- Enlarging the reachable set of a suffix enlarges it for the whole sequence: the two sequences +run the same head layer and only then differ. -/ +theorem reachable_subset_reachable_cons {Ls Ls' : List (List (PauliString n))} + (h : ∀ r : PauliString n, reachable Ls r ⊆ reachable Ls' r) (L : List (PauliString n)) + (p : PauliString n) : reachable (L :: Ls) p ⊆ reachable (L :: Ls') p := by + rw [reachable_cons, reachable_cons] + exact Finset.biUnion_mono fun r _ => h r + /-- **A layer of `k_h`-local rotations with disjoint supports**: the hypothesis that `apd:thm:lightcone` places on each layer of a Trotter step. -/ structure IsLayer (kh : ℕ) (L : List (PauliString n)) : Prop where @@ -510,7 +532,12 @@ theorem P₄_mem_reachable : P₄ ∈ reachable (layers := [L₁, L₂]) (Z 3) : theorem P₆_mem_reachable : P₆ ∈ reachable (layers := [L₁, L₂, L₁]) (Z 3) := by decide -theorem P₆_mem_reachable_unmerged : P₆ ∈ reachable (layers := [L₁, L₂, L₂, L₁]) (Z 3) := by decide +/-- The literal `2Γ = 4` layer reading, obtained from the merged one by letting `P₆` sit out the +repeated `L₂`: deciding this directly would re-explore the whole four-layer branching tree. -/ +theorem P₆_mem_reachable_unmerged : P₆ ∈ reachable (layers := [L₁, L₂, L₂, L₁]) (Z 3) := + reachable_subset_reachable_cons + (reachable_subset_reachable_cons (reachable_subset_cons L₂ [L₁]) L₂) L₁ (Z 3) + P₆_mem_reachable /-- …and the bound is attained: `P₄` has weight exactly `4` and is reachable in the two brickwork layers. Together with `gamma_layers_weight_le`, the maximum reachable weight after `Γ` layers is diff --git a/LeanPool/MassFormula/First.lean b/LeanPool/MassFormula/First.lean index 9f6506c4ea..685f869835 100644 --- a/LeanPool/MassFormula/First.lean +++ b/LeanPool/MassFormula/First.lean @@ -2108,14 +2108,18 @@ private theorem uniformizer_classes_mass {π : 𝒪[K]} (hπ : Irreducible π) { coord hπ hint hei (u - v) = coord hπ hint hei u - coord hπ hint hei v := by intro u v + have h : (basisOfEisenstein hπ hint hei).equivFun (u - v) = + (basisOfEisenstein hπ hint hei).equivFun u - + (basisOfEisenstein hπ hint hei).equivFun v := + (basisOfEisenstein hπ hint hei).equivFun.toLinearMap.map_sub u v unfold coord - rw [map_sub, map_sub] + rw [h, map_sub] have hcadd : ∀ u v : ↥(integers (IntermediateField.adjoin K {x})), coord hπ hint hei (u + v) = coord hπ hint hei u + coord hπ hint hei v := by intro u v unfold coord - rw [map_add, map_add] + rw [LinearEquiv.map_add, map_add] have himg : ∀ t : ↥(integers (IntermediateField.adjoin K {x})) ⧸ I, coord hπ hint hei '' {w | Ideal.Quotient.mk I w = t} = coord hπ hint hei (rep t) +ᵥ @@ -2411,7 +2415,11 @@ theorem lintegral_rootCount (n : ℕ) (hn : 0 < n) have h2 : (basisOfEisenstein hπ hint hei).repr (rep t) i - (basisOfEisenstein hπ hint hei).repr (rep t') i ∈ Ideal.span {π ^ ρ} := Ideal.Quotient.eq.mp (congrFun htt' i) - rw [map_sub, Finsupp.sub_apply] + have hrsub : (basisOfEisenstein hπ hint hei).repr (rep t - rep t') = + (basisOfEisenstein hπ hint hei).repr (rep t) - + (basisOfEisenstein hπ hint hei).repr (rep t') := + (basisOfEisenstein hπ hint hei).repr.toLinearMap.map_sub _ _ + rw [hrsub, Finsupp.sub_apply] rwa [Ideal.mem_span_singleton, ← addVal_le_iff_dvd, hπ.addVal_pow] at h2 have h3 : rep t - rep t' ∈ I := by rw [hImem, le_addVal_mul_iff_coords hπ hint hei ρ] diff --git a/LeanPool/MetricCodes/Foundations.lean b/LeanPool/MetricCodes/Foundations.lean index 0d38f8ab6c..9d0177b01f 100644 --- a/LeanPool/MetricCodes/Foundations.lean +++ b/LeanPool/MetricCodes/Foundations.lean @@ -4168,9 +4168,8 @@ theorem hammingDist_binaryTranslate {n : ℕ} (z x y : BinaryWord n) : theorem binaryWeight_binaryTranslate {n : ℕ} (x y : BinaryWord n) : binaryWeight (binaryTranslate x y) = hammingDist x y := by unfold binaryWeight hammingDist _root_.hammingDist - congr 1 - ext i - simp only [binaryTranslate, bne_iff_ne, ne_eq, mem_filter, mem_univ, true_and] + refine congrArg Finset.card (Finset.filter_congr fun i _ => ?_) + simp only [binaryTranslate, bne_iff_ne, ne_eq] /-- The finite set of length-`n` binary words of weight `w`. -/ def weightShell (n w : ℕ) : Finset (BinaryWord n) := diff --git a/LeanPool/MetricCodes/RootComplex.lean b/LeanPool/MetricCodes/RootComplex.lean index 5ce601fca0..f2d4738df1 100644 --- a/LeanPool/MetricCodes/RootComplex.lean +++ b/LeanPool/MetricCodes/RootComplex.lean @@ -4137,7 +4137,8 @@ private def rootDegreeZeroLaplacianKernelTransport {r : ℕ} (positiveRootFischerLaplacian n lam (rootJointHarmonicDegreeZeroEquiv n lam ((rootJointHarmonicDegreeZeroEquiv n lam).symm p.val))) = 0 - simp only [LinearEquiv.apply_symm_apply, LinearMap.map_coe_ker, map_zero] + rw [LinearEquiv.apply_symm_apply, LinearMap.map_coe_ker] + exact (rootJointHarmonicDegreeZeroEquiv n lam).symm.map_zero left_inv p := by apply Subtype.ext exact (rootJointHarmonicDegreeZeroEquiv n lam).left_inv p.val diff --git a/LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean b/LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean index 88a6072351..480ad0e947 100644 --- a/LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean +++ b/LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean @@ -79,7 +79,7 @@ theorem IsIdempotentElem.comp_idempotent_iff {E₂ : Type*} [AddCommGroup E₂] [Module R E₂] (p : E₂ →ₗ[R] E) : q.comp p = p ↔ LinearMap.range p ≤ LinearMap.range q := by simp_rw [LinearMap.ext_iff, comp_apply, ← IsIdempotentElem.mem_range_iff hq, - SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] + IsConcreteLE.le_iff, mem_range, forall_exists_index, forall_apply_eq_imp_iff] include hq in theorem IsIdempotentElem.comp_idempotent_iff' {E₂ : Type*} [AddCommGroup E₂] [Module R E₂] (p : E₂ →ₗ[R] E) : diff --git a/LeanPool/Monsky/SegmentTriangle.lean b/LeanPool/Monsky/SegmentTriangle.lean index 892c8cc26b..ef5fe153f1 100644 --- a/LeanPool/Monsky/SegmentTriangle.lean +++ b/LeanPool/Monsky/SegmentTriangle.lean @@ -1342,8 +1342,7 @@ lemma colin_sub {u v w : ℝ²} (h : colin u v w) {L : Segment} have hxl : ∃ x, x ∈ openHull L := open_pol_nonempty (by linarith) L rcases hxl with ⟨x, hx⟩ by_cases hxl' : x ∈ closedHull (toSegment u v) - constructor - · exact (colin_sub_aux h hLsub hLv hx hxl') + · exact Or.inl (colin_sub_aux h hLsub hLv hx hxl') have hLsubrev : closedHull L ⊆ closedHull (toSegment w u) := by rw [← reverseSegment_toSegment, reverseSegment_closedHull] exact hLsub diff --git a/LeanPool/MooreBound/DegreeDiameter/CommonBasis.lean b/LeanPool/MooreBound/DegreeDiameter/CommonBasis.lean index f415ea4010..890bde3853 100644 --- a/LeanPool/MooreBound/DegreeDiameter/CommonBasis.lean +++ b/LeanPool/MooreBound/DegreeDiameter/CommonBasis.lean @@ -254,7 +254,7 @@ theorem common_apartment {n : ℕ} (F F' : CompleteFlag K V n) : have hP : ∀ i, ∃ j, P i j := by intro i obtain ⟨x, hxi, hxni⟩ := - SetLike.exists_of_lt (F.strictMono_space Fin.castSucc_lt_succ) + IsConcreteLE.exists_of_lt (F.strictMono_space Fin.castSucc_lt_succ) refine ⟨Fin.last m, x, hxi, ?_, hxni⟩ rw [show (Fin.last m).succ = Fin.last (m + 1) by ext diff --git a/LeanPool/NonSoficGroup/Compression.lean b/LeanPool/NonSoficGroup/Compression.lean index a622d450a4..0a87203d8e 100644 --- a/LeanPool/NonSoficGroup/Compression.lean +++ b/LeanPool/NonSoficGroup/Compression.lean @@ -3589,7 +3589,7 @@ private def sourceConjugatedAlphaUElement apply alphaZero_prefixElementaryGroup_le rw [← compressionU_map_alphaPrefixElementaryGroup] refine ⟨g.val, g.property, ?_⟩ - simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conj_apply] + simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply] private def sourceConjugatedAlphaVElement (g : prefixElementaryGroup alphaPrefixCode) : @@ -3599,7 +3599,7 @@ private def sourceConjugatedAlphaVElement apply alphaZero_prefixElementaryGroup_le rw [← compressionV_map_alphaPrefixElementaryGroup] refine ⟨g.val, g.property, ?_⟩ - simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conj_apply] + simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply] private theorem sourceCompressionUElement_conjugates_alpha (g : prefixElementaryGroup alphaPrefixCode) : diff --git a/LeanPool/NonSoficGroup/Foundations.lean b/LeanPool/NonSoficGroup/Foundations.lean index dd142cdef4..9d80fbba0e 100644 --- a/LeanPool/NonSoficGroup/Foundations.lean +++ b/LeanPool/NonSoficGroup/Foundations.lean @@ -2943,8 +2943,7 @@ private theorem elementaryGroup_finitelyGenerated rintro _ ⟨i, j, hij, a, rfl⟩ have ha : a ∈ C := by simp only [hC, Algebra.mem_top] exact ha i j hij - apply (Group.fg_iff_subgroup_fg (elementaryGroup (Fin n) R)).mpr - exact ⟨t, heq⟩ + exact Subgroup.isMulFG_iff.mpr ⟨t, heq⟩ private theorem elementaryGroup_three_finitelyGenerated [Algebra.FiniteType (ZMod 2) R] : @@ -9725,7 +9724,7 @@ private theorem elementaryReindexGroup_map (e : ι ≃ κ) : have hij : e.symm k ≠ e.symm l := e.symm.injective.ne hkl refine ⟨elementaryUnit (e.symm k) (e.symm l) hij a, elementaryUnit_mem (e.symm k) (e.symm l) hij a, ?_⟩ - simpa only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, Equiv.apply_symm_apply] using + simpa only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, Equiv.apply_symm_apply] using elementaryReindexUnitEquiv_elementaryUnit e (e.symm k) (e.symm l) hij a /-- Internal interface connecting the split non-sofic proof modules. -/ diff --git a/LeanPool/NonSoficGroup/Spectral.lean b/LeanPool/NonSoficGroup/Spectral.lean index c39483cd7a..cab70580ea 100644 --- a/LeanPool/NonSoficGroup/Spectral.lean +++ b/LeanPool/NonSoficGroup/Spectral.lean @@ -2309,8 +2309,8 @@ private theorem heisenbergFiniteFamily_centerComplement_inner_sq_le rw [mem_unitaryFixedSubmodule] rintro ⟨_, ⟨g, hg, rfl⟩⟩ have hga := (mem_unitaryFixedSubmodule π X a).mp ha ⟨g, hg⟩ - simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conj_apply, map_mul, map_inv, - LinearIsometryEquiv.coe_mul, LinearIsometryEquiv.coe_inv, Function.comp_apply, + simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply, map_mul, + map_inv, LinearIsometryEquiv.coe_mul, LinearIsometryEquiv.coe_inv, Function.comp_apply, LinearIsometryEquiv.symm_apply_apply, hga] have horthZ (i : ι) : diff --git a/LeanPool/OrderPQ/PrimeOrder.lean b/LeanPool/OrderPQ/PrimeOrder.lean index 3eb4ff0000..7c14843351 100644 --- a/LeanPool/OrderPQ/PrimeOrder.lean +++ b/LeanPool/OrderPQ/PrimeOrder.lean @@ -30,13 +30,13 @@ variable {G : Type*} [Group G] [IsSimpleGroup G] @[to_additive] lemma ne_bot_iff_eq_top_of_normal {H : Subgroup G} (h : H.Normal) : H ≠ ⊤ ↔ H = ⊥ := by - exact ne_iff_eq_of_or_and_ne (eq_bot_or_eq_top_of_normal H h).symm bot_ne_top.symm + exact ne_iff_eq_of_or_and_ne h.eq_bot_or_eq_top.symm bot_ne_top.symm @[to_additive] lemma monoidHom_injective_or_eq_one {H : Type*} [Group H] (φ : G →* H) : Function.Injective φ ∨ φ = 1 := by rw [← MonoidHom.ker_eq_bot_iff φ, ← MonoidHom.ker_eq_top_iff (f := φ)] - exact eq_bot_or_eq_top_of_normal φ.ker φ.normal_ker + exact φ.normal_ker.eq_bot_or_eq_top @[to_additive] lemma monoidHom_ne_one_iff_injective {H : Type*} [Group H] (φ : G →* H) : diff --git a/LeanPool/PDL/Soundness.lean b/LeanPool/PDL/Soundness.lean index d72a225427..1ea12b0138 100644 --- a/LeanPool/PDL/Soundness.lean +++ b/LeanPool/PDL/Soundness.lean @@ -816,7 +816,7 @@ private theorem loadedDiamondPathsPDL_modL (α : Program) (X : Sequent) (tab : T refine ⟨s, ?_, Or.inr ?_⟩ -- ... it is then obvious that `s` satisfies the required properties: · apply Relation.TransGen.single - constructor + apply Or.inl right refine ⟨Hist, _, nflprep, bas, _, (.modL Z_def rfl), next, tabAt_t_def, ?_⟩ simp only [s, t_to_s] @@ -966,7 +966,7 @@ private theorem loadedDiamondPathsPDL_modR (α : Program) (X : Sequent) (tab : T refine ⟨s, ?_, Or.inr ?_⟩ -- ... it is then obvious that `s` satisfies the required properties: · apply Relation.TransGen.single - constructor + apply Or.inl right refine ⟨Hist, _, nflprep, bas, _, (PdlRule.modR Z_def rfl), next, tabAt_t_def, ?_⟩ simp only [s, t_to_s] diff --git a/LeanPool/PartialCombinatoryAlgebras/GraphModel.lean b/LeanPool/PartialCombinatoryAlgebras/GraphModel.lean index 430692e62f..908ed73af8 100644 --- a/LeanPool/PartialCombinatoryAlgebras/GraphModel.lean +++ b/LeanPool/PartialCombinatoryAlgebras/GraphModel.lean @@ -154,7 +154,7 @@ theorem continuous_id : continuous (@id (Set α)) := by simp only [Membership.mem, Set.Mem] rintro (H | ⟨A, ⟨⟩⟩); assumption · rw [eq_toSet_fromList] - constructor + apply List.Mem.head case mpr => rintro ⟨y, yS, xy⟩ exact yS xy @@ -305,7 +305,7 @@ theorem continuous_snd (S : Set α) : continuous (fun T => apply T S) := by · use y constructor · assumption - · rw [eq_toSet_fromList]; constructor + · rw [eq_toSet_fromList]; apply List.Mem.head · rintro ⟨y, yT, z, zS, xyz⟩ exact ⟨z, zS, yT xyz⟩ diff --git a/LeanPool/PumpingCfg/ChomskyNormalForm/EmptyElimination.lean b/LeanPool/PumpingCfg/ChomskyNormalForm/EmptyElimination.lean index f673d423eb..8e0c54f8dd 100644 --- a/LeanPool/PumpingCfg/ChomskyNormalForm/EmptyElimination.lean +++ b/LeanPool/PumpingCfg/ChomskyNormalForm/EmptyElimination.lean @@ -276,7 +276,10 @@ inductive NullableRelated : List (Symbol T g.NT) → List (Symbol T g.NT) → Pr lemma NullableRelated.refl (u : List (Symbol T g.NT)) : NullableRelated u u := by induction u with | nil => exact empty_left [] (by rfl) - | cons d _ ih => cases d <;> constructor <;> exact ih + | cons d _ ih => + cases d with + | terminal t => exact cons_term ih t + | nonterminal n => exact cons_nterm_match ih n lemma NullableRelated.derives {u v : List (Symbol T g.NT)} (huv : NullableRelated u v) : g.Derives v u := by diff --git a/LeanPool/PumpingCfg/ChomskyNormalForm/Translation.lean b/LeanPool/PumpingCfg/ChomskyNormalForm/Translation.lean index e0f0f32345..7f6f258f50 100644 --- a/LeanPool/PumpingCfg/ChomskyNormalForm/Translation.lean +++ b/LeanPool/PumpingCfg/ChomskyNormalForm/Translation.lean @@ -187,7 +187,7 @@ theorem toCNF_correct : g.language \ {[]} = g.toCNF.language := by (eliminateUnitRules_not_empty_output eliminateEmpty_not_empty_output) _ hrg hrₒ | [Symbol.terminal _] => cases r; simp only at hrₒ; rw [hrₒ] - constructor + apply ContextFreeRule.Wellformed.terminal | [Symbol.nonterminal _] => exfalso apply restrictTerminals_nonUnit_output at hrg diff --git a/LeanPool/PumpingCfg/ChomskyNormalForm/UnitElimination.lean b/LeanPool/PumpingCfg/ChomskyNormalForm/UnitElimination.lean index 1dd8db5f6a..d0a701e23e 100644 --- a/LeanPool/PumpingCfg/ChomskyNormalForm/UnitElimination.lean +++ b/LeanPool/PumpingCfg/ChomskyNormalForm/UnitElimination.lean @@ -144,14 +144,14 @@ lemma generatorsProdDiag_unitPairs {p : g.NT × g.NT} (hp : p ∈ g.generatorsPr | inl hpr => rw [hpr] change UnitPair r.input r.input - constructor + apply UnitPair.refl apply input_mem_generators rw [← Finset.mem_toList, heq] exact List.mem_cons_self | inr hap => obtain ⟨v, hvl, hvp⟩ := hap rw [← hvp] - constructor + apply UnitPair.refl apply input_mem_generators rw [← Finset.mem_toList, heq] exact List.mem_cons_of_mem r hvl diff --git a/LeanPool/QuadraticIterates/ArchMath1992/Iterates.lean b/LeanPool/QuadraticIterates/ArchMath1992/Iterates.lean index 5002b611b5..0e88591aa3 100644 --- a/LeanPool/QuadraticIterates/ArchMath1992/Iterates.lean +++ b/LeanPool/QuadraticIterates/ArchMath1992/Iterates.lean @@ -412,9 +412,9 @@ theorem relfinrank_succ_eq_finrank_adjoin (n : ℕ) (g : AlgebraicClosure ℚ rw [hg (β ^ 2 + (a : AlgebraicClosure ℚ)), add_sub_cancel_right] rcases sq_eq_sq_iff_eq_or_eq_neg.mp hsq with h | h · rw [h] - exact SetLike.le_def.mp le_sup_right hgmem + exact IsConcreteLE.le_iff.mp le_sup_right hgmem · rw [h] - exact neg_mem (SetLike.le_def.mp le_sup_right hgmem) + exact neg_mem (IsConcreteLE.le_iff.mp le_sup_right hgmem) · refine IntermediateField.adjoin_le_iff.mpr ?_ rintro x ⟨α, hα, rfl⟩ exact IntermediateField.subset_adjoin ℚ _ diff --git a/LeanPool/QuadraticIterates/Mathlib/RingTheory/MoebiusFactor.lean b/LeanPool/QuadraticIterates/Mathlib/RingTheory/MoebiusFactor.lean index 5d005f971e..bf4a2892fb 100644 --- a/LeanPool/QuadraticIterates/Mathlib/RingTheory/MoebiusFactor.lean +++ b/LeanPool/QuadraticIterates/Mathlib/RingTheory/MoebiusFactor.lean @@ -341,7 +341,9 @@ theorem moebiusFactorR_isRelPrime {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) 1 ≤ factorization (moebiusFactorR c k) p := by have h1 : (1 : ℕ∞) ≤ emultiplicity q (moebiusFactorR c k) := by rw [← pow_one q] at hdvd - exact pow_dvd_iff_le_emultiplicity.mp (by rwa [pow_one] at hdvd ⊢) |>.trans_eq rfl + exact pow_dvd_iff_le_emultiplicity.mp (by + rw [pow_one] at hdvd ⊢ + assumption) |>.trans_eq rfl rw [emultiplicity_eq_count_normalizedFactors hq.irreducible (moebiusFactorR_ne_zero hc hsd k hk)] at h1 rw [factorization_eq_count] diff --git a/LeanPool/RiemannRochFunctionFields/EllipticCurve/Instances.lean b/LeanPool/RiemannRochFunctionFields/EllipticCurve/Instances.lean index 2d3dc600aa..59764612c8 100644 --- a/LeanPool/RiemannRochFunctionFields/EllipticCurve/Instances.lean +++ b/LeanPool/RiemannRochFunctionFields/EllipticCurve/Instances.lean @@ -250,6 +250,8 @@ theorem isSeparable [W.IsElliptic] : Algebra.IsSeparable k⟮X⟯ K := by · simp only [SetLike.mem_coe, Subalgebra.mem_toSubmodule, basisRatFunc_one] exact IntermediateField.mem_adjoin_simple_self k⟮X⟯ (W.yCoord K) exact hle hz + let : Algebra k⟮X⟯ (IntermediateField.adjoin k⟮X⟯ {W.yCoord K}) := + IntermediateField.algebra' _ have : Algebra.IsSeparable k⟮X⟯ (IntermediateField.adjoin k⟮X⟯ {W.yCoord K}) := (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable k⟮X⟯ K).mpr hsep let : Algebra k⟮X⟯ (⊤ : IntermediateField k⟮X⟯ K) := IntermediateField.algebra' ⊤ diff --git a/LeanPool/RiemannRochFunctionFields/Place.lean b/LeanPool/RiemannRochFunctionFields/Place.lean index d674abc203..135f71ebae 100644 --- a/LeanPool/RiemannRochFunctionFields/Place.lean +++ b/LeanPool/RiemannRochFunctionFields/Place.lean @@ -245,14 +245,15 @@ noncomputable def normalization (v : Place k K) : /-- The normalized `ℤᵐ⁰`-valued valuation associated to a coordinate-free place. -/ noncomputable def valuation (v : Place k K) : Valuation K ℤᵐ⁰ := v.toValuationSubring.valuation.restrict.map - v.normalization.toMonoidWithZeroHom v.normalization.toOrderIso.monotone + (OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom v.normalization) /-- The normalized valuation is equivalent to the canonical valuation of the valuation subring. -/ theorem valuation_isEquiv_canonical (v : Place k K) : v.valuation.IsEquiv v.toValuationSubring.valuation := by exact (Valuation.isEquiv_map_self_of_strictMono - v.normalization.toMonoidWithZeroHom v.normalization.strictMono).trans + (OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom v.normalization) + v.normalization.injective).trans v.toValuationSubring.valuation.isEquiv_restrict.symm /-- Recovering the valuation subring from the normalized valuation gives the original place. -/ diff --git a/LeanPool/RiemannRochFunctionFields/PlaceEquiv.lean b/LeanPool/RiemannRochFunctionFields/PlaceEquiv.lean index 11d8bb7d15..c40f2ec47a 100644 --- a/LeanPool/RiemannRochFunctionFields/PlaceEquiv.lean +++ b/LeanPool/RiemannRochFunctionFields/PlaceEquiv.lean @@ -378,10 +378,10 @@ theorem infinite_X_gt_one (A := A) (K := k⟮X⟯)).symm.trans hmap have hbaseX : 1 < u.valuation k⟮X⟯ RatFunc.X := hbase.one_lt_iff_one_lt.mpr (by simp [← WithZero.exp_zero]) - have he : u.asIdeal.ramificationIdx' w.asIdeal ≠ 0 := - Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver w.asIdeal u.ne_bot + have he : w.asIdeal.ramificationIdx A ≠ 0 := + (Ideal.ramificationIdx_pos_of_isDedekindDomain' w.asIdeal u.ne_bot).ne' have hpow : 1 < (u.valuation k⟮X⟯ RatFunc.X) ^ - u.asIdeal.ramificationIdx' w.asIdeal := by + w.asIdeal.ramificationIdx A := by exact one_lt_pow₀ hbaseX he rw [u.valuation_liesOver K w RatFunc.X] at hpow exact hpow diff --git a/LeanPool/SetTheory/Basic.lean b/LeanPool/SetTheory/Basic.lean index fd2a9ede95..583c484c05 100644 --- a/LeanPool/SetTheory/Basic.lean +++ b/LeanPool/SetTheory/Basic.lean @@ -269,14 +269,14 @@ instance instSetLike : SetLike M M where simp only [Set.ext_iff, Set.mem_ofPred_eq] at eq exact ext eq -instance instPartialOrderM : PartialOrder M := PartialOrder.ofSetLike M M +instance instPartialOrderM : PartialOrder M := PartialOrder.ofSetLike M lemma le_def {x y : M} : x ≤ y ↔ x ⊆ y := Iff.rfl lemma le_iff {x y : M} : x ≤ y ↔ ∀ ⦃z : M⦄, z ∈ x → z ∈ y := Iff.rfl lemma mem_of_le {x y z : M} (hsub : x ≤ y) (hz : z ∈ x) : z ∈ y := hsub hz lemma mem_coe {x y : M} : x ∈ (y : Set M) ↔ x ∈ y := SetLike.mem_coe lemma lt_iff_le_and_exists {x y : M} : x < y ↔ x ≤ y ∧ ∃ z ∈ y, z ∉ x := - SetLike.lt_iff_le_and_exists + IsConcreteLE.lt_iff_le_and_exists @[toZFSet_simps] lemma ToZFSet.le (x y : M) : x ≤ y ↔ ⇓x ≤ ⇓y := by change x ⊆ y ↔ ⇓x ⊆ ⇓y diff --git a/LeanPool/UlmsTheorem/Ulm/Extension.lean b/LeanPool/UlmsTheorem/Ulm/Extension.lean index 7a225b3098..78d560db4a 100644 --- a/LeanPool/UlmsTheorem/Ulm/Extension.lean +++ b/LeanPool/UlmsTheorem/Ulm/Extension.lean @@ -374,7 +374,7 @@ theorem relativeUlmQuotient_nontrivial_iff_proper · intro hroom rw [Submodule.Quotient.nontrivial_iff] at hroom obtain ⟨v, _, hv⟩ := - SetLike.exists_of_lt (lt_top_iff_ne_top.mpr hroom) + IsConcreteLE.exists_of_lt (lt_top_iff_ne_top.mpr hroom) have hv' : (v : G) ∉ pSocleAt p α ⊓ (S ⊔ ulmSubgroup p (Order.succ α)) := by exact hv diff --git a/LeanPool/ZFLean/Integers.lean b/LeanPool/ZFLean/Integers.lean index 8c0b943f91..596e645dcf 100644 --- a/LeanPool/ZFLean/Integers.lean +++ b/LeanPool/ZFLean/Integers.lean @@ -1163,31 +1163,13 @@ instance : Coe ZFInt {x // x ∈ Int} := ⟨instEquivZFIntInt.toFun⟩ instance : Coe {x // x ∈ Int} ZFInt := ⟨instEquivZFIntInt.invFun⟩ theorem _root_.ZFSet.instEquivZFIntInt.mono_iff (x y : { x // x ∈ Int.{u} }) : instEquivZFIntInt.{u}.invFun x < instEquivZFIntInt.{u}.invFun y ↔ x < y := by - constructor - · intro h - dsimp [instEquivZFIntInt] at h - split at h - rename_i f' f bij mono eq; clear f' eq - unfold Equiv.ofBijective at h - dsimp at h - have := mono.1 - (Function.surjInv (Function.Bijective.surjective bij) x) - (Function.surjInv (Function.Bijective.surjective bij) y) |>.mpr h - iterate 2 rw [Function.rightInverse_surjInv (Function.Bijective.surjective bij)] at this - exact this - · intro h - dsimp [instEquivZFIntInt] - split - rename_i f' f bij mono eq; clear f' eq - let f' := Function.surjInv (Function.Bijective.surjective bij) - have mono' : ∀ x y, f' x < f' y ↔ x < y := by - intro x y - have := mono.1 (f' x) (f' y) - iterate 2 rw [Function.rightInverse_surjInv (Function.Bijective.surjective bij)] at this - exact this.symm - unfold Equiv.ofBijective - dsimp - exact mono' x y |>.mpr h + have mono : ∀ a b : ZFInt.{u}, instEquivZFIntInt.{u} a < instEquivZFIntInt.{u} b ↔ a < b := + (Classical.choice ZFInt.exists_mono_bij_zero_eq.{u}).2.2.1 + have hx : instEquivZFIntInt.{u} (instEquivZFIntInt.{u}.invFun x) = x := + instEquivZFIntInt.{u}.apply_symm_apply x + have hy : instEquivZFIntInt.{u} (instEquivZFIntInt.{u}.invFun y) = y := + instEquivZFIntInt.{u}.apply_symm_apply y + rw [← mono (instEquivZFIntInt.{u}.invFun x) (instEquivZFIntInt.{u}.invFun y), hx, hy] instance : Preorder {x // x ∈ Int} where le x y := ZFInt.instPartialOrder.le x y le_refl x := ZFInt.instLinearOrder.le_refl x diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index dc8a286ee9..b60d80a26a 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -1,14 +1,14 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": "../.lake/packages", "packages": [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "a6521b2d0c93dcdf2d640089f95548df5dd8bf46", + "rev": "20b0edcaf3d2882fe2c906158e79f2f5dbebe57c", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0", + "inputRev": "v4.35.0-rc3", "inherited": false, "configFile": "lakefile.lean"}, {"type": "path", @@ -17,12 +17,13 @@ "manifestFile": "lake-manifest.json", "inherited": false, "dir": "../", + "copy": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/leansqlite", "type": "git", "subDir": null, "scope": "", - "rev": "f9cdb9eacb5c8b8ecc02ee9fd9e568d7d28c1416", + "rev": "b4714b301b682bb7aecb4eefe255fb49b02d11d8", "name": "leansqlite", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -32,7 +33,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -42,7 +43,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0e569d08b6443ce0908d356884c765397253e2f0", + "rev": "a0470ae2c2b2c2dabd42f87b8880c9e81ad8172b", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -52,7 +53,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4d8616fd4870d0a3453d845770833eac7951fe1c", + "rev": "fdcc88de7c4c5a11e3239c9416615f34c226d47d", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -72,17 +73,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ed2965256430c3649e86755f9576b54eca72435", + "rev": "c55e6e786f49471c72fbddbec5415808896aec1e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0", + "inputRev": "v4.35.0-rc3", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -92,7 +93,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -102,7 +103,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e928b72544873815af278d38681b31c0293588e3", + "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -112,7 +113,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -122,7 +123,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -132,7 +133,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -142,7 +143,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "rev": "3b7c8101932390d60e92a3f3d917901d5b5a773b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index 6c380253ff..2ee0bea710 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -10,4 +10,4 @@ path = "../" [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.34.0" +rev = "v4.35.0-rc3" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index 12359f928f..f0e00b3338 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.35.0-rc3 diff --git a/lake-manifest.json b/lake-manifest.json index 557f9186bf..574e50e3ab 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ed2965256430c3649e86755f9576b54eca72435", + "rev": "c55e6e786f49471c72fbddbec5415808896aec1e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0", + "inputRev": "v4.35.0-rc3", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e928b72544873815af278d38681b31c0293588e3", + "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "rev": "3b7c8101932390d60e92a3f3d917901d5b5a773b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0", + "inputRev": "v4.35.0-rc3", "inherited": true, "configFile": "lakefile.toml"}], "name": "«lean-pool»", diff --git a/lakefile.toml b/lakefile.toml index c020c09100..5d42a2eff4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,7 +13,7 @@ maxSynthPendingDepth = 3 [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.34.0" +rev = "v4.35.0-rc3" [[lean_lib]] name = "LeanPool" diff --git a/lean-toolchain b/lean-toolchain index 12359f928f..f0e00b3338 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.35.0-rc3 diff --git a/scripts/challenge/pins.env b/scripts/challenge/pins.env index ae04cfab1d..7e8177cca0 100644 --- a/scripts/challenge/pins.env +++ b/scripts/challenge/pins.env @@ -14,7 +14,7 @@ LANDRUN_COMMIT=5ed4a3db3a4ad930d577215c6b9abaa19df7f99f # lean4export must match this repository's lean-toolchain: it reads the oleans # our build produced. The workflow asserts that, and prints the right SHA. -# This is refs/tags/v4.34.0, matching this branch's toolchain. -LEAN4EXPORT_COMMIT=076e8e57707e813375e8f9da8bf989799ace9680 +# This is refs/tags/v4.35.0-rc3, matching this branch's toolchain. +LEAN4EXPORT_COMMIT=66f1fb4bc256072069767fce52d39480e4524869 COMPARATOR_COMMIT=71b52ec29e06d4b7d882726553b1ceb99a2499e0