From 932a58b04d345d516adb54545493f5b3a59d0f33 Mon Sep 17 00:00:00 2001 From: "mathlib-update-dependencies[bot]" <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Date: Sat, 1 Aug 2026 07:42:51 +0000 Subject: [PATCH 01/12] chore: update Mathlib dependencies 2026-08-01 (#42268) This PR updates the Mathlib dependencies. --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 3ac6d313b0..e8e2d9aa79 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ae82a25d0eb1259a7044d6b77adb21475ff13233", + "rev": "2963c249dabd57512a2e101901777e381eb40350", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 40cb31be4a51505f4a25060b8e0c775dcb537dac Mon Sep 17 00:00:00 2001 From: Artie Khovanov <17950993+artie2000@users.noreply.github.com> Date: Sat, 1 Aug 2026 08:36:57 +0000 Subject: [PATCH 02/12] feat(LinearAlgebra/Dimension/Free): division version of tower law (#41488) Split from #37959 Co-authored-by: artie2000 --- .../IntermediateField/Algebraic.lean | 4 ++-- Mathlib/LinearAlgebra/Dimension/Free.lean | 24 +++++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean index 8978537153..fecdb84e63 100644 --- a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean +++ b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean @@ -124,11 +124,11 @@ lemma finrank_lt_of_gt [FiniteDimensional F L] (H : F < E) : theorem finrank_dvd_of_le_left (h : F ≤ E) : finrank E L ∣ finrank F L := by let _ := (inclusion h).toRingHom.toAlgebra have : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq fun x ↦ rfl - exact Dvd.intro_left (finrank F E) (finrank_mul_finrank F E L) + exact Module.finrank_dvd_finrank_left F E L theorem finrank_dvd_of_le_right (h : F ≤ E) : finrank K F ∣ finrank K E := by let _ := (inclusion h).toRingHom.toAlgebra - exact Dvd.intro (finrank F E) (finrank_mul_finrank K F E) + exact Module.finrank_dvd_finrank_right K F E theorem finrank_le_of_le_left [FiniteDimensional F L] (h : F ≤ E) : finrank E L ≤ finrank F L := Nat.le_of_dvd Module.finrank_pos (finrank_dvd_of_le_left h) diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean index 691e13d49d..0f0b6dcf88 100644 --- a/Mathlib/LinearAlgebra/Dimension/Free.lean +++ b/Mathlib/LinearAlgebra/Dimension/Free.lean @@ -70,6 +70,30 @@ theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul, lift_rank_mul_lift_rank, toNat_lift] +theorem Module.finrank_dvd_finrank_left : + Module.finrank K A ∣ Module.finrank F A := + Dvd.intro_left (finrank F K) (finrank_mul_finrank ..) + +theorem Module.finrank_dvd_finrank_right : + Module.finrank F K ∣ Module.finrank F A := + Dvd.intro (finrank K A) (finrank_mul_finrank ..) + +theorem Module.finrank_div_finrank_cancel_right (h : Module.finrank K A ≠ 0) : + Module.finrank F A / Module.finrank K A = Module.finrank F K := + Nat.div_eq_of_eq_mul_left h.bot_lt (finrank_mul_finrank ..).symm + +theorem Module.finrank_div_finrank_cancel_left (h : Module.finrank F K ≠ 0) : + Module.finrank F A / Module.finrank F K = Module.finrank K A := + Nat.div_eq_of_eq_mul_right h.bot_lt (finrank_mul_finrank ..).symm + +theorem Module.finrank_div_finrank_cancel_right_of_nontrivial [Nontrivial A] [Module.Finite K A] : + Module.finrank F A / Module.finrank K A = Module.finrank F K := + finrank_div_finrank_cancel_right F K A ((finrank_pos_iff_of_free ..).mpr ‹_›).ne' + +theorem Module.finrank_div_finrank_cancel_left_of_nontrivial [Nontrivial K] [Module.Finite F K] : + Module.finrank F A / Module.finrank F K = Module.finrank K A := + finrank_div_finrank_cancel_left F K A ((finrank_pos_iff_of_free ..).mpr ‹_›).ne' + end Tower variable {R : Type u} {S : Type*} {M M₁ : Type v} {M' : Type v'} From 62244e5ddb2bb0c35e3500acb5730ad8fb4b17aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Sat, 1 Aug 2026 08:36:59 +0000 Subject: [PATCH 03/12] feat(Algebra/Homology): homotopy equivalences satisfy the two out of three property (#42321) --- Mathlib/Algebra/Homology/Homotopy.lean | 66 +++++++++++++++++++++++--- 1 file changed, 60 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index 9459cf7dc9..16cb0345f8 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/Mathlib/Algebra/Homology/Homotopy.lean @@ -714,9 +714,12 @@ def HomologicalComplex.homotopyEquivalences : namespace HomotopyEquiv +variable {C D E : HomologicalComplex V c} + +variable (C) in /-- Any complex is homotopy equivalent to itself. -/ -@[refl] -def refl (C : HomologicalComplex V c) : HomotopyEquiv C C where +@[refl, simps] +def refl : HomotopyEquiv C C where hom := 𝟙 C inv := 𝟙 C homotopyHomInvId := Homotopy.ofEq (by simp) @@ -726,16 +729,16 @@ instance : Inhabited (HomotopyEquiv C C) := ⟨refl C⟩ /-- Being homotopy equivalent is a symmetric relation. -/ -@[symm] -def symm {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : HomotopyEquiv D C where +@[symm, simps] +def symm (f : HomotopyEquiv C D) : HomotopyEquiv D C where hom := f.inv inv := f.hom homotopyHomInvId := f.homotopyInvHomId homotopyInvHomId := f.homotopyHomInvId /-- Homotopy equivalence is a transitive relation. -/ -@[trans] -def trans {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E) : +@[trans, simps] +def trans (f : HomotopyEquiv C D) (g : HomotopyEquiv D E) : HomotopyEquiv C E where hom := f.hom ≫ g.hom inv := g.inv ≫ f.inv @@ -749,8 +752,59 @@ def ofIso {ι : Type*} {V : Type u} [Category.{v} V] [Preadditive V] {c : Comple {C D : HomologicalComplex V c} (f : C ≅ D) : HomotopyEquiv C D := ⟨f.hom, f.inv, Homotopy.ofEq f.3, Homotopy.ofEq f.4⟩ +lemma homotopyEquivalences_hom (f : HomotopyEquiv C D) : + homotopyEquivalences _ _ f.hom := ⟨f, rfl⟩ + +lemma homotopyEquivalences_inv (f : HomotopyEquiv C D) : + homotopyEquivalences _ _ f.inv := f.symm.homotopyEquivalences_hom + +/-- If `f` if a homotopy equivalence and `h` is a homotopy from `f.hom` to +a morphism `g`, then this is a homotopy equivalence whose `hom` field is `g`. -/ +@[simps hom inv] +def copy (f : HomotopyEquiv C D) {g : C ⟶ D} (h : Homotopy f.hom g) : + HomotopyEquiv C D where + hom := g + inv := f.inv + homotopyHomInvId := (h.symm.compRight _).trans f.homotopyHomInvId + homotopyInvHomId := (h.symm.compLeft _).trans f.homotopyInvHomId + end HomotopyEquiv +namespace HomologicalComplex + +lemma homotopyEquivalences.of_isIso (f : C ⟶ D) [IsIso f] : homotopyEquivalences _ _ f := + ⟨.ofIso (asIso f), rfl⟩ + +lemma homotopyEquivalences.of_homotopy {f g : C ⟶ D} (h : homotopyEquivalences _ _ f) + (hfg : Homotopy f g) : + homotopyEquivalences _ _ g := by + obtain ⟨e, rfl⟩ := h + exact ⟨e.copy hfg, by simp⟩ + +instance : (homotopyEquivalences V c).IsMultiplicative where + id_mem K := ⟨.refl _, rfl⟩ + comp_mem f g := by + rintro ⟨f, rfl⟩ ⟨g, rfl⟩ + exact ⟨f.trans g, rfl⟩ + +instance : (homotopyEquivalences V c).HasTwoOutOfThreeProperty where + of_postcomp f _ := by + rintro ⟨g, rfl⟩ ⟨e, he⟩ + refine (e.trans g.symm).homotopyEquivalences_hom.of_homotopy ?_ + simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, Category.assoc] + exact g.homotopyHomInvId.compLeftId f + of_precomp _ g := by + rintro ⟨f, rfl⟩ ⟨e, he⟩ + refine (f.symm.trans e).homotopyEquivalences_hom.of_homotopy ?_ + simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, ← Category.assoc] + exact f.homotopyInvHomId.compRightId g + +instance : (homotopyEquivalences V c).RespectsIso := + MorphismProperty.respectsIso_of_isStableUnderComposition + (fun _ _ _ _ ↦ .of_isIso _) + +end HomologicalComplex + end namespace CategoryTheory From 32beea3cad9021f3904958d54eddddba078a6aca Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Sat, 1 Aug 2026 11:51:30 +0000 Subject: [PATCH 04/12] =?UTF-8?q?feat(Algebra/DirectSum):=20equivalence=20?= =?UTF-8?q?between=20direct=20sum=20indexed=20by=20=CE=B9=E2=82=81=20and?= =?UTF-8?q?=20double=20sum=20indexed=20by=20=CE=B9=E2=82=82=20and=20fibres?= =?UTF-8?q?=20of=20f=20:=20=CE=B9=E2=82=81=20=E2=86=92=20=CE=B9=E2=82=82?= =?UTF-8?q?=20(#39607)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 1. Add variant `equivCongrLeft'` of `equivCongrLeft`, and corresponding `…_apply` lemma. 2. Add `…_of lemmas` for both `equivCongrLeft` and `equivCongrLeft'`. 3. Add `…of lemma` for `sigmaCurry`, i.e. `sigmaCurry_of`. 4. Add `sigmaFiberAddEquiv`: the equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. Add two `…_apply` lemmas and an `…_of` lemma. Co-authored-by: TentativeConvert --- Mathlib/Algebra/DirectSum/Basic.lean | 49 ++++++++++++++++++++++++++-- 1 file changed, 46 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 90cac152dc..e9d35aa911 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -305,14 +305,20 @@ section CongrLeft variable {κ : Type*} -/-- Reindexing terms of a direct sum. -/ +/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence +`h : ι ≃ κ`. -/ def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv } @[simp] theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : - equivCongrLeft h f k = f (h.symm k) := by - exact DFinsupp.comapDomain'_apply _ h.right_inv _ _ + equivCongrLeft h f k = f (h.symm k) := + DFinsupp.comapDomain'_apply _ h.right_inv _ _ + +@[simp] +theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) : + equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := + DFinsupp.comapDomain'_single h.symm h.right_inv _ _ end CongrLeft @@ -342,6 +348,12 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) sigmaCurry f i j = f ⟨i, j⟩ := DFinsupp.sigmaCurry_apply (δ := δ) _ i j +@[simp] +theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i) (x : δ k.1 k.2) : + sigmaCurry (of (fun k ↦ δ k.1 k.2) k x) = + of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) := + DFinsupp.sigmaCurry_single k x + /-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of `curry`. -/ def sigmaUncurry : (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2 where @@ -360,6 +372,37 @@ def sigmaCurryEquiv : (⨁ i : Σ _i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j := end Sigma +section SigmaFiber + +variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) +variable {β : ι₁ → Type w} [Π i, AddCommMonoid (β i)] + +/-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type +`ι₂` together with the fibres of a map `f : ι₁ → ι₂`. -/ +def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := + (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans + (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) + +theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) : + sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := rfl + +@[simp] +theorem sigmaFiberAddEquiv_apply_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : + sigmaFiberAddEquiv f x j i' = x i' := rfl + +@[simp] +theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : + sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := + let h := Equiv.sigmaFiberEquiv f + let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ + calc sigmaFiberAddEquiv f (of β (h k) x) + _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by + rw [sigmaFiberAddEquiv_apply] + exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) + _ = of _ k.1 (of _ k.2 x) := by simp + +end SigmaFiber + /-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `AddSubmonoid M` indexed by `ι`. From 294355479299d19d1e1c759cef58e9e5e94e51b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 1 Aug 2026 13:03:27 +0000 Subject: [PATCH 05/12] chore({Archive,Counterexamples}): add missing `noncomputable` (#42170) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All these definitions are noncomputable (because they use choice/produce sets), but the computability checker doesn't spot this until I try making `Set` a one-field structure. This is because the computability checker doesn't even try to compute sorts, but it doesn't see that `s : Set α` is (equivalent to) a family of sorts. Follow-up to #41446. Generated by Claude Opus, then reviewed and cherry-picked line-by-line by myself. Assisted-by: Claude Opus 4.8 --- Archive/Wiedijk100Theorems/BuffonsNeedle.lean | 4 ++-- Counterexamples/TopologistsSineCurve.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean index c0b0dd6215..f5c08f4df5 100644 --- a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean +++ b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean @@ -96,7 +96,7 @@ Projection of a needle onto the x-axis. The needle's center is at x-coordinate ` `l` and angle `θ`. Note, `θ` is measured relative to the y-axis, that is, a vertical needle has `θ = 0`. -/ -def needleProjX (x θ : ℝ) : Set ℝ := Set.Icc (x - θ.sin * l / 2) (x + θ.sin * l / 2) +noncomputable def needleProjX (x θ : ℝ) : Set ℝ := Set.Icc (x - θ.sin * l / 2) (x + θ.sin * l / 2) /-- The indicator function of whether a needle at position `⟨x, θ⟩ : ℝ × ℝ` crosses the line `x = 0`. @@ -120,7 +120,7 @@ noncomputable def N : Ω → ℝ := needleCrossesIndicator l ∘ B /-- The possible x-positions and angle relative to the y-axis of a needle. -/ -abbrev needleSpace : Set (ℝ × ℝ) := Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 π +noncomputable abbrev needleSpace : Set (ℝ × ℝ) := Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 π include hd in lemma volume_needleSpace : ℙ (needleSpace d) = ENNReal.ofReal (d * π) := by diff --git a/Counterexamples/TopologistsSineCurve.lean b/Counterexamples/TopologistsSineCurve.lean index f1373a7b72..a552ce3ba8 100644 --- a/Counterexamples/TopologistsSineCurve.lean +++ b/Counterexamples/TopologistsSineCurve.lean @@ -31,14 +31,14 @@ open Topology Filter Set Real namespace TopologistsSineCurve /-- The topologist's sine curve, i.e. the graph of `y = sin (x⁻¹)` for `0 < x`. -/ -def S : Set (ℝ × ℝ) := (fun x ↦ (x, sin x⁻¹)) '' Ioi 0 +noncomputable def S : Set (ℝ × ℝ) := (fun x ↦ (x, sin x⁻¹)) '' Ioi 0 /-- The vertical line segment `{ (0, y) | -1 ≤ y ≤ 1 }`, which is the set of limit points of `S` not contained in `S` itself. -/ def Z : Set (ℝ × ℝ) := (fun y ↦ (0, y)) '' Icc (-1) 1 /-- The union of `S` and `Z` (which we will show is the closure of `S`). -/ -def T : Set (ℝ × ℝ) := S ∪ Z +noncomputable def T : Set (ℝ × ℝ) := S ∪ Z /-- A sequence of `x`-values tending to 0 at which the sine curve has a given `y`-coordinate. -/ noncomputable def xSeq (y : ℝ) (k : ℕ) := 1 / (arcsin y + (k + 1) * (2 * π)) From f4f85c2fcf7946e12ddc6ea21639d953b62d1284 Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Sat, 1 Aug 2026 13:14:38 +0000 Subject: [PATCH 06/12] chore: fix various typos (#42232) This PR probably removes most existing typos in mathlib docstrings. They were found by first extracting docstrings and putting them in a seperate txt file, then run a spell checker on in (in this case: https://github.com/codespell-project/codespell) and finally checking the output (many false ositives from names...) Co-authored-by: Batixx --- .../DerivedCategory/RightDerivedFunctorPlus.lean | 2 +- Mathlib/Algebra/Order/Star/Basic.lean | 2 +- .../DoldKan/SplitSimplicialObject.lean | 2 +- .../Analysis/Complex/UpperHalfPlane/FixedPoints.lean | 2 +- Mathlib/CategoryTheory/IsoCat.lean | 2 +- .../CategoryTheory/Sites/Precoverage/Generates.lean | 2 +- Mathlib/Condensed/Discrete/Colimit.lean | 2 +- Mathlib/Geometry/Convex/Cone/Face/Basic.lean | 4 ++-- .../VectorBundle/CovariantDerivative/Metric.lean | 2 +- Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean | 2 +- Mathlib/Probability/Distributions/Binomial.lean | 2 +- Mathlib/Probability/Distributions/Geometric.lean | 2 +- Mathlib/RingTheory/RingHomProperties.lean | 4 ++-- Mathlib/Tactic/Algebra/AlgebraNF.lean | 2 +- Mathlib/Tactic/Algebra/Basic.lean | 2 +- Mathlib/Tactic/ClickSuggestions/FindPremises.lean | 2 +- Mathlib/Tactic/ClickSuggestions/TryPremises.lean | 2 +- .../Tactic/ComputeAsymptotics/Multiseries/Basis.lean | 2 +- .../Tactic/ComputeAsymptotics/Multiseries/Defs.lean | 2 +- Mathlib/Tactic/Ring/Basic.lean | 4 ++-- Mathlib/Tactic/Ring/Common.lean | 6 +++--- Mathlib/Tactic/SetNotationForOrder.lean | 2 +- Mathlib/Tactic/Translate/Core.lean | 2 +- Mathlib/Topology/Algebra/Module/IsWeak.lean | 2 +- Mathlib/Topology/Algebra/Valued/ValuedField.lean | 2 +- Mathlib/Topology/CWComplex/Classical/Basic.lean | 4 ++-- Mathlib/Topology/Sets/Compacts.lean | 10 +++++----- 27 files changed, 37 insertions(+), 37 deletions(-) diff --git a/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean b/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean index 1fbd95aa53..b257a9a343 100644 --- a/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean +++ b/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean @@ -16,7 +16,7 @@ where `C` has enough injectives, we define the right derived functor between the corresponding bounded below derived categories. TODO(@joelriou): show that this functor is triangulated and refactor -the definiton of `Functor.rightDerived` +the definition of `Functor.rightDerived` -/ diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index 5ba1bd85cc..5e9a7191d7 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -472,7 +472,7 @@ instance (priority := 100) StarRingEquivClass.instOrderIsoClass [EquivLike F R S /-- While `IsSelfAdjoint.map` assumes the map is star-preserving, this lemma instead assumes the map is an order-preserving additive map from a space where self-adjoint elements can be expressed as -differences of nonnegative elemens, and whose codomain is a star-ordered ring. When such maps are +differences of nonnegative elements, and whose codomain is a star-ordered ring. When such maps are linear over `ℂ`, they are also star-preserving, and this lemma is used to establish that one by splitting into real and imaginary parts. -/ @[aesop safe apply (rule_sets := [CStarAlgebra])] diff --git a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean index dda65810f8..c3e2fbbed0 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean @@ -254,7 +254,7 @@ noncomputable def toNondegComplex : K[X] ⟶ s.nondegComplex := set_option backward.defeqAttrib.useBackward true in /-- Given a splitting `s` of a simplicial object `X` in a preadditive category, this is the split monomormphism from the chain complex `s.nondegComplex` to -the alternating face map complex fo `X`. -/ +the alternating face map complex of `X`. -/ @[no_expose] noncomputable def fromNondegComplex : s.nondegComplex ⟶ K[X] := (fullyFaithfulToKaroubi _).preimage diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean index d89e7b6c83..52510c6ad4 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean @@ -117,7 +117,7 @@ theorem gl_smul_eq_self_iff_quadratic (h : 0 < g.val.det) : simp [gl_smul_eq_iff_num_eq, σ, h, num, denom] grind -/-- If `g` is a non-scalar orientation perserving matrix with a fixed point in `ℍ`, +/-- If `g` is a non-scalar orientation preserving matrix with a fixed point in `ℍ`, then it's an elliptic matrix. -/ theorem isElliptic_of_exists_smul_eq_self (h : 0 < g.val.det) (hgc : g ∉ Subgroup.center _) (hfix : ∃ z : ℍ, g • z = z) : g.IsElliptic := by diff --git a/Mathlib/CategoryTheory/IsoCat.lean b/Mathlib/CategoryTheory/IsoCat.lean index b1bb84307c..5912c5c483 100644 --- a/Mathlib/CategoryTheory/IsoCat.lean +++ b/Mathlib/CategoryTheory/IsoCat.lean @@ -17,7 +17,7 @@ This is a strict notion, stronger than an equivalence of categories `C ≌ D`. We also define `Functor.IsIso` as a property saying that a functor is fully faithful and bijective on objects. We develop basic api for these two concepts. -Unless the application explicitely demands an isomorphism, the equivalence of categories is +Unless the application explicitly demands an isomorphism, the equivalence of categories is to be preferred. ## Main definitions diff --git a/Mathlib/CategoryTheory/Sites/Precoverage/Generates.lean b/Mathlib/CategoryTheory/Sites/Precoverage/Generates.lean index 3fc9fe92ea..f47f5e23b9 100644 --- a/Mathlib/CategoryTheory/Sites/Precoverage/Generates.lean +++ b/Mathlib/CategoryTheory/Sites/Precoverage/Generates.lean @@ -74,7 +74,7 @@ lemma Generates.isSheaf_of_forall (h : K.Generates J) (F : Cᵒᵖ ⥤ Type w) /- By assumption, the statement holds for `w = max u v`. The idea of the proof is to construct a suitable `Type max u v` valued subsheaf of `F` for each covering sieve `S` in `J` and every family of sections over `S` to check the necessary conditions. - We explain existence below, uniqueness works similary. -/ + We explain existence below, uniqueness works similarly. -/ intro X S hS rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] refine ⟨?_, ?_⟩ diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/Mathlib/Condensed/Discrete/Colimit.lean index 7579e7ecc2..4614a90010 100644 --- a/Mathlib/Condensed/Discrete/Colimit.lean +++ b/Mathlib/Condensed/Discrete/Colimit.lean @@ -40,7 +40,7 @@ abbrev locallyConstantPresheaf : Profinite.{u}ᵒᵖ ⥤ Type (u + 1) := #adaptation_note /-- In this declaration and `isColimitLocallyConstantPresheaf`, `coe_comp` interferes with rewriting via -`Cone.w`, so we needed to manualy exclude it. +`Cone.w`, so we needed to manually exclude it. -/ set_option backward.defeqAttrib.useBackward true in /-- diff --git a/Mathlib/Geometry/Convex/Cone/Face/Basic.lean b/Mathlib/Geometry/Convex/Cone/Face/Basic.lean index c99b7852c9..922db36ac9 100644 --- a/Mathlib/Geometry/Convex/Cone/Face/Basic.lean +++ b/Mathlib/Geometry/Convex/Cone/Face/Basic.lean @@ -23,8 +23,8 @@ in `F` are also in `F`. ## Implementation notes * We do not use `IsExtreme` as a definition because this is an affine notion and does not allow the - flexibility necessary to deal wth cones over general rings. E.g. the cone of positive integers has - no proper subset that are extreme. We prove that every face is an extreme set of its cone. + flexibility necessary to deal with cones over general rings. E.g. the cone of positive integers + has no proper subset that are extreme. We prove that every face is an extreme set of its cone. * Most results proven over a division ring hold more generally over an Archimedean ring. In particular, `iff_mem_of_add_mem_left` holds whenever for every `x ∈ R` there is a `y ∈ R` with `1 ≤ x * y`. diff --git a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean index 0214645732..c6f77447d3 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean @@ -36,7 +36,7 @@ metric `g` if and only if the differentiated metric tensor `∇ g` (defined by `CovariantDerivative.IsMetricCompatible` with the characterisation that parallel transport be an isometry. -* Given connections on bundles `V` and `W`, there is an induced connnection on the bundle +* Given connections on bundles `V` and `W`, there is an induced connection on the bundle `Hom(V, W)`. When this induced connection has been defined in Mathlib, rephrase the definition of `CovariantDerivative.derivMetricTensor`, to be simply the covariant derivative of the metric tensor (considered as a section of `Hom(V, Hom(V, ℝ))`). diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean index 3589e93ce4..74b492056d 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean @@ -80,7 +80,7 @@ and returning the `Trie α`. Performance note: In the `apply` search discrimination tree, after root node `⟨Eq, 3⟩`, there are about `150,000` entries in the `pending` array. -To deal with this smoothly, we parallellize the computation into chunks of `5000` entries. +To deal with this smoothly, we parallelize the computation into chunks of `5000` entries. -/ private def evalNode (trie : TrieIndex) : TreeM α (Trie α) := do let node := (← get)[trie]! diff --git a/Mathlib/Probability/Distributions/Binomial.lean b/Mathlib/Probability/Distributions/Binomial.lean index 29b4531403..7c124b3f60 100644 --- a/Mathlib/Probability/Distributions/Binomial.lean +++ b/Mathlib/Probability/Distributions/Binomial.lean @@ -36,7 +36,7 @@ Results should be proven for both `Bin(n, p)` and `Bin(R, n, p)` when possible, one to prove the second. Note that results concerning `Bin(R, n, p)` may require `[MeasurableSingletonClass R]` and/or `[CharZero R]`. -When refering to `Bin(n, p)` in names, use `binomial`. When refering to `Bin(R, n, p)`, +When referring to `Bin(n, p)` in names, use `binomial`. When referring to `Bin(R, n, p)`, use `map_cast_binomial`. ## Notation diff --git a/Mathlib/Probability/Distributions/Geometric.lean b/Mathlib/Probability/Distributions/Geometric.lean index dd685d47ad..a73c3605ea 100644 --- a/Mathlib/Probability/Distributions/Geometric.lean +++ b/Mathlib/Probability/Distributions/Geometric.lean @@ -19,7 +19,7 @@ As the parameter `p` needs to lie between `0` and `1`, we define `geometricMeasu `p : unitInterval`. Imagine a certain experience which has success probability `p`. If you repeat this experience -infintely many times and independently, the number of failures before the first success +infinitely many times and independently, the number of failures before the first success follows a geometric distribution with parameter `p`. ## Main definition diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean index 2e55dbc25f..e4b392180f 100644 --- a/Mathlib/RingTheory/RingHomProperties.lean +++ b/Mathlib/RingTheory/RingHomProperties.lean @@ -279,7 +279,7 @@ lemma CodescendsAlong.and (hP : CodescendsAlong P Q) (hP' : CodescendsAlong P' Q end Descent /-- A property of ring homomorphisms `P` is said to have equalizers, if the equalizer of algebra -maps between algebras satisfiying `P` also satisfies `P`. -/ +maps between algebras satisfying `P` also satisfies `P`. -/ def HasEqualizers (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop := ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f g : S →ₐ[R] T), P (algebraMap R S) → P (algebraMap R T) → @@ -290,7 +290,7 @@ lemma HasEqualizers.and (hP : HasEqualizers P) (hQ : HasEqualizers Q) : fun f g hf hg ↦ ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩ /-- A property of ring homomorphisms `P` is said to have finite products, if a finite product of -algebras satisfiying `Q` also satisfies `P`. -/ +algebras satisfying `Q` also satisfies `P`. -/ def HasFiniteProducts (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop := ∀ {R : Type u} [CommRing R] {ι : Type u} [_root_.Finite ι] (S : ι → Type u) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)], diff --git a/Mathlib/Tactic/Algebra/AlgebraNF.lean b/Mathlib/Tactic/Algebra/AlgebraNF.lean index 04730c671c..1ceaa5e51d 100644 --- a/Mathlib/Tactic/Algebra/AlgebraNF.lean +++ b/Mathlib/Tactic/Algebra/AlgebraNF.lean @@ -11,7 +11,7 @@ public import Mathlib.Tactic.Algebra.Basic This file contains helper functions for the (currently unimplemented) `algebra_nf` tactic. -The defnitions in this file are currently only used by `polynomial_nf`. +The definitions in this file are currently only used by `polynomial_nf`. -/ public meta section diff --git a/Mathlib/Tactic/Algebra/Basic.lean b/Mathlib/Tactic/Algebra/Basic.lean index 8f111bbc09..1b15b769a3 100644 --- a/Mathlib/Tactic/Algebra/Basic.lean +++ b/Mathlib/Tactic/Algebra/Basic.lean @@ -34,7 +34,7 @@ The main limitation of the current implementation is that it does not handle rat when the algebra `A` is a field but the base ring `R` is not. This is never an issue when working with polynomials, but would be an issue when working with a number field over its ring of integers. -When inferring the base ring, we assum that any two rings `R` and `S` that appear are comparable, +When inferring the base ring, we assume that any two rings `R` and `S` that appear are comparable, in the sense that either `R` is an `S`-algebra or `S` is an `R`-algebra. -/ diff --git a/Mathlib/Tactic/ClickSuggestions/FindPremises.lean b/Mathlib/Tactic/ClickSuggestions/FindPremises.lean index de12bedf79..fed54c353d 100644 --- a/Mathlib/Tactic/ClickSuggestions/FindPremises.lean +++ b/Mathlib/Tactic/ClickSuggestions/FindPremises.lean @@ -269,7 +269,7 @@ public def computeModuleDiscrTrees (choice : Choice) (parentDecl? : Option Name) return .append {} pre /-- Compute the discrimination trees for the local variables in `lctx`. -We restrict to the varaibles in `lctx` to avoid using introduced bound variables. -/ +We restrict to the variables in `lctx` to avoid using introduced bound variables. -/ public def computeLCtxDiscrTrees (choice : Choice) (lctx : LocalContext) (fvarId? : Option FVarId) : MetaM PreDiscrTrees := do let mut entries : Entries := {} diff --git a/Mathlib/Tactic/ClickSuggestions/TryPremises.lean b/Mathlib/Tactic/ClickSuggestions/TryPremises.lean index 02beae1c07..306662fe4b 100644 --- a/Mathlib/Tactic/ClickSuggestions/TryPremises.lean +++ b/Mathlib/Tactic/ClickSuggestions/TryPremises.lean @@ -157,7 +157,7 @@ def findRflTarget? (root subExpr : Expr) (rwKind : RwKind) : ClickSuggestionsM ( catch _ => return none -/-- Compute the library rearch suggestions. This uses `token` to incrementally udpate the output. -/ +/-- Compute the library rearch suggestions. This uses `token` to incrementally update the output. -/ public def librarySearchSuggestions (rootExpr subExpr : Expr) (lctx : LocalContext) (rwKind : RwKind) (parentDecl? : Option Name) (token : RefreshToken) : ClickSuggestionsM Unit := do diff --git a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Basis.lean b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Basis.lean index 81f1baed72..866fc87908 100644 --- a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Basis.lean +++ b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Basis.lean @@ -155,7 +155,7 @@ theorem push_log_last {basis_hd : ℝ → ℝ} {basis_tl : Basis} simpa [List.getLast_of_getLast?_eq_some hg] using Real.isLittleO_log_id_atTop.comp_tendsto <| Real.tendsto_log_atTop.comp <| h_basis.tendsto_atTop <| List.mem_of_getLast? hg -/-- Auxillary lemma. If function `f` is eventually positive, `g` tends to `atTop`, and +/-- Auxiliary lemma. If function `f` is eventually positive, `g` tends to `atTop`, and `log f =o[atTop] log g` then for any `a` and `b > 0`, then `f^a =o[atTop] g^b`. -/ theorem pow_isLittleO_pow_of_log {f g : ℝ → ℝ} (a b : ℝ) (hf : ∀ᶠ x in atTop, 0 < f x) (hg : Tendsto g atTop atTop) (h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)) (hb : 0 < b) : diff --git a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean index 51a86e9897..c504e032b5 100644 --- a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean +++ b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean @@ -882,7 +882,7 @@ theorem elim_cons {exp : ℝ} generalize h_ms : (mk (.cons exp coef tl) f) = ms at h cases h <;> simp at h_ms; grind -/-- One can replace `f` in `Approximates` with the funcion that eventually equals `f`. -/ +/-- One can replace `f` in `Approximates` with the function that eventually equals `f`. -/ theorem replaceFun {ms : MultiseriesExpansion (basis_hd :: basis_tl)} {f : ℝ → ℝ} (h_equiv : ms.toFun =ᶠ[atTop] f) (h_approx : ms.Approximates) : (ms.replaceFun f).Approximates := by diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean index ea4a8ac1fb..50ccb80447 100644 --- a/Mathlib/Tactic/Ring/Basic.lean +++ b/Mathlib/Tactic/Ring/Basic.lean @@ -33,7 +33,7 @@ even though it is not strictly speaking an equation in the language of commutati The basic approach to prove equalities is to normalise both sides and check for equality. We use `Mathlib.Tactic.Ring.Common` to implement the normal forms and normalization procedure. -This file defines the evaluation of basic operations such as addition and multipication of the +This file defines the evaluation of basic operations such as addition and multiplication of the rational coefficients as embedded inside the (semi)ring. This is done using `norm_num`. It further implements the core `ring1` tactic. @@ -479,7 +479,7 @@ partial def isOne {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring $α)) else failure -/-- The comarisons on the basetype used to compare normalized ring expressions. -/ +/-- The comparisons on the basetype used to compare normalized ring expressions. -/ partial def _root_.Mathlib.Tactic.Ring.ringCompare {u : Lean.Level} {α : Q(Type u)} : Common.RingCompare (α := α) RatCoeff where eq zx zy := zx.value == zy.value diff --git a/Mathlib/Tactic/Ring/Common.lean b/Mathlib/Tactic/Ring/Common.lean index d5b432a833..1e801aaa61 100644 --- a/Mathlib/Tactic/Ring/Common.lean +++ b/Mathlib/Tactic/Ring/Common.lean @@ -272,7 +272,7 @@ instance {α : Q(Type u)} {E : Q($α) → Type} {e : Q($α)} [Inhabited (Σ e, E let ⟨e', v⟩ : Σ e, E e := default; ⟨e', v, default⟩ -/-- Defines how comparisons and binary equality are computed in the base type. These are seperated +/-- Defines how comparisons and binary equality are computed in the base type. These are separated from RingCompute because they can often be defined without using instance caches. -/ structure RingCompare {u : Lean.Level} {α : Q(Type u)} (BaseType : Q($α) → Type) where /-- Returns whether two coefficients are equal -/ @@ -286,12 +286,12 @@ structure RingCompare {u : Lean.Level} {α : Q(Type u)} (BaseType : Q($α) → T `algebra` will implement these using `ring` -/ structure RingCompute {u : Lean.Level} {α : Q(Type u)} (BaseType : Q($α) → Type) (sα : Q(CommSemiring $α)) extends RingCompare BaseType where - /-- Evaluate the sum of two coefficents. + /-- Evaluate the sum of two coefficients. If the result is zero returns a proof of this fact, which is used to remove zero terms. -/ add {x y : Q($α)} : BaseType x → BaseType y → MetaM ((Result BaseType q($x + $y)) × (Option Q(IsNat ($x + $y) 0))) - /-- Evaluate the product of two coefficents. -/ + /-- Evaluate the product of two coefficients. -/ mul {x y : Q($α)} : BaseType x → BaseType y → MetaM (Result BaseType q($x * $y)) /-- Given a commutative ring `β` with a scalar multiplication action on `α` and a `x : β`, cast `x` to `α` such that the scalar multiplication turns into normal multiplication. Typically one diff --git a/Mathlib/Tactic/SetNotationForOrder.lean b/Mathlib/Tactic/SetNotationForOrder.lean index b8a5b03d20..48c149854b 100644 --- a/Mathlib/Tactic/SetNotationForOrder.lean +++ b/Mathlib/Tactic/SetNotationForOrder.lean @@ -26,7 +26,7 @@ tagged with `@[use_set_notation_for_order]`. This tag is used for `Set`, `Finset`, `PSet` and `ZFSet`. It is not used for `Multiset` and `List`, since they have both `≤` and `⊆` defined on them, with different meanings. -TODO: Unify more order operations suh as `∪`/`⊔` and `∩`/`⊓`. +TODO: Unify more order operations such as `∪`/`⊔` and `∩`/`⊓`. -/ /-- `UsesSetNotationForOrder` is used to track whether a type is tagged with diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean index a7e4bb221e..aedaa43e71 100644 --- a/Mathlib/Tactic/Translate/Core.lean +++ b/Mathlib/Tactic/Translate/Core.lean @@ -1002,7 +1002,7 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config unless ← withReducible <| isDefEq srcType tgtType do throwError "`{t.attrName}` validation failed: expected{indentExpr srcType}\nbut '{tgt}' has \ type{indentExpr tgtType}" - -- Process any remaining universe contraints, to assign all universe metavariables. + -- Process any remaining universe constraints, to assign all universe metavariables. discard <| processPostponed (mayPostpone := false) (exceptionOnFailure := true) let tgtParams := tgtDecl.levelParams.toArray let params ← levels.mapIdxM fun i level ↦ do diff --git a/Mathlib/Topology/Algebra/Module/IsWeak.lean b/Mathlib/Topology/Algebra/Module/IsWeak.lean index 841dc9ef29..a3bd4fe919 100644 --- a/Mathlib/Topology/Algebra/Module/IsWeak.lean +++ b/Mathlib/Topology/Algebra/Module/IsWeak.lean @@ -36,7 +36,7 @@ example (y : F) : Continuous (fun x : E ↦ B' x y) := sorry ``` However, this statement contains an abuse of the the definitional equality `E := E'` since `x : E`, -but `B'` has domain `E'`. Morever, one might be tempted to say that `B'.IsWeak`, but this is +but `B'` has domain `E'`. Moreover, one might be tempted to say that `B'.IsWeak`, but this is impossible because the domain of `B'` is `E'`, which is equipped with the incorrect topology. Instead, what one should do is to first define a new bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` by composing `B'` with the linear equivalence between `E` and `E'`, and then establish `B.IsWeak`. diff --git a/Mathlib/Topology/Algebra/Valued/ValuedField.lean b/Mathlib/Topology/Algebra/Valued/ValuedField.lean index a61856d733..235700f18d 100644 --- a/Mathlib/Topology/Algebra/Valued/ValuedField.lean +++ b/Mathlib/Topology/Algebra/Valued/ValuedField.lean @@ -421,7 +421,7 @@ theorem closure_coe_completion_v_mul_v_lt {r s : K} (hr : r ≠ 0) (hs : s ≠ 0 all_goals simp [← lt_div_iff₀, zero_lt_iff, hr] /-- The zero-preserving monoid homomorphism from the `ValueGroup₀` of the valuation on `K` to -that of the extension to its completion. TODO: Split out the definiton of `(restrict₀_surjective +that of the extension to its completion. TODO: Split out the definition of `(restrict₀_surjective (.ofClass hv.v) x).choose` and prove a spec lemma of it. Remove tactic `set` in the proof. -/ noncomputable def valueGroup₀_hom_extensionValuation : ValueGroup₀ (.ofClass hv.v) →*₀ ValueGroup₀ (.ofClass hv.extensionValuation) where diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean index 3d5c029693..5b66d66c1c 100644 --- a/Mathlib/Topology/CWComplex/Classical/Basic.lean +++ b/Mathlib/Topology/CWComplex/Classical/Basic.lean @@ -71,10 +71,10 @@ together. below for a restriction on when we want to create aliases. * For types and definitions relevant to CW complexes like `cell`, `openCell`, `closedCell`, `cellFrontier`, `skeletonLT` and similar, we want there to exist only one actually used version, - namely the version in the `RelCWComplex` namespace (and thus no seperate definition in the + namely the version in the `RelCWComplex` namespace (and thus no separate definition in the `CWComplex` namespace.) This is to avoid unnecessary duplication of lemmas. To achieve this, definitions from the `RelCWComplex` namespace should be added to the `CWComplex` namespace with - `export` intead of `alias_in`/`alias`. These will then apply to the absolute CW complex through + `export` instead of `alias_in`/`alias`. These will then apply to the absolute CW complex through the instance `CWComplex.instRelCWComplex`. * For statements, the auxiliary construction `skeletonLT` is preferred over `skeleton` as it makes the base case of inductions easier. The statement about `skeleton` should then be derived from the diff --git a/Mathlib/Topology/Sets/Compacts.lean b/Mathlib/Topology/Sets/Compacts.lean index bcac748c53..1663594972 100644 --- a/Mathlib/Topology/Sets/Compacts.lean +++ b/Mathlib/Topology/Sets/Compacts.lean @@ -284,7 +284,7 @@ theorem singleton_prod_singleton (x : α) (y : β) : open Topology -/-- The compacts neigbourhoods of a compact -/ +/-- The compacts neighbourhoods of a compact -/ def compactNhds (K : Compacts α) : Set (Compacts α) := {K' | ∀ (x : K), (K': Set α) ∈ 𝓝 x.val} @@ -301,7 +301,7 @@ lemma exists_open_set_nhds_of_mem_compactsNhds {K K' : Compacts α} (h : K' ∈ ∃ U : Opens α, (K : Set α) ⊆ U ∧ (U : Set α) ⊆ K' := exists_open_set_nhds_of_compactsNhds ⟨K', h⟩ -/-- The compact neigbourhood induced by the existence of an open subset between two compacts -/ +/-- The compact neighbourhood induced by the existence of an open subset between two compacts -/ def compactNhdsMkOfOpens {K : Compacts α} (L : Compacts α) (U : Opens α) (h1 : (K : Set α) ⊆ U) (h2 : (U : Set α) ⊆ L) : K.compactNhds := @@ -322,7 +322,7 @@ instance (K : Compacts α) : IsCodirectedOrder K.openNhds where ⟨Subtype.mk_le_mk.2 inf_le_left, Subtype.mk_le_mk.2 inf_le_right⟩⟩ instance (K : Compacts α) : Top K.openNhds := ⟨⊤, Set.subset_univ _⟩ --- in particular `K.openNhds` is not empty and thus the induced catgory is cofiltered +-- in particular `K.openNhds` is not empty and thus the induced category is cofiltered instance : Bot (⊥ : Compacts α).openNhds := ⟨⊥, fun _ h ↦ h⟩ @@ -378,14 +378,14 @@ namespace Opens /-- The set of compacts inside an open subset -/ def compactsInside (U : Opens α) : Set (Compacts α) := {K | (K : Set α) ⊆ U} -/-- For `K` a compact subset insde an open subset `U`, `U` has a structure of open neighbourhood +/-- For `K` a compact subset inside an open subset `U`, `U` has a structure of open neighbourhood of `K` -/ def openNhdsOfCompactsInside {U : Opens α} (K : U.compactsInside) : (K.val).openNhds := ⟨U, K.property⟩ end Opens -/-- For `U` an open neighbourhood of `K`, `K` has a structure of compact insde `U` -/ +/-- For `U` an open neighbourhood of `K`, `K` has a structure of compact inside `U` -/ def Compacts.compactsInsideOfOpenNhds {K : Compacts α} (U : K.openNhds) : (U.val).compactsInside := ⟨K, U.property⟩ From d5c40f0b612031a266692bc719fa5fef659fb7fa Mon Sep 17 00:00:00 2001 From: Francesco Chotuck <101644758+FrankieNC@users.noreply.github.com> Date: Sat, 1 Aug 2026 13:56:11 +0000 Subject: [PATCH 07/12] feat(MeasureTheory): pushforward of Hausdorff measure under a homothety (#41798) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove `Measure.map (AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d]` for `c ≠ 0`, resolving the TODO in `Mathlib/MeasureTheory/Measure/Hausdorff.lean`: the generalisation of `AffineMap.homothety_continuous` it was waiting for has since been merged, so the result follows from `hausdorffMeasure_homothety_preimage` via `Measure.ext`. --- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index da41388c14..40c6cffbbc 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -1065,9 +1065,11 @@ theorem hausdorffMeasure_homothety_preimage {d : ℝ} (hd : 0 ≤ d) (x : P) {c hausdorffMeasure_homothety_image hd x (_ : 𝕜ˣ).isUnit.ne_zero, Units.val_inv_eq_inv_val, Units.val_mk0, nnnorm_inv] -/-! TODO: prove `Measure.map (AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d]`, which needs a -more general version of `AffineMap.homothety_continuous`. -/ - +theorem map_homothety_hausdorffMeasure {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0) : + Measure.map (AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d] := by + ext s hs + rw [Measure.map_apply (AffineMap.homothety_continuous x c).measurable hs, + hausdorffMeasure_homothety_preimage hd x hc s, Measure.smul_apply] end NormedFieldAffine From cb48454af87fbe318fc368e6eb02c9156e1936c1 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Sat, 1 Aug 2026 16:40:17 +0000 Subject: [PATCH 08/12] chore(RingTheory/Valuation/Basic): remove all `set_option`s in this file (#42335) Co-authored-by: Whysoseriourhah --- Mathlib/RingTheory/Valuation/Basic.lean | 117 ++++++++++-------- .../Valuation/ValuativeRel/Basic.lean | 6 +- 2 files changed, 68 insertions(+), 55 deletions(-) diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean index 01cd74bc42..0c0dcca687 100644 --- a/Mathlib/RingTheory/Valuation/Basic.lean +++ b/Mathlib/RingTheory/Valuation/Basic.lean @@ -351,12 +351,17 @@ theorem map_one_sub_of_lt (h : v x < 1) : v (1 - x) = 1 := by rw [sub_eq_add_neg 1 x] simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h -set_option backward.isDefEq.respectTransparency false in +lemma OrderMonoidWithZeroHom.ofClass_monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} + [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] [FunLike F α β] + [MonoidWithZeroHomClass F α β] {f : F} (hf : Monotone f) : + Monotone (MonoidWithZeroHom.ofClass f) := hf + /-- An ordered monoid isomorphism `Γ₀ ≃ Γ'₀` induces an equivalence `Valuation R Γ₀ ≃ Valuation R Γ'₀`. -/ def congr (f : Γ₀ ≃*o Γ'₀) : Valuation R Γ₀ ≃ Valuation R Γ'₀ where - toFun := map (.ofClass f) f.toOrderIso.monotone - invFun := map (.ofClass f.symm) f.toOrderIso.symm.monotone + toFun := map (.ofClass f) (OrderMonoidWithZeroHom.ofClass_monotone f.toOrderIso.monotone) + invFun := map (.ofClass f.symm) + (OrderMonoidWithZeroHom.ofClass_monotone f.symm.toOrderIso.monotone) left_inv _ := by ext; simp right_inv _ := by ext; simp @@ -457,20 +462,32 @@ lemma leAddSubgroup_monotone (v : Valuation R Γ₀) : Monotone v.leAddSubgroup open MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ -set_option backward.isDefEq.respectTransparency.types false in /-- The restriction of a valuation so that it takes values in its `valueGroup₀`. -/ def restrict : Valuation R (ValueGroup₀ (.ofClass v)) where __ := restrict₀ (.ofClass v) map_add_le_max' x y := by by_cases H : v x ≠ 0 ∨ v y ≠ 0 - · rcases H with h | h <;> - simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, coe_ofClass, h, - reduceDIte, le_sup_iff] <;> - · split_ifs with H _ hy - all_goals simp [← Units.val_le_val] - simpa using map_add_le _ (by simp_all) (by simp_all) + · rcases H with h | h + all_goals simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, coe_ofClass, h, + reduceDIte, le_sup_iff] + all_goals split_ifs with H + · simp [H] + · simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk, ← Units.val_le_val, + Units.val_mk0] + split_ifs with hy + · simpa [hy] using map_add_le _ (le_rfl (a := v x)) (hy ▸ zero_le) + · simp [hy, ← Units.val_le_val] + · simp [H] + · simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk] + split_ifs with hx + · simpa [hx, ← Units.val_le_val] using map_add_le _ (hx ▸ zero_le) (le_rfl (a := v y)) + · simp [hx, ← Units.val_le_val] · simp only [ne_eq, not_or, Decidable.not_not] at H - simpa [restrict₀_apply, H] using map_add_le _ (le_of_eq H.1) (le_of_eq H.2) + simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, + MonoidWithZeroHom.coe_ofClass, H, ↓reduceDIte, max_self, nonpos_iff_eq_zero] + replace H : v (x + y) = 0 := + le_antisymm (map_add_le _ (le_of_eq H.1) (le_of_eq H.2)) zero_le + simp [H] lemma restrict_def (x : R) : v.restrict x = restrict₀ (.ofClass v) x := rfl @@ -478,34 +495,36 @@ lemma restrict_def (x : R) : v.restrict x = restrict₀ (.ofClass v) x := rfl lemma embedding_restrict (x : R) : embedding (v.restrict x) = v x := embedding_restrict₀ x -set_option backward.isDefEq.respectTransparency false in +lemma restrict_lt_iff_lt_embedding {x : R} {g : ValueGroup₀ (.ofClass v)} : + v.restrict x < g ↔ v x < embedding g := + embedding_strictMono.lt_iff_lt.symm.trans (by simp) + +lemma restrict_le_iff_le_embedding {x : R} {g : ValueGroup₀ (.ofClass v)} : + v.restrict x ≤ g ↔ v x ≤ embedding g := + embedding_strictMono.le_iff_le.symm.trans (by simp) + lemma restrict_eq_mk {x : R} (hx : v x ≠ 0) : v.restrict x = (valueGroup.mk (.ofClass v) 1 x (by simp) hx : ValueGroup₀ (.ofClass v)) := by - simp [restrict_def, restrict₀_apply, dif_neg hx, valueGroup.mk] + simp [restrict_def, restrict₀_apply, valueGroup.mk, hx] @[simp] lemma restrict_pos_iff (x : R) : 0 < v.restrict x ↔ 0 < v x := by simp only [restrict_def, restrict₀_apply] split_ifs with h <;> simpa [zero_lt_iff] -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma restrict_lt_iff {x y : R} : v.restrict x < v.restrict y ↔ v x < v y := by - simp [restrict_def, restrict₀_apply] - split_ifs with hx hy <;> simp_all [zero_lt_iff.mpr, ← Units.val_lt_val] + rw [restrict_lt_iff_lt_embedding, embedding_restrict] -set_option backward.isDefEq.respectTransparency.types false in -theorem isEquiv_restrict : v.IsEquiv v.restrict := by - intro x y - aesop (add norm [restrict_def, restrict₀_apply]) +@[simp] +lemma restrict_le_iff {x y : R} : v.restrict x ≤ v.restrict y ↔ v x ≤ v y := by + rw [restrict_le_iff_le_embedding, embedding_restrict] -lemma restrict_lt_iff_lt_embedding {x : R} {g : ValueGroup₀ (.ofClass v)} : - v.restrict x < g ↔ v x < embedding g := - embedding_strictMono.lt_iff_lt.symm.trans (by simp) +@[simp] +lemma restrict_inj {x y : R} : v.restrict x = v.restrict y ↔ v x = v y := + embedding_inj.symm.trans (by simp) -lemma restrict_le_iff_le_embedding {x : R} {g : ValueGroup₀ (.ofClass v)} : - v.restrict x ≤ g ↔ v x ≤ embedding g := - embedding_strictMono.le_iff_le.symm.trans (by simp) +theorem isEquiv_restrict : v.IsEquiv v.restrict := fun _ _ ↦ v.restrict_le_iff.symm @[simp] lemma restrict_lt_one_iff {x : R} : v.restrict x < 1 ↔ v x < 1 := by @@ -523,18 +542,6 @@ lemma restrict_eq_zero_iff {x : R} : v.restrict x = 0 ↔ v x = 0 := by lemma restrict_eq_one_iff {x : R} : v.restrict x = 1 ↔ v x = 1 := by simp [restrict_def, restrict₀_eq_one_iff] -set_option backward.isDefEq.respectTransparency.types false in -@[simp] -lemma restrict_le_iff {x y : R} : v.restrict x ≤ v.restrict y ↔ v x ≤ v y := by - simp only [restrict_def, restrict₀_apply, MonoidWithZeroHom.coe_ofClass] - split_ifs with hx hy <;> simp_all [← Units.val_le_val] - -set_option backward.isDefEq.respectTransparency.types false in -@[simp] -lemma restrict_inj {x y : R} : v.restrict x = v.restrict y ↔ v x = v y := by - simp only [restrict_def, restrict₀_apply, MonoidWithZeroHom.coe_ofClass] - aesop - lemma exists_div_eq_of_unit (γ : (ValueGroup₀ (.ofClass v))ˣ) : ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = γ.1 := by set u := WithZero.unzero (Units.ne_zero γ) with hu_def @@ -725,6 +732,9 @@ theorem eq_zero (h : v₁.IsEquiv v₂) {r : R} : v₁ r = 0 ↔ v₂ r = 0 := b have : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0 := h.eq_iff rwa [v₁.map_zero, v₂.map_zero] at this +lemma ofClass_eq_zero (h : v₁.IsEquiv v₂) {r : R} : (MonoidWithZeroHom.ofClass v₁) r = 0 ↔ + (MonoidWithZeroHom.ofClass v₂) r = 0 := eq_zero h + @[deprecated "use `(eq_zero _).ne` instead." (since := "2026-01-05")] theorem ne_zero (h : v₁.IsEquiv v₂) {r : R} : v₁ r ≠ 0 ↔ v₂ r ≠ 0 := (eq_zero h).ne @@ -797,6 +807,7 @@ section LinearOrderedCommGroupWithZero variable [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] [LinearOrderedCommGroupWithZero Γ''₀] + section Ring variable [Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀} {u : Valuation R Γ''₀} @@ -814,10 +825,12 @@ noncomputable def valueGroup₀Fun (h : v.IsEquiv w) (x : ValueGroup₀ (.ofClas haveI c := (x.zero_or_exists_mk'.resolve_left hx).choose valueGroup.mk (.ofClass w) c.1.1 c.1.2 (h.eq_zero.ne.mp c.2.1) (h.eq_zero.ne.mp c.2.2) -set_option backward.isDefEq.respectTransparency.types false in -theorem valueGroup₀Fun_spec (h : v.IsEquiv w) {r s : R} (hr : v r ≠ 0) (hs : v s ≠ 0) : +theorem valueGroup₀Fun_spec (h : v.IsEquiv w) {r s : R} (hr : (MonoidWithZeroHom.ofClass v) r ≠ 0) + (hs : (MonoidWithZeroHom.ofClass v) s ≠ 0) + (hr' : (MonoidWithZeroHom.ofClass w) r ≠ 0 := h.ofClass_eq_zero.ne.1 hr) + (hs' : (MonoidWithZeroHom.ofClass w) s ≠ 0 := h.ofClass_eq_zero.ne.1 hs) : valueGroup₀Fun h (valueGroup.mk (.ofClass v) r s hr hs) = - valueGroup.mk (.ofClass w) r s (h.eq_zero.ne.mp hr) (h.eq_zero.ne.mp hs) := by + valueGroup.mk (.ofClass w) r s hr' hs' := by rw [valueGroup₀Fun, dif_neg (by simp)] generalize_proofs _ _ _ _ H _ have c_spec := H.choose_spec @@ -826,7 +839,6 @@ theorem valueGroup₀Fun_spec (h : v.IsEquiv w) {r s : R} (hr : v r ≠ 0) (hs : theorem valueGroup₀Fun_zero (h : v.IsEquiv w) : valueGroup₀Fun h 0 = 0 := by simp [valueGroup₀Fun] -set_option backward.isDefEq.respectTransparency.types false in /-- The isomorphism between the `ValueGroup₀`'s of two equivalent valuations. -/ noncomputable def orderMonoidIso (h : v.IsEquiv w) : ValueGroup₀ (.ofClass v) ≃*o ValueGroup₀ (.ofClass w) where @@ -837,15 +849,15 @@ noncomputable def orderMonoidIso (h : v.IsEquiv w) : · simp_all [valueGroup₀Fun_zero] obtain _ | ⟨r₂, s₂, hr₂, hs₂, rfl⟩ := y.zero_or_exists_mk · simp_all [valueGroup₀Fun_zero] - simp [← WithZero.coe_mul, valueGroup.mk_mul, valueGroup₀Fun_spec] + simp [← WithZero.coe_mul, valueGroup.mk_mul, valueGroup₀Fun_spec h] left_inv x := by obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk · simp_all [valueGroup₀Fun_zero] - simp [valueGroup₀Fun_spec] + rw [valueGroup₀Fun_spec h, valueGroup₀Fun_spec h.symm] right_inv x := by obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk · simp_all [valueGroup₀Fun_zero] - simp [valueGroup₀Fun_spec] + rw [valueGroup₀Fun_spec h.symm, valueGroup₀Fun_spec h] map_le_map_iff' {x} {y} := by simp only [valueGroup₀Fun, ne_eq] split_ifs with hx0 hy0 hy0 @@ -880,30 +892,33 @@ theorem orderMonoidIso_spec (h : v.IsEquiv w) (a : R) : · rw [← restrict_eq_zero_iff] at ha rwa [ha, map_zero, Eq.comm, ← h_res.eq_zero] · rw [(v.restrict_eq_mk ha)] - convert! valueGroup₀Fun_spec (h := h) (hs := ha) (r := 1) (by simp) - exact w.restrict_eq_mk ((eq_zero h.symm).ne.mpr ha) + simp [orderMonoidIso, valueGroup₀Fun_spec h (hs := ha), + w.restrict_eq_mk ((eq_zero h.symm).ne.mpr ha)] + +lemma orderMonoidIso_spec₀ (h : v.IsEquiv w) (a : R) : + h.orderMonoidIso (restrict₀ (.ofClass v) a) = restrict₀ (.ofClass w) a := + orderMonoidIso_spec h a theorem orderMonoidIso_symm (h : v.IsEquiv w) (h' : w.IsEquiv v) : h.orderMonoidIso.symm = h'.orderMonoidIso := by rfl -set_option backward.isDefEq.respectTransparency false in @[simp] theorem orderMonoidIso_eq_refl (h : v.IsEquiv v) : h.orderMonoidIso = .refl _ := by ext x obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk · simp - · simp [orderMonoidIso, valueGroup₀Fun_spec] + · simp [orderMonoidIso, valueGroup₀Fun_spec h] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem orderMonoidIso_trans (h : v.IsEquiv w) (h' : w.IsEquiv u) : h.orderMonoidIso.trans h'.orderMonoidIso = (h.trans h').orderMonoidIso := by ext x obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk · simp - · simp [orderMonoidIso, valueGroup₀Fun_spec] + · simp [orderMonoidIso, valueGroup₀Fun_spec h, valueGroup₀Fun_spec h', + valueGroup₀Fun_spec (trans h h')] end IsEquiv diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean index 2fe4309342..12d87ad0c6 100644 --- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean +++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean @@ -1149,7 +1149,6 @@ lemma embed_strictMono [v.Compatible] : StrictMono (embed v) := by · simp [restrict₀_apply, embed] · simp [restrict₀_apply, embed] -set_option backward.isDefEq.respectTransparency false in /-- When we have `h : w.IsEquiv v`, the image group (with zero) of `v` is isomorphic to that of `w` via `h.orderMonoidIso`. Then the following diagram is commutative: @@ -1170,10 +1169,9 @@ theorem orderMonoidIso_embed [v.Compatible] {Γ' : Type*} [LinearOrderedCommGrou (w : Valuation R Γ') [w.Compatible] (x : ValueGroupWithZero R) (h : w.IsEquiv v) : h.orderMonoidIso (embed w x) = embed v x := by - simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk] + simp only [embed, coe_mk, ZeroHom.coe_mk] induction x using ValueGroupWithZero.ind with - | mk r s => - simp + | mk r s => simp [Valuation.IsEquiv.orderMonoidIso_spec₀] /-- If a valuation `v` is compatible with the valuative relation, then `ValueGroupWithZero R` is isomorphic to the image group (with zero) of `v` as an ordered group with zero. -/ From 0419afcbb9cf185587c9caf12e0cd4408f517127 Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Sat, 1 Aug 2026 21:09:15 +0000 Subject: [PATCH 09/12] chore(Combinatorics/SimpleGraph/Operations): golf `edge` lemmas (#41873) Also tags `Subgraph.Adj.adj_sub`/`spanningCoe_adj`/`sup_adj`/`edge_adj` with `grind`. --- .../Combinatorics/SimpleGraph/Acyclic.lean | 4 +-- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- .../Combinatorics/SimpleGraph/Operations.lean | 26 +++++++------------ .../Combinatorics/SimpleGraph/Subgraph.lean | 5 +++- 4 files changed, 16 insertions(+), 21 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index 47fd0de04d..1cab39f719 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean @@ -402,9 +402,9 @@ lemma reachable_eq_of_maximal_isAcyclic (F : SimpleGraph V) have : ∃ d ∈ p.darts, d.fst ∈ s ∧ d.snd ∉ s := p.exists_boundary_dart s rfl this rcases this with ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩ have : ¬F.Reachable v' u' := mt ConnectedComponent.sound <| s.mem_supp_iff u' |>.mp hu ▸ hv - suffices F ⊔ edge v' u' ≤ F by grind [Adj.reachable, sup_le_iff, le_iff_adj, edge_adj] + suffices F ⊔ edge v' u' ≤ F by grind [Adj.reachable, sup_le_iff, le_iff_adj] refine h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left - grind [Maximal, sup_le, le_iff_adj, edge_adj, huv.symm] + grind [Maximal, sup_le, le_iff_adj, huv.symm] /-- A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph. -/ theorem maximal_isAcyclic_iff_reachable_eq {F : SimpleGraph V} (hle : F ≤ G) (hF : F.IsAcyclic) : diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index f6adc4c39b..8ce12ed2dd 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -221,7 +221,7 @@ instance : Max (SimpleGraph V) where { Adj := x.Adj ⊔ y.Adj symm.symm v w h := by rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm] } -@[simp] +@[simp, grind =] theorem sup_adj (x y : SimpleGraph V) (v w : V) : (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w := Iff.rfl diff --git a/Mathlib/Combinatorics/SimpleGraph/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Operations.lean index 19ba94a37b..726a787560 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Operations.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Operations.lean @@ -136,13 +136,12 @@ section AddEdge /-- The graph with a single `s-t` edge. It is empty iff `s = t`. -/ def edge : SimpleGraph V := fromEdgeSet {s(s, t)} +@[grind =] lemma edge_adj (v w : V) : (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w := by rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff] lemma adj_edge {v w : V} : (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w := by - simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, - and_congr_left_iff] - tauto + grind lemma edge_comm : edge s t = edge t s := by rw [edge, edge, Sym2.eq_swap] @@ -166,7 +165,7 @@ lemma edge_le_iff {v w : V} : edge v w ≤ G ↔ v = w ∨ G.Adj v w := by obtain h | h := eq_or_ne v w · simp [h] · refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩ - aesop (add simp [edge_adj, adj_symm]) + grind [adj_symm] @[simp] lemma edgeSet_edge (v w : V) : (edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet := by simp [edge] @@ -180,16 +179,14 @@ lemma edgeSet_edge_of_ne (h : s ≠ t) : (edge s t).edgeSet = {s(s, t)} := by si @[deprecated (since := "2026-03-18")] alias edge_edgeSet_of_ne := edgeSet_edge_of_ne lemma sup_edge_of_adj (h : G.Adj s t) : G ⊔ edge s t = G := by - rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff, - mem_edgeSet] + simp [h] @[simp] lemma deleteEdges_edge {u v : V} {s : Set (Sym2 V)} (h : s(u, v) ∈ s) : (edge u v).deleteEdges s = ⊥ := by simp [edge, Set.sdiff_subset_iff, h] lemma disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v := by - by_cases h : u = v - · subst h - simp [edge_self_eq_bot] + rcases eq_or_ne u v with rfl | h + · simp [edge_self_eq_bot] simp [← disjoint_edgeSet, edgeSet_edge_of_ne h] lemma sdiff_edge {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G := by @@ -207,11 +204,7 @@ theorem sSup_edge_eq : sSup { edge u v | (u : V) (v : V) (_ : G.Adj u v) } = G : theorem Subgraph.spanningCoe_sup_edge_le {H : Subgraph (G ⊔ edge s t)} (h : ¬ H.Adj s t) : H.spanningCoe ≤ G := by intro v w hvw - have := hvw.adj_sub - simp only [Subgraph.spanningCoe_adj, SimpleGraph.sup_adj, SimpleGraph.edge_adj] at * - by_cases hs : s(v, w) = s(s, t) - · exact (h ((Subgraph.adj_congr_of_sym2 hs).mp hvw)).elim - · aesop + grind [adj_congr_of_sym2] variable [Fintype V] [DecidableRel G.Adj] @@ -220,9 +213,8 @@ instance : Fintype (edge s t).edgeSet := by rw [edge]; infer_instance theorem edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) : (G ⊔ edge s t).edgeFinset = G.edgeFinset.cons s(s, t) (by simp_all) := by - let := Classical.decEq V - rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm] - simp_rw [edgeFinset, edgeSet_edge_of_ne h]; rfl + classical + simp [edgeFinset, edgeSet_edge_of_ne h] theorem card_edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) : #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1 := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean index 62efb7fbfc..6799d9a54b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean @@ -111,6 +111,7 @@ theorem adj_symm (G' : Subgraph G) {u v : V} (h : G'.Adj u v) : G'.Adj v u := protected theorem Adj.symm {G' : Subgraph G} {u v : V} (h : G'.Adj u v) : G'.Adj v u := G'.adj_symm h +@[grind →] protected theorem Adj.adj_sub {H : G.Subgraph} {u v : V} (h : H.Adj u v) : G.Adj u v := H.adj_sub h @@ -169,11 +170,13 @@ protected def spanningCoe (G' : Subgraph G) : SimpleGraph V where symm := G'.symm loopless.irrefl _ hadj := G.irrefl hadj.adj_sub +attribute [grind =] Subgraph.spanningCoe_adj + @[simp] lemma spanningCoe_coe (G' : G.Subgraph) : G'.coe.spanningCoe = G'.spanningCoe := by ext simp only [map_adj, Function.Embedding.subtype_apply, Subtype.exists] - grind [spanningCoe_adj, coe_adj, edge_vert, adj_symm] + grind [coe_adj, edge_vert, adj_symm] theorem Adj.of_spanningCoe {G' : Subgraph G} {u v : G'.verts} (h : G'.spanningCoe.Adj u v) : G.Adj u v := From 54df8a3f96ac6f0b356728db732feb977d017aab Mon Sep 17 00:00:00 2001 From: "mathlib-update-dependencies[bot]" <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Date: Sat, 1 Aug 2026 21:19:44 +0000 Subject: [PATCH 10/12] chore: update Mathlib dependencies 2026-08-01 (#42347) This PR updates the Mathlib dependencies. --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index e8e2d9aa79..71d2d1d50d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2963c249dabd57512a2e101901777e381eb40350", + "rev": "0ecf8993df88c044962426c2cbca0de5717d6150", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 18f56bef5344cefb0563662c495e3eb3824a2589 Mon Sep 17 00:00:00 2001 From: Monica Omar <23701951+themathqueen@users.noreply.github.com> Date: Sun, 2 Aug 2026 03:03:54 +0000 Subject: [PATCH 11/12] feat(Analysis/CStarAlgebra/Basic): `star (ball x r) = ball (star x) r` (#42309) --- Mathlib/Analysis/CStarAlgebra/Basic.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean index 59c88f4ea2..3ecd3338d8 100644 --- a/Mathlib/Analysis/CStarAlgebra/Basic.lean +++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean @@ -77,6 +77,26 @@ instance [NormedField 𝕜] [NormedSpace 𝕜 E] [Star 𝕜] [TrivialStar 𝕜] NormedSpace 𝕜 (selfAdjoint E) where norm_smul_le _ _ := norm_smul_le _ (_ : E) +variable (x : E) (r : ℝ) + +@[simp] lemma Metric.star_ball : star (ball x r) = ball (star x) r := by + simpa using star_isometry.preimage_ball (star x) r + +@[simp] lemma Metric.star_closedBall : star (closedBall x r) = closedBall (star x) r := by + simpa using star_isometry.preimage_closedBall (star x) r + +@[simp] lemma Metric.star_sphere : star (sphere x r) = sphere (star x) r := by + simpa using star_isometry.preimage_sphere (star x) r + +@[simp] lemma dist_star_star (x y : E) : dist (star x) (star y) = dist x y := + star_isometry.dist_eq x y + +@[simp] lemma edist_star_star (x y : E) : edist (star x) (star y) = edist x y := + star_isometry.edist_eq x y + +@[simp] lemma nndist_star_star (x y : E) : nndist (star x) (star y) = nndist x y := + star_isometry.nndist_eq x y + end NormedStarGroup instance RingHomIsometric.starRingEnd [NormedCommRing E] [StarRing E] [NormedStarGroup E] : From ae0d973d69b779efa724095bd41793b8cf233831 Mon Sep 17 00:00:00 2001 From: Emily Riehl <19517483+emilyriehl@users.noreply.github.com> Date: Sun, 2 Aug 2026 05:59:39 +0000 Subject: [PATCH 12/12] feat(CategoryTheory): initial object implies corepresentable (#41994) If the category of elements of a covariant functor has an initial object, then the functor is corepresentable. Co-authored-by: emilyriehl --- Mathlib/CategoryTheory/Limits/Elements.lean | 55 +++++++++++++++++++-- 1 file changed, 50 insertions(+), 5 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Elements.lean b/Mathlib/CategoryTheory/Limits/Elements.lean index 4648d35aba..04b8205c15 100644 --- a/Mathlib/CategoryTheory/Limits/Elements.lean +++ b/Mathlib/CategoryTheory/Limits/Elements.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Markus Himmel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Markus Himmel +Authors: Markus Himmel, Emily Riehl -/ module @@ -22,10 +22,6 @@ the category of elements of `A` has limits of shape `I` and the forgetful functo - If `A` is (co)representable, then `A.Elements` has an initial object. -## TODOs - -- Show that `A` is (co)representable if `A.Elements` has an initial object. - -/ set_option backward.defeqAttrib.useBackward true @@ -135,4 +131,53 @@ end Initial end CategoryOfElements +namespace Functor.Elements + +/-- An initial object in the category `F.Elements` of a covariant functor defines a +corepresentation for that functor. -/ +def corepresentableByOfIsInitial {F : C ⥤ Type w} {E : Elements F} (he : IsInitial E) : + CorepresentableBy F E.fst where + homEquiv := + { toFun f := F.map f E.snd + invFun y := (he.to ⟨_, y⟩).val + left_inv f := Subtype.ext_iff.mp (he.hom_ext (he.to ⟨_, F.map f E.snd⟩) ⟨f, rfl⟩) + right_inv y := (he.to ⟨_, y⟩).prop } + +lemma isCorepresentable_of_hasInitial (F : C ⥤ Type w) [HasInitial (Elements F)] : + IsCorepresentable F where + has_corepresentation := + ⟨(⊥_ F.Elements).fst, + (Nonempty.intro (corepresentableByOfIsInitial initialIsInitial))⟩ + +theorem hasInitial_iff_isCorepresentable (F : C ⥤ Type w) : + HasInitial (Elements F) ↔ IsCorepresentable F where + mp _ := isCorepresentable_of_hasInitial F + mpr _ := inferInstance + +/-- An initial object in the category `F.Elements` of a contravariant functor defines a +representation for that functor. -/ +def representableByOfIsInitial {F : Cᵒᵖ ⥤ Type w} {E : Elements F} (he : IsInitial E) : + RepresentableBy F (E.fst.unop) where + homEquiv := + { toFun f := F.map f.op E.snd + invFun y := (he.to ⟨_, y⟩).val.unop + left_inv f := by + have := + Subtype.ext_iff.mp (he.hom_ext (he.to ⟨_, F.map f.op E.snd⟩) ⟨f.op, rfl⟩) + simp only [this, Quiver.Hom.unop_op] + right_inv y := (he.to ⟨_, y⟩).prop } + +lemma isRepresentable_of_hasInitial (F : Cᵒᵖ ⥤ Type w) [HasInitial (Elements F)] : + IsRepresentable F where + has_representation := + ⟨(⊥_ F.Elements).fst.unop, + (Nonempty.intro (representableByOfIsInitial initialIsInitial))⟩ + +theorem hasInitial_iff_isRepresentable (F : Cᵒᵖ ⥤ Type w) : + HasInitial (Elements F) ↔ IsRepresentable F where + mp _ := isRepresentable_of_hasInitial F + mpr _ := inferInstance + +end Functor.Elements + end CategoryTheory