From 21da9fc40346c3663f0ecad16e2198748a5ba1ca Mon Sep 17 00:00:00 2001 From: Salvatore Mercuri <47568553+smmercuri@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:07:23 +0000 Subject: [PATCH 01/20] feat: notation for adele rings (#40535) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Notation: - `K∞` : `NumberField.InfiniteAdeleRing K`; - `𝔸ᶠ[R, K]`: `IsDedekindDomain.FiniteAdeleRing R K`; - `𝔸[R, K]` : `NumberField.AdeleRing R K`; - specialisations `𝔸ᶠ[K]` and `𝔸[K]` to `R = RingOfIntegers K`. --- .../NumberTheory/NumberField/AdeleRing.lean | 19 +++++++---- .../NumberField/InfiniteAdeleRing.lean | 32 +++++++++---------- .../DedekindDomain/FiniteAdeleRing.lean | 29 +++++++++-------- 3 files changed, 44 insertions(+), 36 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/AdeleRing.lean b/Mathlib/NumberTheory/NumberField/AdeleRing.lean index fc0c7267779..c88b4583107 100644 --- a/Mathlib/NumberTheory/NumberField/AdeleRing.lean +++ b/Mathlib/NumberTheory/NumberField/AdeleRing.lean @@ -50,24 +50,31 @@ deriving CommRing, TopologicalSpace, IsTopologicalRing, Algebra K namespace AdeleRing +/-- `𝔸ᶠ[K]` is notation for `IsDedekindDomain.FiniteAdeleRing (𝓞 K) K`. -/ +scoped notation:max "𝔸ᶠ[" K "]" => FiniteAdeleRing (𝓞 K) K +/-- `𝔸[R, K]` is notation for `NumberField.AdeleRing R K`. -/ +scoped notation:max "𝔸[" R ", " K "]" => AdeleRing R K +/-- `𝔸[K]` is notation for `NumberField.AdeleRing (𝓞 K) K`. -/ +scoped notation:max "𝔸[" K "]" => AdeleRing (𝓞 K) K + variable (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] -instance : Inhabited (AdeleRing R K) := ⟨0⟩ +instance : Inhabited 𝔸[R, K] := ⟨0⟩ @[simp] theorem algebraMap_fst_apply (x : K) (v : InfinitePlace K) : - (algebraMap K (AdeleRing R K) x).1 v = x := rfl + (algebraMap K 𝔸[R, K] x).1 v = x := rfl @[simp] theorem algebraMap_snd_apply (x : K) (v : HeightOneSpectrum R) : - (algebraMap K (AdeleRing R K) x).2 v = x := rfl + (algebraMap K 𝔸[R, K] x).2 v = x := rfl -theorem algebraMap_injective [NumberField K] : Function.Injective (algebraMap K (AdeleRing R K)) := - fun _ _ hxy => (algebraMap K _).injective (Prod.ext_iff.1 hxy).1 +theorem algebraMap_injective [NumberField K] : Function.Injective (algebraMap K 𝔸[R, K]) := + fun _ _ hxy => (algebraMap K K∞).injective (Prod.ext_iff.1 hxy).1 /-- The subgroup of principal adeles `(x)ᵥ` where `x ∈ K`. -/ -abbrev principalSubgroup : AddSubgroup (AdeleRing R K) := (algebraMap K _).range.toAddSubgroup +abbrev principalSubgroup : AddSubgroup 𝔸[R, K] := (algebraMap K 𝔸[R, K]).range.toAddSubgroup end AdeleRing diff --git a/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean b/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean index a1cd977f3b3..e2e126fb604 100644 --- a/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean +++ b/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean @@ -54,24 +54,26 @@ deriving CommRing, Inhabited, TopologicalSpace, IsTopologicalRing, Algebra K namespace InfiniteAdeleRing +/-- `K∞` is notation for `NumberField.InfiniteAdeleRing K`. -/ +scoped[NumberField.AdeleRing] notation:max K "∞" => InfiniteAdeleRing K + +open scoped AdeleRing + variable (K : Type*) [Field K] -instance [NumberField K] : Nontrivial (InfiniteAdeleRing K) := +instance [NumberField K] : Nontrivial K∞ := (inferInstance : Nonempty (InfinitePlace K)).elim fun w => Pi.nontrivial_at w -@[simp] -theorem algebraMap_apply (x : K) (v : InfinitePlace K) : - algebraMap K (InfiniteAdeleRing K) x v = x := rfl +@[simp] theorem algebraMap_apply (x : K) (v : InfinitePlace K) : algebraMap K K∞ x v = x := rfl /-- The infinite adele ring is locally compact. -/ -instance locallyCompactSpace [NumberField K] : LocallyCompactSpace (InfiniteAdeleRing K) := +instance locallyCompactSpace [NumberField K] : LocallyCompactSpace K∞ := Pi.locallyCompactSpace_of_finite open scoped Classical in /-- The ring isomorphism between the infinite adele ring of a number field and the space `ℝ ^ r₁ × ℂ ^ r₂`, where `(r₁, r₂)` is the signature of the number field. -/ -abbrev ringEquiv_mixedSpace : - InfiniteAdeleRing K ≃+* mixedEmbedding.mixedSpace K := +abbrev ringEquiv_mixedSpace : K∞ ≃+* mixedEmbedding.mixedSpace K := RingEquiv.trans (RingEquiv.piEquivPiSubtypeProd (fun (v : InfinitePlace K) => IsReal v) (fun (v : InfinitePlace K) => v.Completion)) @@ -84,7 +86,7 @@ abbrev ringEquiv_mixedSpace : Equiv.subtypeEquivRight (fun _ => not_isReal_iff_isComplex)))) @[simp] -theorem ringEquiv_mixedSpace_apply (x : InfiniteAdeleRing K) : +theorem ringEquiv_mixedSpace_apply (x : K∞) : ringEquiv_mixedSpace K x = (fun (v : {w : InfinitePlace K // IsReal w}) => extensionEmbeddingOfIsReal v.2 (x v), fun (v : {w : InfinitePlace K // IsComplex w}) => extensionEmbedding v.1 (x v)) := rfl @@ -93,7 +95,7 @@ theorem ringEquiv_mixedSpace_apply (x : InfiniteAdeleRing K) : ring to the mixed embedding `x ↦ (φᵢ(x))ᵢ` of `K` into the space `ℝ ^ r₁ × ℂ ^ r₂`, where `(r₁, r₂)` is the signature of `K` and `φᵢ` are the complex embeddings of `K`. -/ theorem mixedEmbedding_eq_algebraMap_comp {x : K} : - mixedEmbedding K x = ringEquiv_mixedSpace K (algebraMap K _ x) := by + mixedEmbedding K x = ringEquiv_mixedSpace K (algebraMap K K∞ x) := by ext v <;> simp /-- @@ -101,23 +103,21 @@ theorem mixedEmbedding_eq_algebraMap_comp {x : K} : The number field $K$ is dense in the infinite adele ring $\prod_v K_v$. -/ -theorem denseRange_algebraMap [NumberField K] : DenseRange <| algebraMap K (InfiniteAdeleRing K) := +theorem denseRange_algebraMap [NumberField K] : DenseRange <| algebraMap K K∞ := (DenseRange.piMap fun v => Completion.denseRange_coe v).comp (InfinitePlace.denseRange_algebraMap_pi K) (.piMap fun v => Completion.continuous_coe v) /-- The norm on the infinite adele ring is given by the product of the normalized norms across infinite places. The normalized norm is the real norm at real places and the square of the complex norm at complex places. -/ -instance [NumberField K] : Norm (InfiniteAdeleRing K) where - norm x := ∏ v, ‖x v‖ ^ v.mult +instance [NumberField K] : Norm K∞ where norm x := ∏ v, ‖x v‖ ^ v.mult variable {K} -theorem norm_def [NumberField K] (x : InfiniteAdeleRing K) : - ‖x‖ = ∏ v, ‖x v‖ ^ v.mult := rfl +theorem norm_def [NumberField K] (x : K∞) : ‖x‖ = ∏ v, ‖x v‖ ^ v.mult := rfl set_option backward.isDefEq.respectTransparency false in -theorem norm_eq_zero_of_not_isUnit [NumberField K] {x : InfiniteAdeleRing K} (hx : ¬IsUnit x) : +theorem norm_eq_zero_of_not_isUnit [NumberField K] {x : K∞} (hx : ¬IsUnit x) : ‖x‖ = 0 := by rw [Pi.isUnit_iff, not_forall] at hx obtain ⟨v, hv⟩ := hx @@ -126,7 +126,7 @@ theorem norm_eq_zero_of_not_isUnit [NumberField K] {x : InfiniteAdeleRing K} (hx /-- The product formula for the infinite adele ring. This is the adelic version of `NumberField.InfinitePlace.prod_eq_abs_norm`. -/ theorem coe_norm_eq_abs_norm [NumberField K] (x : K) : - ‖algebraMap K (InfiniteAdeleRing K) x‖ = |Algebra.norm ℚ x| := by + ‖algebraMap K K∞ x‖ = |Algebra.norm ℚ x| := by simpa [-Rat.cast_abs, norm_def] using! InfinitePlace.prod_eq_abs_norm x end InfiniteAdeleRing diff --git a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean index 0cda4b73f6b..7d3a06d38fc 100644 --- a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean +++ b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean @@ -106,13 +106,16 @@ instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (adicCompletion namespace FiniteAdeleRing +/-- `𝔸ᶠ[R, K]` is notation for `IsDedekindDomain.FiniteAdeleRing R K`. -/ +scoped notation:max "𝔸ᶠ[" R ", " K "]" => FiniteAdeleRing R K + /-- The canonical map from `K` to the finite adeles of `K`. The content of the existence of this map is the fact that an element `k` of `K` is integral at all but finitely many places, which is `IsDedekindDomain.HeightOneSpectrum.Support.finite R k`. -/ -protected def algebraMap : K →+* FiniteAdeleRing R K where +protected def algebraMap : K →+* 𝔸ᶠ[R, K] where toFun k := ⟨fun i ↦ k, by simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K, valuedAdicCompletion_eq_valuation', not_le] @@ -122,25 +125,25 @@ protected def algebraMap : K →+* FiniteAdeleRing R K where map_zero' := Subtype.ext <| funext fun _ ↦ adicCompletion.coe_zero .. map_add' x y := Subtype.ext <| funext fun _ ↦ adicCompletion.coe_add .. -instance : Algebra K (FiniteAdeleRing R K) := (FiniteAdeleRing.algebraMap R K).toAlgebra +instance : Algebra K 𝔸ᶠ[R, K] := (FiniteAdeleRing.algebraMap R K).toAlgebra @[simp] theorem algebraMap_apply (k : K) (v : HeightOneSpectrum R) : - algebraMap K (FiniteAdeleRing R K) k v = k := rfl + algebraMap K 𝔸ᶠ[R, K] k v = k := rfl -instance : Algebra R (FiniteAdeleRing R K) := Algebra.compHom _ (algebraMap R K) +instance : Algebra R 𝔸ᶠ[R, K] := Algebra.compHom _ (algebraMap R K) -instance : IsScalarTower R K (FiniteAdeleRing R K) := +instance : IsScalarTower R K 𝔸ᶠ[R, K] := IsScalarTower.of_algebraMap_eq' rfl variable {R} in @[ext] -lemma ext {a₁ a₂ : FiniteAdeleRing R K} (h : ∀ v, a₁ v = a₂ v) : a₁ = a₂ := +lemma ext {a₁ a₂ : 𝔸ᶠ[R, K]} (h : ∀ v, a₁ v = a₂ v) : a₁ = a₂ := Subtype.ext <| funext h section Topology -instance : IsTopologicalRing (FiniteAdeleRing R K) := +instance : IsTopologicalRing 𝔸ᶠ[R, K] := haveI : Fact (∀ v : HeightOneSpectrum R, IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K))) := ⟨fun _ ↦ Valued.isOpen_valuationSubring _⟩ @@ -153,19 +156,19 @@ section Units variable {R K} set_option backward.isDefEq.respectTransparency false in -theorem isUnit_iff {a : FiniteAdeleRing R K} : +theorem isUnit_iff {a : 𝔸ᶠ[R, K]} : IsUnit a ↔ (∀ v, a v ≠ 0) ∧ ∀ᶠ v in Filter.cofinite, Valued.v (a v) = 1 := by rw [RestrictedProduct.isUnit_iff] simp only [isUnit_iff_ne_zero, adicCompletionIntegers.isUnit_iff_valued_eq_one, exists_prop, Filter.eventually_cofinite, not_and_or, Set.ofPred_or] simpa using! fun _ _ ↦ a.2 -theorem unitsEquiv_finite_valued_eq_one (a : (FiniteAdeleRing R K)ˣ) : +theorem unitsEquiv_finite_valued_eq_one (a : 𝔸ᶠ[R, K]ˣ) : ∀ᶠ v in Filter.cofinite, Valued.v (RestrictedProduct.unitsEquiv _ a v).1 = 1 := by filter_upwards [(RestrictedProduct.unitsEquiv _ a).2] using fun _ h ↦ adicCompletionIntegers.mem_units_iff_valued_eq_one.1 h -theorem infinite_valued_ne_one_of_not_isUnit {a : FiniteAdeleRing R K} (ha₀ : ∀ v, a v ≠ 0) +theorem infinite_valued_ne_one_of_not_isUnit {a : 𝔸ᶠ[R, K]} (ha₀ : ∀ v, a v ≠ 0) (ha : ¬IsUnit a) : {v | Valued.v (a v) ≠ 1}.Infinite := by contrapose! ha rw [isUnit_iff] @@ -175,11 +178,9 @@ variable (R) variable (K) in /-- The global embedding of the units of `K` into the units of `FiniteAdeleRing R K`. -/ -def unitEmbedding : Kˣ →* (FiniteAdeleRing R K)ˣ := Units.map (algebraMap K (FiniteAdeleRing R K)) +def unitEmbedding : Kˣ →* 𝔸ᶠ[R, K]ˣ := Units.map (algebraMap K 𝔸ᶠ[R, K]) -@[simp] -theorem unitEmbedding_apply (k : Kˣ) : - unitEmbedding R K k = algebraMap K (FiniteAdeleRing R K) k := rfl +@[simp] theorem unitEmbedding_apply (k : Kˣ) : unitEmbedding R K k = algebraMap K 𝔸ᶠ[R, K] k := rfl end Units From be4fe8f18dc36f2938ae3ec16af35008bd0d6224 Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Wed, 29 Jul 2026 08:16:47 +0000 Subject: [PATCH 02/20] fix(LinearAlgebra/Matrix): make accidental private instance public (#42212) Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/LinearAlgebra/Matrix/Nonsingular.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean b/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean index 68ef3c3b93a..4bd03428237 100644 --- a/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean +++ b/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean @@ -5,9 +5,9 @@ Authors: Junyan Xu, Aristotle AI -/ module +public import Mathlib.LinearAlgebra.InvariantBasisNumber public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic -import Mathlib.LinearAlgebra.InvariantBasisNumber import Mathlib.LinearAlgebra.Matrix.SemiringInverse import Mathlib.LinearAlgebra.Matrix.ToLin @@ -33,13 +33,13 @@ a matrix is nonsingular if and only if its determinant is not a zero divisor). rank condition. -/ +public section + variable {R m n : Type*} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] variable {A : Matrix n n R} namespace Matrix -public section - lemma isDetpBalanced_iff_sub_mul_det_eq_zero {R : Type*} [CommRing R] {A : Matrix n n R} {a b : R} : A.IsDetpBalanced a b ↔ (a - b) * A.det = 0 := by grind [IsDetpBalanced, det_eq_detp_sub_detp] @@ -141,8 +141,6 @@ theorem linearIndependent_col_iff_row [Finite n] : have := Fintype.ofFinite classical rw [linearIndependent_col_iff, linearIndependent_row_iff] -end - end Matrix open Matrix From 69538871db6b37033c369f63feadb1559ab1f2d8 Mon Sep 17 00:00:00 2001 From: Richard Osborn Date: Wed, 29 Jul 2026 08:26:23 +0000 Subject: [PATCH 03/20] feat(SetTheory/Cardinal): strong induction on Nat.card for finite types (#41978) Add the `Finite` analogue for `induction_subsingleton_or_nontrivial`. --- Mathlib/GroupTheory/Nilpotent.lean | 26 +++++++++---------------- Mathlib/SetTheory/Cardinal/NatCard.lean | 18 +++++++++++++++++ 2 files changed, 27 insertions(+), 17 deletions(-) diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean index 5306d9a7705..2e510e6fa9f 100644 --- a/Mathlib/GroupTheory/Nilpotent.lean +++ b/Mathlib/GroupTheory/Nilpotent.lean @@ -1207,23 +1207,15 @@ variable {G : Type*} [hG : Group G] /-- A p-group is nilpotent -/ theorem IsPGroup.isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) : IsNilpotent G := by - cases nonempty_fintype G - classical - revert hG - apply @Fintype.induction_subsingleton_or_nontrivial _ G _ - · intro _ _ _ _ - infer_instance - · intro G _ _ ih _ h - have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by - simp only [← Nat.card_eq_fintype_card] - rw [card_eq_card_quotient_mul_card_subgroup (center G)] - simp only [Nat.card_eq_fintype_card] - apply lt_mul_of_one_lt_right - · exact Fintype.card_pos_iff.mpr One.instNonempty - · simp only [← Nat.card_eq_fintype_card] - exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center) - have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G)) - exact of_quotient_center_nilpotent hnq + induction G using Finite.induction_subsingleton_or_nontrivial generalizing hG with + | hbase => infer_instance + | hstep G ih => + have hcq : Nat.card (G ⧸ center G) < Nat.card G := by + rw [card_eq_card_quotient_mul_card_subgroup (center G)] + apply lt_mul_of_one_lt_right Nat.card_pos + exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center) + have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G)) + exact of_quotient_center_nilpotent hnq variable [Finite G] diff --git a/Mathlib/SetTheory/Cardinal/NatCard.lean b/Mathlib/SetTheory/Cardinal/NatCard.lean index ee56380d8b6..c238a719a3a 100644 --- a/Mathlib/SetTheory/Cardinal/NatCard.lean +++ b/Mathlib/SetTheory/Cardinal/NatCard.lean @@ -146,6 +146,24 @@ theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) : have := Fintype.ofFinite α simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx +/-- A custom induction principle for finite types, by strong induction on `Nat.card`: +the base case is a subsingleton type, and the induction step is for nontrivial types, +where one can assume the hypothesis for all types of smaller cardinality. -/ +@[elab_as_elim] +theorem induction_subsingleton_or_nontrivial {P : Type* → Prop} (α) [Finite α] + (hbase : ∀ (α) [Finite α] [Subsingleton α], P α) + (hstep : ∀ (α) [Finite α] [Nontrivial α], + (∀ (β) [Finite β], Nat.card β < Nat.card α → P β) → P α) : + P α := by + obtain ⟨n, hn⟩ : ∃ n, Nat.card α = n := ⟨Nat.card α, rfl⟩ + induction n using Nat.strong_induction_on generalizing α with | _ n ih + rcases subsingleton_or_nontrivial α with hsing | hnontriv + · apply hbase + · apply hstep + intro β _ hlt + rw [hn] at hlt + exact ih (Nat.card β) hlt _ rfl + end Finite namespace ENat From e91869b3f7e43297eb8ecae06142b0e1c163a475 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= Date: Wed, 29 Jul 2026 08:56:56 +0000 Subject: [PATCH 04/20] feat: lemmas about the `smallInductiveDimension` (#40879) We prove various lemmas about the `smallInductiveDimension` of a topological space, as well as interactions with the `HasSmallInductiveDimensionLT` and `HasSmallInductiveDimensionLE` typeclasses. --- Mathlib/Topology/SmallInductiveDimension.lean | 76 +++++++++++++++++-- 1 file changed, 68 insertions(+), 8 deletions(-) diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean index 811b88bf42d..b5087dd23ef 100644 --- a/Mathlib/Topology/SmallInductiveDimension.lean +++ b/Mathlib/Topology/SmallInductiveDimension.lean @@ -33,7 +33,7 @@ In this file we formalize this notion, and characterize the cases `n = 0` and `n @[expose] public section -open Set TopologicalSpace +open Set Topology TopologicalSpace /-- For a topological space, the property of having small inductive dimension less than `n : ℕ` is @@ -45,7 +45,7 @@ class inductive HasSmallInductiveDimensionLT.{u} : ∀ (X : Type u) [TopologicalSpace X], ℕ → Prop where | zero {X : Type u} [TopologicalSpace X] [IsEmpty X] : HasSmallInductiveDimensionLT X 0 | succ {X : Type u} [TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : IsTopologicalBasis s) - (h : ∀ U ∈ s, HasSmallInductiveDimensionLT ↑(frontier U) n) : + (h : ∀ U ∈ s, HasSmallInductiveDimensionLT (frontier U) n) : HasSmallInductiveDimensionLT X (n + 1) variable {X : Type*} [TopologicalSpace X] @@ -55,12 +55,8 @@ variable (X) in abbrev HasSmallInductiveDimensionLE (n : ℕ) := HasSmallInductiveDimensionLT X (n + 1) -variable (X) in -/-- The small inductive dimension of a topological space. -/ -noncomputable def smallInductiveDimension : WithBot ℕ∞ := - sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < i → HasSmallInductiveDimensionLT X i} - -lemma hasSmallInductiveDimensionLT_zero_iff : HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X := +@[simp] +theorem hasSmallInductiveDimensionLT_zero_iff : HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X := ⟨fun h ↦ by cases h; assumption, fun _ ↦ .zero⟩ @[deprecated (since := "2026-06-21")] @@ -101,3 +97,67 @@ theorem HasSmallInductiveDimensionLT.hasSmallInductiveDimensionLE {n : ℕ} instance (n : ℕ) [IsEmpty X] : HasSmallInductiveDimensionLT X n := .mono zero_le <| hasSmallInductiveDimensionLT_zero_iff.2 ‹_› + +/-! ### Small inductive dimension -/ + +variable (X) in +/-- The small inductive dimension of a topological space. -/ +noncomputable def smallInductiveDimension : WithBot ℕ∞ := + sInf {n | ∀ i : ℕ, n < i → HasSmallInductiveDimensionLT X i} + +private theorem hasSmallInductiveDimensionLT_of_smallInductiveDimension_lt {n : ℕ} + (h : smallInductiveDimension X < n) : HasSmallInductiveDimensionLT X n := by + contrapose! h + simp only [smallInductiveDimension, le_sInf_iff, mem_ofPred_eq] + intro a ha + contrapose! ha + exact ⟨n, ha, h⟩ + +private theorem hasSmallInductiveDimensionLE_of_smallInductiveDimension_le {n : ℕ} + (h : smallInductiveDimension X ≤ n) : HasSmallInductiveDimensionLE X n := by + apply hasSmallInductiveDimensionLT_of_smallInductiveDimension_lt (h.trans_lt _) + exact_mod_cast n.lt_add_one + +theorem smallInductiveDimension_le_iff {n : ℕ} : + smallInductiveDimension X ≤ n ↔ HasSmallInductiveDimensionLE X n where + mp := hasSmallInductiveDimensionLE_of_smallInductiveDimension_le + mpr h := sInf_le fun m hm ↦ .mono (by simpa using hm) h + +theorem smallInductiveDimension_lt_iff {n : ℕ} : + smallInductiveDimension X < n ↔ HasSmallInductiveDimensionLT X n where + mp := hasSmallInductiveDimensionLT_of_smallInductiveDimension_lt + mpr h := by + cases n with + | zero => + rw [smallInductiveDimension, csInf_eq_bot_of_bot_mem] + · simp + · exact fun _ _ ↦ h.mono zero_le + | succ n => + apply (smallInductiveDimension_le_iff.2 h).trans_lt + exact_mod_cast n.lt_add_one + +variable (X) in +theorem smallInductiveDimension_le (n : ℕ) [H : HasSmallInductiveDimensionLE X n] : + smallInductiveDimension X ≤ n := + smallInductiveDimension_le_iff.2 H + +variable (X) in +theorem smallInductiveDimension_lt (n : ℕ) [H : HasSmallInductiveDimensionLT X n] : + smallInductiveDimension X < n := + smallInductiveDimension_lt_iff.2 H + +theorem smallInductiveDimension_eq (n : ℕ) + (hle : HasSmallInductiveDimensionLE X n) (hlt : ¬ HasSmallInductiveDimensionLT X n) : + smallInductiveDimension X = n := by + apply (smallInductiveDimension_le_iff.2 hle).antisymm + rwa [← not_lt, smallInductiveDimension_lt_iff] + +@[simp] +theorem smallInductiveDimension_eq_bot : smallInductiveDimension X = ⊥ ↔ IsEmpty X := by + simp_rw [← hasSmallInductiveDimensionLT_zero_iff, ← smallInductiveDimension_lt_iff, + WithBot.lt_coe_bot.symm, bot_eq_zero', Nat.cast_zero, WithBot.coe_zero] + +variable (X) in +@[simp] +theorem smallInductiveDimension_of_isEmpty [IsEmpty X] : smallInductiveDimension X = ⊥ := + smallInductiveDimension_eq_bot.2 ‹_› From 6d8afdba83d18ca3e6c8a5838ef7d5d5d548cb09 Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:56:59 +0000 Subject: [PATCH 05/20] chore: remove some (triple) underscore soup (#42208) Inspired by #42205. I searched for ` _ _ _]` in vscode and manually went through all ~25 and see if they could be removed (and in some cases some minor style improvement). For ` _ _]` it is already over 100, so that work ought to be automatised Co-authored-by: Batixx --- Mathlib/Algebra/Group/Defs.lean | 2 +- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean | 6 +++--- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean | 2 +- Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean | 2 +- Mathlib/Data/Finset/Density.lean | 2 +- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean | 2 +- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean | 2 +- Mathlib/Topology/UniformSpace/Ascoli.lean | 2 +- 8 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 3111721ff63..72942dc5428 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -1117,7 +1117,7 @@ theorem inv_eq_one_div (x : G) : x⁻¹ = 1 / x := by rw [div_eq_mul_inv, one_mu @[to_additive] theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c) := by - rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _] + rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc] @[to_additive (attr := simp)] theorem one_div (a : G) : 1 / a = a⁻¹ := diff --git a/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean index 1defc05fd53..ce9b8010738 100644 --- a/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean +++ b/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean @@ -811,7 +811,7 @@ instance [AddMonoid k] [SMul S₁ S₂] [SMulZeroClass S₁ k] [SMulZeroClass S instance [AddMonoid k] [SMulZeroClass S₁ k] [SMulZeroClass S₂ k] [SMulCommClass S₁ S₂ k] : SMulCommClass S₁ S₂ (SkewMonoidAlgebra k G) := - ⟨fun _ _ ⟨_⟩ ↦ by simp_rw [← ofCoeff_smul, smul_comm _ _ _]⟩ + ⟨fun _ _ ⟨_⟩ ↦ by simp_rw [← ofCoeff_smul, smul_comm]⟩ instance [AddMonoid k] [SMulZeroClass S k] [SMulZeroClass Sᵐᵒᵖ k] [IsCentralScalar S k] : IsCentralScalar S (SkewMonoidAlgebra k G) := @@ -897,7 +897,7 @@ theorem coeff_mul_antidiagonal_of_finset (f g : SkewMonoidAlgebra k G) (x : G) let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0 calc (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x - _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _] + _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product] _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support, @@ -923,7 +923,7 @@ theorem coeff_mul_antidiagonal_finsum (f g : SkewMonoidAlgebra k G) (x : G) : let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0 calc (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x - _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _] + _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product] _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support, diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean index eef257f5abb..b7d7e35ae75 100644 --- a/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean +++ b/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean @@ -745,7 +745,7 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : ⦋ by_cases h' : x ≤ Fin.castSucc i · rw [Fin.predAbove_of_le_castSucc i x h'] dsimp [δ] - rw [Fin.succAbove_of_castSucc_lt _ _ _] + rw [Fin.succAbove_of_castSucc_lt] · rw [Fin.castSucc_castPred] · exact (Fin.castSucc_lt_succ_iff.mpr h') · simp only [not_le] at h' diff --git a/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean b/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean index f847a89d7e6..92375dd9017 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean @@ -36,7 +36,7 @@ instance reflectsIsomorphisms_forget₂ [HasForget₂ C D] [(forget C).ReflectsI { reflects := fun X Y f {i} => by have i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _ have : IsIso ((forget C).map f) := by - rwa [← @HasForget₂.forget_comp C _ _ _ _ _ D _ _ _ _ _] + rwa [← @HasForget₂.forget_comp (C := C) (D := D)] apply isIso_of_reflects_iso f (forget C) } end CategoryTheory diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean index 847080985a9..3c837b046b5 100644 --- a/Mathlib/Data/Finset/Density.lean +++ b/Mathlib/Data/Finset/Density.lean @@ -167,7 +167,7 @@ lemma dens_inter_add_dens_union (s t : Finset α) : dens (s ∩ t) + dens (s ∪ t) = dens s + dens t := by rw [add_comm, dens_union_add_dens_inter] @[simp] lemma dens_union_of_disjoint (h : Disjoint s t) : dens (s ∪ t) = dens s + dens t := by - rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _] + rw [← disjUnion_eq_union s t h, dens_disjUnion] lemma dens_sdiff_add_dens_eq_dens (h : s ⊆ t) : dens (t \ s) + dens s = dens t := by simp [dens, ← card_sdiff_add_card_eq_card h, add_div] diff --git a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean index 3b52650f79d..970a536cb95 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean @@ -152,7 +152,7 @@ theorem one_left (b : ℕ) : J(1 | b) = 1 := /-- The Jacobi symbol is multiplicative in its first argument. -/ theorem mul_left (a₁ a₂ : ℤ) (b : ℕ) : J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b) := by - simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _] + simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul] exact List.prod_map_mul (l := (primeFactorsList b).attach) (f := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₁) (g := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₂) diff --git a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean index 3c893ab7a53..2e66a2bfa54 100644 --- a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean +++ b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean @@ -139,7 +139,7 @@ theorem norm_nonneg (x : ℤ[i]) : 0 ≤ norm x := Zsqrtd.norm_nonneg (by simp) _ @[simp] -theorem norm_eq_zero {x : ℤ[i]} : norm x = 0 ↔ x = 0 := by rw [← @Int.cast_inj ℝ _ _ _]; simp +theorem norm_eq_zero {x : ℤ[i]} : norm x = 0 ↔ x = 0 := by rw [← Int.cast_inj (α := ℝ)]; simp theorem norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0 := by rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]; simp [norm_nonneg] diff --git a/Mathlib/Topology/UniformSpace/Ascoli.lean b/Mathlib/Topology/UniformSpace/Ascoli.lean index 716a7b82de3..5c7c248f62f 100644 --- a/Mathlib/Topology/UniformSpace/Ascoli.lean +++ b/Mathlib/Topology/UniformSpace/Ascoli.lean @@ -501,7 +501,7 @@ theorem ArzelaAscoli.isCompact_of_equicontinuous suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by rw [isCompact_iff_compactSpace] at hS1 ⊢ exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace - rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _] + rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi] · exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal · exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton) · exact fun _ ↦ id From 7630dcddf054c350d73150d536390a15dbd1afc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 29 Jul 2026 08:57:01 +0000 Subject: [PATCH 06/20] chore(AlgebraicTopology/SimplexCategory): delete synthesizable instances (#42222) `inferInstance` works in place of `inferInstanceAs` in both places. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Comparator-related.20import.20subtleties/with/613349677) --- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean b/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean index b7d7e35ae75..fef916f767c 100644 --- a/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean +++ b/Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean @@ -596,12 +596,6 @@ instance : ConcreteCategory SimplexCategory (fun i j => Fin (i.len + 1) →o Fin hom := Hom.toOrderHom ofHom f := Hom.mk f -instance (x : SimplexCategory) : Fintype (ToType x) := - inferInstanceAs (Fintype (Fin _)) - -instance (x : SimplexCategory) (n : ℕ) : OfNat (ToType x) n := - inferInstanceAs (OfNat (Fin _) n) - lemma toType_apply (x : SimplexCategory) : ToType x = Fin (x.len + 1) := rfl @[simp] From 53a560fefea0a9525485d49d9f1c811ed89ae6f0 Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 29 Jul 2026 11:09:52 +0000 Subject: [PATCH 07/20] chore: rename `QuotientAddGroup.mk_out_eq_mul` to `mk_out_eq_add` (#41654) The additive lemma states `(mk g).out = g + h`, so by the `to_additive` naming convention its name should end in `add`, not `mul`. Rename it to `QuotientAddGroup.mk_out_eq_add` (a copy-paste error inherited from mathlib3) and deprecate the old name. --- Mathlib/GroupTheory/Coset/Defs.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Coset/Defs.lean b/Mathlib/GroupTheory/Coset/Defs.lean index 2af03b2d5f2..e50fde599d2 100644 --- a/Mathlib/GroupTheory/Coset/Defs.lean +++ b/Mathlib/GroupTheory/Coset/Defs.lean @@ -209,7 +209,7 @@ variable (s) /-- It can be useful to write `obtain ⟨h, H⟩ := mk_out_eq_mul ...`, and then `rw [H]` or `simp_rw [H]` or `simp only [H]`. In order for `simp_rw` and `simp only` to work, this lemma is stated in terms of an arbitrary `h : s`, rather than the specific `h = g⁻¹ * (mk g).out`. -/ -@[to_additive QuotientAddGroup.mk_out_eq_mul] +@[to_additive] theorem mk_out_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h := ⟨⟨g⁻¹ * (mk g).out, QuotientGroup.eq.mp (mk g).out_eq'.symm⟩, by rw [mul_inv_cancel_left]⟩ @@ -249,6 +249,9 @@ theorem preimage_mk_one (N : Subgroup α) : end QuotientGroup +@[deprecated (since := "2026-07-12")] +alias QuotientAddGroup.mk_out_eq_mul := QuotientAddGroup.mk_out_eq_add + namespace Subgroup open QuotientGroup From d160677fd383cf76893d1cba56bf84f251052956 Mon Sep 17 00:00:00 2001 From: Michael Rothgang <10105016+grunweg@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:40:37 +0000 Subject: [PATCH 08/20] chore(Archive): convert to the module system (#42010) This is just a general good practice these days. Two specific reasons are: - the module system makes thing faster, for example by reducing how much stuff has to be imported. - In the long run, we want to only support the module system, and not any non-module system uses of mathlib. #41950 signals this. That way, we can use no_expose, without needing to worry about uses without the module system where the definition will be exposed anyways. The migration is mostly mechanical, akin to what `modulize.lean` would do: make all imports `public`, and add `@[expose] public section` at the beginning of each file. (In a few cases of files without definitions, omit the expose attribute.) Inspired by #36236; re-done by hand. All files omitted there are actually fine to hand-convert. --- Counterexamples.lean | 60 ++++++++++--------- Counterexamples/AharoniKorman.lean | 16 +++-- .../CanonicallyOrderedCommSemiringTwoMul.lean | 8 ++- Counterexamples/CharPZeroNeCharZero.lean | 7 ++- .../CliffordAlgebraNotInjective.lean | 19 +++--- Counterexamples/Cyclotomic105.lean | 8 ++- Counterexamples/DimensionPolynomial.lean | 12 ++-- Counterexamples/DirectSumIsInternal.lean | 12 ++-- ...DiscreteTopologyNonDiscreteUniformity.lean | 6 +- Counterexamples/EulerSumOfPowers.lean | 5 +- Counterexamples/Girard.lean | 7 ++- Counterexamples/HeawoodUnitDistance.lean | 8 ++- Counterexamples/HomogeneousPrimeNotPrime.lean | 12 ++-- Counterexamples/InvertibleModuleNotIdeal.lean | 10 +++- .../IrrationalPowerOfIrrational.lean | 9 +-- Counterexamples/MapFloor.lean | 15 +++-- Counterexamples/MonicNonRegular.lean | 6 +- Counterexamples/Motzkin.lean | 8 ++- Counterexamples/NowhereDifferentiable.lean | 11 ++-- .../OrderedCancelAddCommMonoidWithBounds.lean | 6 +- Counterexamples/PeanoCurve.lean | 10 +++- Counterexamples/Phillips.lean | 15 +++-- Counterexamples/PolynomialIsDomain.lean | 14 +++-- Counterexamples/Pseudoelement.lean | 11 ++-- Counterexamples/QuadraticForm.lean | 6 +- .../SeminormLatticeNotDistrib.lean | 7 ++- .../SeparableNotSecondCountable.lean | 6 +- Counterexamples/SorgenfreyLine.lean | 23 ++++--- Counterexamples/TopologistsSineCurve.lean | 8 ++- .../ZeroDivisorsInAddMonoidAlgebras.lean | 14 +++-- 30 files changed, 216 insertions(+), 143 deletions(-) diff --git a/Counterexamples.lean b/Counterexamples.lean index 7a514ba1e05..80c2aea1aec 100644 --- a/Counterexamples.lean +++ b/Counterexamples.lean @@ -1,29 +1,31 @@ -import Counterexamples.AharoniKorman -import Counterexamples.CanonicallyOrderedCommSemiringTwoMul -import Counterexamples.CharPZeroNeCharZero -import Counterexamples.CliffordAlgebraNotInjective -import Counterexamples.Cyclotomic105 -import Counterexamples.DimensionPolynomial -import Counterexamples.DirectSumIsInternal -import Counterexamples.DiscreteTopologyNonDiscreteUniformity -import Counterexamples.EulerSumOfPowers -import Counterexamples.Girard -import Counterexamples.HeawoodUnitDistance -import Counterexamples.HomogeneousPrimeNotPrime -import Counterexamples.InvertibleModuleNotIdeal -import Counterexamples.IrrationalPowerOfIrrational -import Counterexamples.MapFloor -import Counterexamples.MonicNonRegular -import Counterexamples.Motzkin -import Counterexamples.NowhereDifferentiable -import Counterexamples.OrderedCancelAddCommMonoidWithBounds -import Counterexamples.PeanoCurve -import Counterexamples.Phillips -import Counterexamples.PolynomialIsDomain -import Counterexamples.Pseudoelement -import Counterexamples.QuadraticForm -import Counterexamples.SeminormLatticeNotDistrib -import Counterexamples.SeparableNotSecondCountable -import Counterexamples.SorgenfreyLine -import Counterexamples.TopologistsSineCurve -import Counterexamples.ZeroDivisorsInAddMonoidAlgebras +module -- shake: keep-all --deprecated_module: ignore + +public import Counterexamples.AharoniKorman +public import Counterexamples.CanonicallyOrderedCommSemiringTwoMul +public import Counterexamples.CharPZeroNeCharZero +public import Counterexamples.CliffordAlgebraNotInjective +public import Counterexamples.Cyclotomic105 +public import Counterexamples.DimensionPolynomial +public import Counterexamples.DirectSumIsInternal +public import Counterexamples.DiscreteTopologyNonDiscreteUniformity +public import Counterexamples.EulerSumOfPowers +public import Counterexamples.Girard +public import Counterexamples.HeawoodUnitDistance +public import Counterexamples.HomogeneousPrimeNotPrime +public import Counterexamples.InvertibleModuleNotIdeal +public import Counterexamples.IrrationalPowerOfIrrational +public import Counterexamples.MapFloor +public import Counterexamples.MonicNonRegular +public import Counterexamples.Motzkin +public import Counterexamples.NowhereDifferentiable +public import Counterexamples.OrderedCancelAddCommMonoidWithBounds +public import Counterexamples.PeanoCurve +public import Counterexamples.Phillips +public import Counterexamples.PolynomialIsDomain +public import Counterexamples.Pseudoelement +public import Counterexamples.QuadraticForm +public import Counterexamples.SeminormLatticeNotDistrib +public import Counterexamples.SeparableNotSecondCountable +public import Counterexamples.SorgenfreyLine +public import Counterexamples.TopologistsSineCurve +public import Counterexamples.ZeroDivisorsInAddMonoidAlgebras diff --git a/Counterexamples/AharoniKorman.lean b/Counterexamples/AharoniKorman.lean index a7f42ed111c..25abfb4d362 100644 --- a/Counterexamples/AharoniKorman.lean +++ b/Counterexamples/AharoniKorman.lean @@ -3,12 +3,14 @@ Copyright (c) 2024 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta -/ -import Mathlib.Algebra.Order.Field.Basic -import Mathlib.Algebra.Order.Field.Rat -import Mathlib.Data.Setoid.Partition -import Mathlib.Order.Filter.AtTopBot.Basic -import Mathlib.Order.Interval.Set.Infinite -import Mathlib.Order.WellFoundedSet +module + +public import Mathlib.Algebra.Order.Field.Basic +public import Mathlib.Algebra.Order.Field.Rat +public import Mathlib.Data.Setoid.Partition +public import Mathlib.Order.Filter.AtTopBot.Basic +public import Mathlib.Order.Interval.Set.Infinite +public import Mathlib.Order.WellFoundedSet /-! # Disproof of the Aharoni–Korman conjecture @@ -67,6 +69,8 @@ aim of reaching a contradiction (as then, no such partition can exist). We may f we have a contradiction (`no_spinalMap`), and therefore show that no spinal map exists. -/ +@[expose] public section + attribute [aesop 2 simp] Set.subset_def Finset.subset_iff /-- A type synonym on ℕ³ on which we will construct Hollom's partial order P_5. -/ diff --git a/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean b/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean index 16029d0bd99..fc6001a2079 100644 --- a/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean +++ b/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean @@ -3,8 +3,10 @@ Copyright (c) 2021 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ -import Mathlib.Algebra.Ring.Subsemiring.Order -import Mathlib.Data.ZMod.Basic +module + +public import Mathlib.Algebra.Ring.Subsemiring.Order +public import Mathlib.Data.ZMod.Basic /-! # A canonically ordered commutative semiring where multiplication by 2 is not injective @@ -24,7 +26,7 @@ Reference: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology -/ - +@[expose] public section namespace Counterexample diff --git a/Counterexamples/CharPZeroNeCharZero.lean b/Counterexamples/CharPZeroNeCharZero.lean index fcb0eb5e258..4532e2e779d 100644 --- a/Counterexamples/CharPZeroNeCharZero.lean +++ b/Counterexamples/CharPZeroNeCharZero.lean @@ -3,8 +3,10 @@ Copyright (c) 2022 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa, Eric Wieser -/ -import Mathlib.Algebra.CharP.Lemmas -import Mathlib.Algebra.Ring.PUnit +module + +public import Mathlib.Algebra.CharP.Lemmas +public import Mathlib.Algebra.Ring.PUnit /-! # `CharP R 0` and `CharZero R` need not coincide for semirings @@ -19,6 +21,7 @@ This file shows that there are semirings `R` for which `CharP R 0` holds and `Ch The example is `{0, 1}` with saturating addition. -/ +@[expose] public section namespace Counterexample diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean index f47f319b0e9..f6c2d638551 100644 --- a/Counterexamples/CliffordAlgebraNotInjective.lean +++ b/Counterexamples/CliffordAlgebraNotInjective.lean @@ -3,12 +3,14 @@ Copyright (c) 2021 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ -import Mathlib.Algebra.CharP.Pi -import Mathlib.Algebra.CharP.Quotient -import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction -import Mathlib.RingTheory.MvPolynomial.Basic -import Mathlib.RingTheory.MvPolynomial.Ideal -import Mathlib.Tactic.Ring.NamePolyVars +module + +public import Mathlib.Algebra.CharP.Pi +public import Mathlib.Algebra.CharP.Quotient +public import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction +public import Mathlib.RingTheory.MvPolynomial.Basic +public import Mathlib.RingTheory.MvPolynomial.Ideal +public import Mathlib.Tactic.Ring.NamePolyVars /-! # `algebraMap R (CliffordAlgebra Q)` is not always injective. @@ -30,10 +32,9 @@ As a bonus result, we also show `BilinMap.not_forall_toQuadraticMap_surjective`: are quadratic forms that cannot be expressed via even non-symmetric bilinear forms. -/ -noncomputable section +@[expose] public noncomputable section -open LinearMap (BilinForm) -open LinearMap (BilinMap) +open LinearMap (BilinForm BilinMap) name_poly_vars X, Y, Z over ZMod 2 diff --git a/Counterexamples/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean index 8d32ce2328e..abf3c54a2e3 100644 --- a/Counterexamples/Cyclotomic105.lean +++ b/Counterexamples/Cyclotomic105.lean @@ -3,8 +3,10 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Riccardo Brasca -/ -import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic -import Mathlib.Tactic.NormNum.Prime +module + +public import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic +public import Mathlib.Tactic.NormNum.Prime /-! # Not all coefficients of cyclotomic polynomials are -1, 0, or 1 @@ -14,9 +16,9 @@ theorem `not_forall_coeff_cyclotomic_neg_one_zero_one`. We prove this with the c `coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2`. -/ +@[expose] public section open Nat (properDivisors) - open Finset namespace Counterexample diff --git a/Counterexamples/DimensionPolynomial.lean b/Counterexamples/DimensionPolynomial.lean index e3b0ec0ba20..7777b22e58a 100644 --- a/Counterexamples/DimensionPolynomial.lean +++ b/Counterexamples/DimensionPolynomial.lean @@ -3,10 +3,12 @@ Copyright (c) 2025 Jingting Wang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jingting Wang -/ -import Mathlib.RingTheory.KrullDimension.Polynomial -import Mathlib.RingTheory.KrullDimension.LocalRing -import Mathlib.FieldTheory.RatFunc.AsPolynomial -import Mathlib.RingTheory.PowerSeries.Inverse +module + +public import Mathlib.RingTheory.KrullDimension.Polynomial +public import Mathlib.RingTheory.KrullDimension.LocalRing +public import Mathlib.FieldTheory.RatFunc.AsPolynomial +public import Mathlib.RingTheory.PowerSeries.Inverse /-! # Krull dimension of polynomial ring @@ -22,6 +24,8 @@ We define the commutative ring `A` as `{f ∈ k(t)⟦Y⟧ | f(0) ∈ k}` for a f -/ +@[expose] public section + namespace Counterexample namespace DimensionPolynomial diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean index b2f95cb70a4..638eaae576d 100644 --- a/Counterexamples/DirectSumIsInternal.lean +++ b/Counterexamples/DirectSumIsInternal.lean @@ -3,10 +3,12 @@ Copyright (c) 2021 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser, Kevin Buzzard -/ -import Mathlib.Algebra.DirectSum.Module -import Mathlib.Algebra.Group.ConjFinite -import Mathlib.Data.Fintype.Lattice -import Mathlib.Tactic.FinCases +module + +public import Mathlib.Algebra.DirectSum.Module +public import Mathlib.Algebra.Group.ConjFinite +public import Mathlib.Data.Fintype.Lattice +public import Mathlib.Tactic.FinCases /-! # Not all complementary decompositions of a module over a semiring make up a direct sum @@ -19,6 +21,8 @@ This file demonstrates why `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_ take `Ring R` and not `Semiring R`. -/ +public section + namespace Counterexample theorem UnitsInt.one_ne_neg_one : (1 : ℤˣ) ≠ -1 := by decide diff --git a/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean b/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean index bd6548b6cf5..1458342e806 100644 --- a/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean +++ b/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean @@ -3,7 +3,9 @@ Copyright (c) 2024 Filippo A. E. Nuccio. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Filippo A. E. Nuccio -/ -import Mathlib.Analysis.SpecificLimits.Basic +module + +public import Mathlib.Analysis.SpecificLimits.Basic /-! # Discrete uniformities and discrete topology @@ -75,6 +77,8 @@ inequality) to explicit subsets, many proofs are easily closed by `aesop` or `om * [N. Bourbaki, *General Topology*, Chapter II][bourbaki1966] -/ +@[expose] public section + open Set Function Filter Metric /- We remove the "usual" instances of (discrete) topological space and of (discrete) uniform space diff --git a/Counterexamples/EulerSumOfPowers.lean b/Counterexamples/EulerSumOfPowers.lean index 69b1fba2b18..1e8e2baef70 100644 --- a/Counterexamples/EulerSumOfPowers.lean +++ b/Counterexamples/EulerSumOfPowers.lean @@ -3,7 +3,9 @@ Copyright (c) 2025 Snir Broshi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Snir Broshi, Michael Stoll -/ -import Mathlib.NumberTheory.FLT.Three +module + +public import Mathlib.NumberTheory.FLT.Three /-! # Euler's sum of powers conjecture @@ -27,6 +29,7 @@ http://euler.free.fr/ https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf -/ +@[expose] public section namespace Counterexample diff --git a/Counterexamples/Girard.lean b/Counterexamples/Girard.lean index 16ea6890ecf..961031ec7d9 100644 --- a/Counterexamples/Girard.lean +++ b/Counterexamples/Girard.lean @@ -3,8 +3,10 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Mathlib.Logic.Basic -import Mathlib.Data.Set.Defs +module + +public import Mathlib.Logic.Basic +public import Mathlib.Data.Set.Defs /-! # Girard's paradox @@ -25,6 +27,7 @@ Based on Watkins' LF implementation of Hurkens' simplification of Girard's parad * `girard`: there are no Girard universes. -/ +@[expose] public section namespace Counterexample diff --git a/Counterexamples/HeawoodUnitDistance.lean b/Counterexamples/HeawoodUnitDistance.lean index 0d199e6a6a4..a909e32afb4 100644 --- a/Counterexamples/HeawoodUnitDistance.lean +++ b/Counterexamples/HeawoodUnitDistance.lean @@ -3,8 +3,10 @@ Copyright (c) 2025 Jeremy Tan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Tan -/ -import Mathlib.Analysis.InnerProductSpace.PiL2 -import Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic +module + +public import Mathlib.Analysis.InnerProductSpace.PiL2 +public import Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic /-! # A simple planar unit-distance embedding of the Heawood graph @@ -25,6 +27,8 @@ and Jeremy Tan [in August 2025](https://github.com/Parcly-Taxel/Shibuya/commit/b Its coordinates are polynomials in the unique real root of `2c^3 + 3c + 1`. -/ +@[expose] public section + namespace SimpleGraph open Finset diff --git a/Counterexamples/HomogeneousPrimeNotPrime.lean b/Counterexamples/HomogeneousPrimeNotPrime.lean index f6ad1b8b76c..7b997682cd8 100644 --- a/Counterexamples/HomogeneousPrimeNotPrime.lean +++ b/Counterexamples/HomogeneousPrimeNotPrime.lean @@ -3,10 +3,12 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Eric Wieser, Jujian Zhang -/ -import Mathlib.Algebra.Divisibility.Finite -import Mathlib.Algebra.Divisibility.Prod -import Mathlib.Algebra.GroupWithZero.Units.Fintype -import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal +module + +public import Mathlib.Algebra.Divisibility.Finite +public import Mathlib.Algebra.Divisibility.Prod +public import Mathlib.Algebra.GroupWithZero.Units.Fintype +public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal /-! # A homogeneous ideal that is homogeneously prime but not prime @@ -25,12 +27,12 @@ structure of linear ordered additive commutative monoid by setting `0 + 0 = 0` a and not prime. But it is homogeneously prime, i.e. if `(a, b), (c, d)` are two homogeneous elements then `(a, b) * (c, d) ∈ I` implies either `(a, b) ∈ I` or `(c, d) ∈ I`. - ## Tags homogeneous, prime -/ +@[expose] public section namespace Counterexample diff --git a/Counterexamples/InvertibleModuleNotIdeal.lean b/Counterexamples/InvertibleModuleNotIdeal.lean index bf54f34f6c1..8fb5981cf31 100644 --- a/Counterexamples/InvertibleModuleNotIdeal.lean +++ b/Counterexamples/InvertibleModuleNotIdeal.lean @@ -3,9 +3,11 @@ Copyright (c) 2025 Junyan Xu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Junyan Xu -/ -import Mathlib.Algebra.TrivSqZeroExt.Basic -import Mathlib.Data.DFinsupp.Module -import Mathlib.RingTheory.PicardGroup +module + +public import Mathlib.Algebra.TrivSqZeroExt.Basic +public import Mathlib.Data.DFinsupp.Module +public import Mathlib.RingTheory.PicardGroup /-! # A class of examples of invertible modules that are not isomorphic to ideals @@ -13,6 +15,8 @@ import Mathlib.RingTheory.PicardGroup References: https://math.stackexchange.com/a/5090562 or https://mathoverflow.net/a/499258 -/ +public section + variable (R : Type*) [CommRing R] /-- The trivial square-zero extension of a commutative ring R given by the direct sum diff --git a/Counterexamples/IrrationalPowerOfIrrational.lean b/Counterexamples/IrrationalPowerOfIrrational.lean index f61b83cdfcb..1598c78874e 100644 --- a/Counterexamples/IrrationalPowerOfIrrational.lean +++ b/Counterexamples/IrrationalPowerOfIrrational.lean @@ -3,8 +3,10 @@ Copyright (c) 2024 Seewoo Lee. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Seewoo Lee -/ -import Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import Mathlib.NumberTheory.Real.Irrational +module + +public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +public import Mathlib.NumberTheory.Real.Irrational /-! # An irrational power of an irrational number need not be irrational @@ -16,7 +18,6 @@ Consider `c = √2^√2`. If `c` is rational, we are done. If `c` is irrational, then `c^√2 = 2` is rational, so we are done. -/ - open Real namespace Counterexample @@ -26,7 +27,7 @@ There exist irrational `a`, `b` with rational `a^b`. Note that the positivity assumption on `a` is imposed because of the definition of `rpow` for negative bases. See `Real.rpow_def_of_neg` for more details. -/ -theorem not_irrational_rpow : +public theorem not_irrational_rpow : ¬ ∀ a b : ℝ, Irrational a → Irrational b → 0 < a → Irrational (a ^ b) := by push Not by_cases hc : Irrational (√2 ^ √2) diff --git a/Counterexamples/MapFloor.lean b/Counterexamples/MapFloor.lean index 9edd2ddce52..ccd46ac7f45 100644 --- a/Counterexamples/MapFloor.lean +++ b/Counterexamples/MapFloor.lean @@ -3,10 +3,12 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ -import Mathlib.Algebra.Order.Round -import Mathlib.Algebra.Order.Group.PiLex -import Mathlib.Algebra.Order.Hom.Ring -import Mathlib.Algebra.Polynomial.Reverse +module + +public import Mathlib.Algebra.Order.Round +public import Mathlib.Algebra.Order.Group.PiLex +public import Mathlib.Algebra.Order.Hom.Ring +public import Mathlib.Algebra.Polynomial.Reverse /-! # Floors and ceils aren't preserved under ordered ring homomorphisms @@ -35,11 +37,10 @@ But it does not preserve floors (nor ceils) as `⌊-ε⌋ = -1` while `⌊f (-ε (`IntWithEpsilon.forgetEpsilons_floor_lt`, `IntWithEpsilon.lt_forgetEpsilons_ceil`). -/ +@[expose] public noncomputable section namespace Counterexample -noncomputable section - open Function Int Polynomial /-- The integers with infinitesimals adjoined. Higher powers of `ε` are smaller than lower @@ -130,6 +131,4 @@ theorem lt_forgetEpsilons_ceil (n : ℤ) : end IntWithEpsilon -end - end Counterexample diff --git a/Counterexamples/MonicNonRegular.lean b/Counterexamples/MonicNonRegular.lean index 7efe730dd03..d32455f99d0 100644 --- a/Counterexamples/MonicNonRegular.lean +++ b/Counterexamples/MonicNonRegular.lean @@ -3,8 +3,9 @@ Copyright (c) 2023 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ +module -import Mathlib.Algebra.Polynomial.Monic +public import Mathlib.Algebra.Polynomial.Monic /-! # `Monic` does not necessarily imply `IsRegular` in a `Semiring` with no opposites @@ -23,6 +24,9 @@ The products `(X + 2) * (X + 2)` and `(X + 2) * (X + 3)` are equal to By truncation, `4, 5, 6` all mean `3` in `N`. It follows that multiplication by `(X + 2)` is not injective. -/ + +@[expose] public section + open Polynomial namespace Counterexample.NonRegular diff --git a/Counterexamples/Motzkin.lean b/Counterexamples/Motzkin.lean index 77498fd6603..f7b96bf226c 100644 --- a/Counterexamples/Motzkin.lean +++ b/Counterexamples/Motzkin.lean @@ -3,8 +3,10 @@ Copyright (c) 2025 Jeremy Tan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Tan, Heather Macbeth -/ -import Mathlib.Tactic.LinearCombination -import Mathlib.Tactic.Positivity +module + +public import Mathlib.Tactic.LinearCombination +public import Mathlib.Tactic.Positivity /-! # The Motzkin polynomial @@ -21,7 +23,7 @@ variable {K : Type*} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] /-- The **Motzkin polynomial** is nonnegative. This bivariate polynomial cannot be written as a sum of squares. -/ -lemma motzkin_polynomial_nonneg (x y : K) : +public lemma motzkin_polynomial_nonneg (x y : K) : 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1 := by by_cases hx : x = 0 · simp [hx] diff --git a/Counterexamples/NowhereDifferentiable.lean b/Counterexamples/NowhereDifferentiable.lean index 2e1abcba12e..ec3671ccf3e 100644 --- a/Counterexamples/NowhereDifferentiable.lean +++ b/Counterexamples/NowhereDifferentiable.lean @@ -3,8 +3,10 @@ Copyright (c) 2025 Weiyi Wang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weiyi Wang -/ -import Mathlib.Analysis.Real.Pi.Bounds -import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn +module + +public import Mathlib.Analysis.Real.Pi.Bounds +public import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn /-! # Weierstrass function: a function that is continuous everywhere but differentiable nowhere @@ -29,6 +31,8 @@ which is the original bound given by Karl Weierstrass. There is a better bound $ -/ +@[expose] public section + namespace NowhereDifferentiable open Real Topology Filter @@ -39,8 +43,7 @@ For real parameter $a$ and $b$, define the Weierstrass function as $$f(x) = \sum_{n=0}^\infty a^n \cos (b^n\pi x)$$ -/ -noncomputable -def weierstrass (a b x : ℝ) := ∑' n, a ^ n * cos (b ^ n * π * x) +noncomputable def weierstrass (a b x : ℝ) := ∑' n, a ^ n * cos (b ^ n * π * x) /-! ### Continuity diff --git a/Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean b/Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean index b5346725242..c1d6097a05c 100644 --- a/Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean +++ b/Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean @@ -3,8 +3,10 @@ Copyright (c) 2023 Martin Dvorak. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Martin Dvorak -/ -import Mathlib.Algebra.Order.Monoid.Defs -import Mathlib.Order.BoundedOrder.Lattice +module + +public import Mathlib.Algebra.Order.Monoid.Defs +public import Mathlib.Order.BoundedOrder.Lattice /-! # Do not combine `IsOrderedCancelAddMonoid` with `BoundedOrder` diff --git a/Counterexamples/PeanoCurve.lean b/Counterexamples/PeanoCurve.lean index cf184312534..87c36c62a51 100644 --- a/Counterexamples/PeanoCurve.lean +++ b/Counterexamples/PeanoCurve.lean @@ -3,16 +3,20 @@ Copyright (c) 2025 Vasilii Nesterov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Vasilii Nesterov -/ -import Mathlib.Analysis.Complex.Tietze -import Mathlib.Topology.MetricSpace.HausdorffAlexandroff +module + +public import Mathlib.Analysis.Complex.Tietze +public import Mathlib.Topology.MetricSpace.HausdorffAlexandroff /-! # Peano curve -This file proves the existence of a Peano curve -- continuous surjective map from the interval +This file proves the existence of a Peano curve -- a continuous surjective map from the interval `[0, 1]` onto the square `[0, 1] × [0, 1]`. -/ +public section + open scoped unitInterval /-- There is a continuous function on `ℝ` that maps the Cantor set to the square. -/ diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean index 53f57c8e186..f45f6e352eb 100644 --- a/Counterexamples/Phillips.lean +++ b/Counterexamples/Phillips.lean @@ -3,10 +3,12 @@ Copyright (c) 2021 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ -import Mathlib.Analysis.Normed.Module.HahnBanach -import Mathlib.MeasureTheory.Integral.Bochner.Set -import Mathlib.MeasureTheory.Measure.Lebesgue.Basic -import Mathlib.Topology.ContinuousMap.Bounded.Star +module + +public import Mathlib.Analysis.Normed.Module.HahnBanach +public import Mathlib.MeasureTheory.Integral.Bochner.Set +public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic +public import Mathlib.Topology.ContinuousMap.Bounded.Star /-! # A counterexample on Pettis integrability @@ -72,6 +74,7 @@ on a discrete copy of the original type, as mathlib only contains the space of a continuous functions (which is the useful one). -/ +@[expose] public noncomputable section namespace Counterexample @@ -85,8 +88,6 @@ open Cardinal (aleph) open scoped Cardinal BoundedContinuousFunction -noncomputable section - /-- A copy of a type, endowed with the discrete topology -/ def DiscreteCopy (α : Type u) : Type u := α @@ -583,6 +584,4 @@ theorem no_pettis_integral (Hcont : #ℝ = ℵ₁) : end Phillips1940 -end - end Counterexample diff --git a/Counterexamples/PolynomialIsDomain.lean b/Counterexamples/PolynomialIsDomain.lean index 5f0ecfbb6be..4e24bff1a26 100644 --- a/Counterexamples/PolynomialIsDomain.lean +++ b/Counterexamples/PolynomialIsDomain.lean @@ -3,10 +3,12 @@ Copyright (c) 2025 Junyan Xu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Junyan Xu -/ -import Mathlib.Algebra.GroupWithZero.TransferInstance -import Mathlib.Algebra.Order.Ring.Nat -import Mathlib.Algebra.Ring.Equiv -import Mathlib.RingTheory.Polynomial.Opposites +module + +public import Mathlib.Algebra.GroupWithZero.TransferInstance +public import Mathlib.Algebra.Order.Ring.Nat +public import Mathlib.Algebra.Ring.Equiv +public import Mathlib.RingTheory.Polynomial.Opposites /-! # A commutative semiring that is a domain whose polynomial semiring is not a domain @@ -18,8 +20,10 @@ As a consequence, the polynomial semiring `NatMaxAdd[X]` is not a domain, even though it has no zero-divisors other than 0. -/ +public section + /-- A type synonym for ℕ equipped with maximum as addition. -/ -def NatMaxAdd := ℕ +@[expose] def NatMaxAdd := ℕ open scoped Polynomial diff --git a/Counterexamples/Pseudoelement.lean b/Counterexamples/Pseudoelement.lean index 2bc8b8fc8a2..0924871e0c3 100644 --- a/Counterexamples/Pseudoelement.lean +++ b/Counterexamples/Pseudoelement.lean @@ -3,8 +3,10 @@ Copyright (c) 2022 Riccardo Brasca. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Riccardo Brasca -/ -import Mathlib.CategoryTheory.Abelian.Pseudoelements -import Mathlib.Algebra.Category.ModuleCat.Biproducts +module + +public import Mathlib.CategoryTheory.Abelian.Pseudoelements +public import Mathlib.Algebra.Category.ModuleCat.Biproducts /-! # Pseudoelements and pullbacks @@ -29,13 +31,12 @@ given by `t ↦ (t, 2 * t)` and `y : ℚ ⟶ ℚ ⊞ ℚ` given by `t ↦ (t, t) * [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2] -/ +@[expose] public noncomputable section open CategoryTheory.Abelian CategoryTheory CategoryTheory.Limits ModuleCat LinearMap namespace Counterexample -noncomputable section - open CategoryTheory.Abelian.Pseudoelement /-- `x` is given by `t ↦ (t, 2 * t)`. -/ @@ -118,6 +119,4 @@ theorem exist_ne_and_fst_eq_fst_and_snd_eq_snd : pseudoApply biprod.snd x = pseudoApply biprod.snd y := ⟨⟦x⟧, ⟦y⟧, mk'_x_ne_mk'_y, fst_mk'_x_eq_fst_mk'_y, snd_mk'_x_eq_snd_mk'_y⟩ -end - end Counterexample diff --git a/Counterexamples/QuadraticForm.lean b/Counterexamples/QuadraticForm.lean index b6466778a9e..16210d6f984 100644 --- a/Counterexamples/QuadraticForm.lean +++ b/Counterexamples/QuadraticForm.lean @@ -3,7 +3,9 @@ Copyright (c) 2023 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ -import Mathlib.LinearAlgebra.QuadraticForm.Basic +module + +public import Mathlib.LinearAlgebra.QuadraticForm.Basic /-! # `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2 @@ -13,6 +15,7 @@ The main result of this file is `LinearMap.BilinForm.not_injOn_toQuadraticForm_i The counterexample we use is $B (x, y) (x', y') ↦ xy' + x'y$ where `x y x' y' : ZMod 2`. -/ +@[expose] public section variable (F : Type*) [CommRing F] @@ -23,7 +26,6 @@ open LinearMap.BilinMap namespace Counterexample - /-- The bilinear form we will use as a counterexample, over some field `F` of characteristic two. -/ def B : BilinForm F (F × F) := (mul F F).compl₁₂ (fst _ _ _) (snd _ _ _) + (mul F F).compl₁₂ (snd _ _ _) (fst _ _ _) diff --git a/Counterexamples/SeminormLatticeNotDistrib.lean b/Counterexamples/SeminormLatticeNotDistrib.lean index 536a6c30ea0..5ea73a444e1 100644 --- a/Counterexamples/SeminormLatticeNotDistrib.lean +++ b/Counterexamples/SeminormLatticeNotDistrib.lean @@ -3,7 +3,9 @@ Copyright (c) 2022 Pierre-Alexandre Bazin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Pierre-Alexandre Bazin -/ -import Mathlib.Analysis.Seminorm +module + +public import Mathlib.Analysis.Seminorm /-! # The lattice of seminorms is not distributive @@ -18,8 +20,9 @@ This proves the lattice `Seminorm ℝ (ℝ × ℝ)` is not distributive. * https://en.wikipedia.org/wiki/Seminorm#Examples -/ -open Seminorm +@[expose] public section +open Seminorm open scoped NNReal namespace Counterexample diff --git a/Counterexamples/SeparableNotSecondCountable.lean b/Counterexamples/SeparableNotSecondCountable.lean index bdc8853b913..a3a19c7f0f3 100644 --- a/Counterexamples/SeparableNotSecondCountable.lean +++ b/Counterexamples/SeparableNotSecondCountable.lean @@ -3,7 +3,9 @@ Copyright (c) 2025 Yury G. Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov -/ -import Mathlib.Analysis.Real.Cardinality +module + +public import Mathlib.Analysis.Real.Cardinality /-! # Example of a linear order which is a separable space but is not a second countable topology @@ -16,6 +18,8 @@ so that the duplicate is greater than the original point and points with different real values are compared by these values. -/ +public section + open Set TopologicalSpace namespace RealProdLexBool diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean index 6618e73e90a..40a7a881d66 100644 --- a/Counterexamples/SorgenfreyLine.lean +++ b/Counterexamples/SorgenfreyLine.lean @@ -3,14 +3,16 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import Mathlib.Analysis.Real.Cardinality -import Mathlib.Order.Interval.Set.Monotone -import Mathlib.Topology.Baire.Lemmas -import Mathlib.Topology.Baire.LocallyCompactRegular -import Mathlib.Topology.EMetricSpace.Paracompact -import Mathlib.Topology.Instances.Irrational -import Mathlib.Topology.Metrizable.Urysohn -import Mathlib.Topology.Separation.NotNormal +module + +public import Mathlib.Analysis.Real.Cardinality +public import Mathlib.Order.Interval.Set.Monotone +public import Mathlib.Topology.Baire.Lemmas +public import Mathlib.Topology.Baire.LocallyCompactRegular +public import Mathlib.Topology.EMetricSpace.Paracompact +public import Mathlib.Topology.Instances.Irrational +public import Mathlib.Topology.Metrizable.Urysohn +public import Mathlib.Topology.Separation.NotNormal /-! # Sorgenfrey line @@ -32,14 +34,13 @@ Prove that the Sorgenfrey line is a paracompact space. -/ +@[expose] public noncomputable section open Set Filter TopologicalSpace open scoped Topology Cardinal namespace Counterexample -noncomputable section - /-- The Sorgenfrey line (denoted as `ℝₗ` within the `SorgenfreyLine` namespace). It is the real line with the topology space structure generated by half-open intervals `Set.Ico a b`. -/ @@ -321,6 +322,4 @@ theorem not_secondCountableTopology : ¬SecondCountableTopology ℝₗ := end SorgenfreyLine -end - end Counterexample diff --git a/Counterexamples/TopologistsSineCurve.lean b/Counterexamples/TopologistsSineCurve.lean index 15f0293b588..218afac81a1 100644 --- a/Counterexamples/TopologistsSineCurve.lean +++ b/Counterexamples/TopologistsSineCurve.lean @@ -3,8 +3,10 @@ Copyright (c) 2025 Daniele Bolla. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniele Bolla, David Loeffler -/ -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse -import Mathlib.Topology.Connected.PathConnected +module + +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse +public import Mathlib.Topology.Connected.PathConnected /-! # The "topologist's sine curve" is connected but not path-connected @@ -22,6 +24,8 @@ similar result has also been independently formalized by Vlad Tsyrklevich (https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/golf.20request.3A.20Topologist's.20sine.20curve). -/ +@[expose] public section + open Topology Filter Set Real namespace TopologistsSineCurve diff --git a/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean b/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean index 5b0f8d98d00..8243f4b33dd 100644 --- a/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean +++ b/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean @@ -3,11 +3,13 @@ Copyright (c) 2022 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ -import Mathlib.Algebra.Group.UniqueProds.Basic -import Mathlib.Algebra.MonoidAlgebra.Defs -import Mathlib.Algebra.Ring.GeomSum -import Mathlib.Data.Finsupp.Lex -import Mathlib.Data.ZMod.Basic +module + +public import Mathlib.Algebra.Group.UniqueProds.Basic +public import Mathlib.Algebra.MonoidAlgebra.Defs +public import Mathlib.Algebra.Ring.GeomSum +public import Mathlib.Data.Finsupp.Lex +public import Mathlib.Data.ZMod.Basic /-! # Examples of zero-divisors in `AddMonoidAlgebra`s @@ -40,7 +42,7 @@ finitely supported function is lexicographic, matching the list notation. The i `[1, 1] > [1, 0]`. -/ - +@[expose] public section open Finsupp hiding single open AddMonoidAlgebra From e631b64438d263de54e682d9ee63d84dbb010473 Mon Sep 17 00:00:00 2001 From: Thomas Browning <13339017+tb65536@users.noreply.github.com> Date: Wed, 29 Jul 2026 13:38:42 +0000 Subject: [PATCH 09/20] chore(Combinatorics/SimpleGraph/StronglyRegular): fix statement of `conway_99` (#42233) Kevin's Claude noticed that the `proof_wanted` for `conway_99` is misformalized. It asserts the existence of a simple graph `g` but then refers to the variable `G`. Co-authored-by: tb65536 --- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean index f982dd2b27d..9bea39c519e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean +++ b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean @@ -82,7 +82,8 @@ theorem IsSRGWith.ediam_eq_two [Nontrivial V] (h : G.IsSRGWith n k ℓ μ) (ht : /-- **Conway's 99-graph problem** (from https://oeis.org/A248380/a248380.pdf) can be reformulated as the existence of a strongly regular graph with params (99, 14, 1, 2). This is an open problem, and has no known proof of existence. -/ -proof_wanted conway_99 : ∃ α : Type*, ∃ (g : SimpleGraph α), IsSRGWith G 99 14 1 2 +proof_wanted conway_99 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α) (_ : DecidableRel g.Adj), + IsSRGWith g 99 14 1 2 variable [DecidableEq V] From edc39bf7bcc706ba243ae824adaa60fff00416db Mon Sep 17 00:00:00 2001 From: Thomas Browning <13339017+tb65536@users.noreply.github.com> Date: Wed, 29 Jul 2026 13:56:48 +0000 Subject: [PATCH 10/20] chore(NumberTheory/RamificationInertia/Basic): deprecate file (#41248) This PR deprecates `NumberTheory/RamificationInertia/Basic.lean` in favor of `RingTheory/RamificationInertia/Basic.lean`. Co-authored-by: tb65536 --- .../RamificationInertia/Basic.lean | 46 ++++++++++++++++--- 1 file changed, 40 insertions(+), 6 deletions(-) diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean index 39a7c21aa4a..508511d2346 100644 --- a/Mathlib/NumberTheory/RamificationInertia/Basic.lean +++ b/Mathlib/NumberTheory/RamificationInertia/Basic.lean @@ -43,6 +43,8 @@ leaving `p` and `P` implicit. -/ +deprecated_module "Use RingTheory.RamificationInertia.Basic" (since := "2026-07-01") + @[expose] public section @@ -87,6 +89,7 @@ Here, More precisely, we avoid quotients in this statement and instead require that `b ∪ pS` spans `S`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S] [IsTorsionFree R K] (hp : p ≠ ⊤) (b : Set S) @@ -185,6 +188,7 @@ The statement we prove is actually slightly more general: * it suffices that the inclusion `algebraMap R S : R → S` is nontrivial * the function `f' : V'' → V'` doesn't need to be injective -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem FinrankQuotientMap.linearIndependent_of_nontrivial [IsDedekindDomain R] (hRS : RingHom.ker (algebraMap R S) ≠ ⊤) (F : V'' →ₗ[R] V) (hf : Function.Injective F) (f' : V'' →ₗ[R] V') {ι : Type*} {b : ι → V''} (hb' : LinearIndependent S (f' ∘ b)) : @@ -221,6 +225,7 @@ variable (L) /-- If `p` is a maximal ideal of `R`, and `S` is the integral closure of `R` in `L`, then the dimension `[S/pS : R/p]` is equal to `[Frac(S) : Frac(R)]`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem finrank_quotient_map [IsDomain S] [IsDedekindDomain R] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S] : @@ -275,10 +280,11 @@ local notation "e" => ramificationIdx' p P /-- `R / p` has a canonical map to `S / (P ^ e)`, where `e` is the ramification index of `P` over `p`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable instance Quotient.algebraQuotientPowRamificationIdx : Algebra (R ⧸ p) (S ⧸ P ^ e) := Quotient.algebraQuotientOfLEComap (Ideal.map_le_iff_le_comap.mp le_pow_ramificationIdx') -@[simp] +@[simp, deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Quotient.algebraMap_quotient_pow_ramificationIdx (x : R) : algebraMap (R ⧸ p) (S ⧸ P ^ e) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk (P ^ e) (f x) := rfl @@ -286,20 +292,21 @@ theorem Quotient.algebraMap_quotient_pow_ramificationIdx (x : R) : This can't be an instance since the map `f : R → S` is generally not inferable. -/ -@[instance_reducible] +@[instance_reducible, + deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] def Quotient.algebraQuotientOfRamificationIdxNeZero [hfp : NeZero e] : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap (le_comap_of_ramificationIdx'_ne_zero hfp.out) attribute [local instance] Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero -@[simp] +@[simp, deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Quotient.algebraMap_quotient_of_ramificationIdx_neZero [NeZero e] (x : R) : algebraMap (R ⧸ p) (S ⧸ P) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk P (f x) := rfl /-- The inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)`. -/ -@[simps] +@[simps, deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def powQuotSuccInclusion (i : ℕ) : Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1)) →ₗ[R ⧸ p] Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i) where @@ -307,6 +314,7 @@ noncomputable def powQuotSuccInclusion (i : ℕ) : map_add' _ _ := rfl map_smul' _ _ := rfl +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem powQuotSuccInclusion_injective (i : ℕ) : Function.Injective (powQuotSuccInclusion p P i) := by rintro ⟨_, _⟩ ⟨_, _⟩ h @@ -316,6 +324,7 @@ theorem powQuotSuccInclusion_injective (i : ℕ) : See `quotientToQuotientRangePowQuotSucc` for this as a linear map, and `quotientRangePowQuotSuccInclusionEquiv` for this as a linear equivalence. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) : S ⧸ P → (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i) := @@ -328,6 +337,7 @@ noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk, Subtype.coe_mk, map_mul, map_sub, mul_sub] +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem quotientToQuotientRangePowQuotSuccAux_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) : quotientToQuotientRangePowQuotSuccAux p P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩ := by @@ -337,6 +347,7 @@ section variable [hfp : NeZero (ramificationIdx' p P)] /-- `S ⧸ P` embeds into the quotient by `P^(i+1) ⧸ P^e` as a subspace of `P^i ⧸ P^e`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def quotientToQuotientRangePowQuotSucc {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) : S ⧸ P →ₗ[R ⧸ p] @@ -356,12 +367,14 @@ noncomputable def quotientToQuotientRangePowQuotSucc Algebra.smul_def, Quotient.algebraMap_quotient_pow_ramificationIdx] ring +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem quotientToQuotientRangePowQuotSucc_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) : quotientToQuotientRangePowQuotSucc p P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩ := quotientToQuotientRangePowQuotSuccAux_mk p P a_mem x set_option backward.isDefEq.respectTransparency.types false in +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem quotientToQuotientRangePowQuotSucc_injective [IsDedekindDomain S] [P.IsPrime] {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) : Function.Injective (quotientToQuotientRangePowQuotSucc p P a_mem) := fun x => @@ -381,6 +394,7 @@ theorem quotientToQuotientRangePowQuotSucc_injective [IsDedekindDomain S] [P.IsP ((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_left a_notMem +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S] (hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) : @@ -406,6 +420,7 @@ theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S] /-- Quotienting `P^i / P^e` by its subspace `P^(i+1) ⧸ P^e` is `R ⧸ p`-linearly isomorphic to `S ⧸ P`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def quotientRangePowQuotSuccInclusionEquiv [IsDedekindDomain S] [P.IsPrime] (hP : P ≠ ⊥) {i : ℕ} (hi : i < e) : ((P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion p P i)) @@ -420,6 +435,7 @@ noncomputable def quotientRangePowQuotSuccInclusionEquiv [IsDedekindDomain S] /-- Since the inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)` has a kernel isomorphic to `P / S`, `[P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]` -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem rank_pow_quot_aux [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) {i : ℕ} (hi : i < e) : Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) = @@ -429,6 +445,7 @@ theorem rank_pow_quot_aux [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : (quotientRangePowQuotSuccInclusionEquiv p P hP0 hi).symm.rank_eq] exact (Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion p P i))).symm +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem rank_pow_quot [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (i : ℕ) (hi : i ≤ e) : Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) = @@ -449,6 +466,7 @@ end /-- If `p` is a maximal ideal of `R`, `S` extends `R` and `P^e` lies over `p`, then the dimension `[S/(P^e) : R/p]` is equal to `e * [S/P : R/p]`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem rank_prime_pow_ramificationIdx [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (he : e ≠ 0) : Module.rank (R ⧸ p) (S ⧸ P ^ e) = @@ -463,6 +481,7 @@ theorem rank_prime_pow_ramificationIdx [IsDedekindDomain S] [p.IsMaximal] [P.IsP /-- If `p` is a maximal ideal of `R`, `S` extends `R` and `P^e` lies over `p`, then the dimension `[S/(P^e) : R/p]`, as a natural number, is equal to `e * [S/P : R/p]`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem finrank_prime_pow_ramificationIdx [IsDedekindDomain S] (hP0 : P ≠ ⊥) [p.IsMaximal] [P.IsPrime] (he : e ≠ 0) : finrank (R ⧸ p) (S ⧸ P ^ e) = @@ -490,32 +509,39 @@ section FactorsMap variable [IsDedekindDomain S] +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Factors.ne_bot (P : (factors (map (algebraMap R S) p)).toFinset) : (P : Ideal S) ≠ ⊥ := (prime_of_factor _ (Multiset.mem_toFinset.mp P.2)).ne_zero +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] instance Factors.isPrime (P : (factors (map (algebraMap R S) p)).toFinset) : IsPrime (P : Ideal S) := Ideal.isPrime_of_prime (prime_of_factor _ (Multiset.mem_toFinset.mp P.2)) +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Factors.ramificationIdx_ne_zero (P : (factors (map (algebraMap R S) p)).toFinset) : ramificationIdx' p P.1 ≠ 0 := IsDedekindDomain.ramificationIdx'_ne_zero (ne_zero_of_mem_factors (Multiset.mem_toFinset.mp P.2)) (Factors.isPrime p P) (Ideal.le_of_dvd (dvd_of_mem_factors (Multiset.mem_toFinset.mp P.2))) +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] instance Factors.fact_ramificationIdx_neZero (P : (factors (map (algebraMap R S) p)).toFinset) : NeZero (ramificationIdx' p P.1) := ⟨Factors.ramificationIdx_ne_zero p P⟩ attribute [local instance] Quotient.algebraQuotientOfRamificationIdxNeZero +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] instance Factors.isScalarTower (P : (factors (map (algebraMap R S) p)).toFinset) : IsScalarTower R (R ⧸ p) (S ⧸ (P : Ideal S)) := IsScalarTower.of_algebraMap_eq' rfl +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] instance Factors.liesOver [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) : P.1.LiesOver p := ⟨(comap_eq_of_scalar_tower_quotient (algebraMap (R ⧸ p) (S ⧸ P.1)).injective).symm⟩ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) : finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) = @@ -523,6 +549,7 @@ theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal] rw [finrank_prime_pow_ramificationIdx, inertiaDeg'_algebraMap] exacts [Factors.ne_bot p P, NeZero.ne _] +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] instance Factors.finiteDimensional_quotient_pow [Module.Finite R S] [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) : FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) := by @@ -534,6 +561,7 @@ universe w /-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R` factors in `S` as `∏ i, P i ^ e i`, then `S ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def Factors.piQuotientEquiv (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) : S ⧸ map (algebraMap R S) p ≃+* ∀ P : (factors (map (algebraMap R S) p)).toFinset, @@ -547,11 +575,11 @@ noncomputable def Factors.piQuotientEquiv (p : Ideal R) (hp : map (algebraMap R rw [IsDedekindDomain.ramificationIdx'_eq_factors_count hp (Factors.isPrime p P) (Factors.ne_bot p P)] -@[simp] +@[simp, deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Factors.piQuotientEquiv_mk (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) (x : S) : Factors.piQuotientEquiv p hp (Ideal.Quotient.mk _ x) = fun _ => Ideal.Quotient.mk _ x := rfl -@[simp] +@[simp, deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem Factors.piQuotientEquiv_map (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) (x : R) : Factors.piQuotientEquiv p hp (algebraMap _ _ x) = fun _ => Ideal.Quotient.mk _ (algebraMap _ _ x) := rfl @@ -561,6 +589,7 @@ variable (S) /-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R` factors in `S` as `∏ i, P i ^ e i`, then `S ⧸ I` factors `R ⧸ I`-linearly as `Π i, R ⧸ (P i ^ e i)`. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] noncomputable def Factors.piQuotientLinearEquiv (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) : (S ⧸ map (algebraMap R S) p) ≃ₗ[R ⧸ p] ∀ P : (factors (map (algebraMap R S) p)).toFinset, @@ -581,6 +610,7 @@ variable (K L : Type*) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [I for `P` ranging over the primes lying over `p`, `∑ P, e P * f P = [Frac(S) : Frac(R)]`; here `S` is a finite `R`-module (and thus `Frac(S) : Frac(R)` is a finite extension) and `p` is maximal. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem sum_ramification_inertia {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ∑ P ∈ IsDedekindDomain.primesOverFinset p S, ramificationIdx' p P * inertiaDeg' p P = finrank K L := by @@ -602,6 +632,7 @@ theorem sum_ramification_inertia {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff] · exact finrank_quotient_map p K L +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem inertiaDeg_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p] (hp0 : p ≠ ⊥) : p.inertiaDeg' P ≤ Module.finrank K L := by @@ -611,6 +642,7 @@ theorem inertiaDeg_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaxima refine le_trans (Nat.le_mul_of_pos_left _ ?_) (Nat.le_add_right _ _) exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver _ hp0 +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem ramificationIdx_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p] : p.ramificationIdx' P ≤ Module.finrank K L := by @@ -622,6 +654,7 @@ theorem ramificationIdx_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsM refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _) exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] theorem card_primesOverFinset_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : Finset.card (IsDedekindDomain.primesOverFinset p S) ≤ Module.finrank K L := by rw [← sum_ramification_inertia S K L hp0, Finset.card_eq_sum_ones] @@ -633,6 +666,7 @@ theorem card_primesOverFinset_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} · exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P /-- `Ideal.sum_ramification_inertia`, in the local (DVR) case. -/ +@[deprecated "Use results of RingTheory.RamificationInertia.Basic" (since := "2026-07-01")] lemma ramificationIdx_mul_inertiaDeg_of_isLocalRing [IsLocalRing S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ramificationIdx' p (IsLocalRing.maximalIdeal S) * From 3edb3c0658f69f197b1e501b1f7623f3f7b3898c Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero <23321199+fbarroero@users.noreply.github.com> Date: Wed, 29 Jul 2026 15:39:30 +0000 Subject: [PATCH 11/20] feat(Algebra/GroupWithZero/WithZero): `toAdd_unzero_eq_log` and simplify proofs (#42149) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the lemma ```lean lemma toAdd_unzero_eq_log {x : Mᵐ⁰} (hx : x ≠ 0) : (unzero hx).toAdd = log x ``` and uses it to simplify some proofs involving `log`, `exp`, and rank-one discrete valuations. Co-authored-by: fbarroero --- Mathlib/Algebra/GroupWithZero/WithZero.lean | 12 ++++----- .../Order/GroupWithZero/Canonical.lean | 20 +++++++-------- .../Valuation/Discrete/RankOne.lean | 25 +++++-------------- 3 files changed, 21 insertions(+), 36 deletions(-) diff --git a/Mathlib/Algebra/GroupWithZero/WithZero.lean b/Mathlib/Algebra/GroupWithZero/WithZero.lean index 5b62e51974c..508b4790bfe 100644 --- a/Mathlib/Algebra/GroupWithZero/WithZero.lean +++ b/Mathlib/Algebra/GroupWithZero/WithZero.lean @@ -10,7 +10,6 @@ public import Mathlib.Algebra.Group.WithOne.Defs public import Mathlib.Algebra.GroupWithZero.Equiv public import Mathlib.Algebra.GroupWithZero.Units.Basic public import Mathlib.Data.Nat.Cast.Defs -public import Mathlib.Data.Option.Basic public import Mathlib.Data.Option.NAry /-! @@ -422,6 +421,10 @@ lemma log_pow : ∀ (x : Mᵐ⁰) (n : ℕ), log (x ^ n) = n • log x | 0, n + 1 => by simp | (x : Multiplicative M), n => rfl +lemma toAdd_unzero_eq_log {x : Mᵐ⁰} (hx : x ≠ 0) : (unzero hx).toAdd = log x := by + lift x to Multiplicative M using hx + simp [log] + end AddMonoid section AddGroup @@ -438,12 +441,7 @@ def logEquiv : (Gᵐ⁰)ˣ ≃ G := unitsWithZeroEquiv.toEquiv.trans Multiplicat @[simp] lemma coe_expEquiv_apply (a : G) : expEquiv a = exp a := rfl -@[simp] lemma logEquiv_apply (x : (Gᵐ⁰)ˣ) : logEquiv x = log x := by - obtain ⟨_ | a, _ | b, hab, hba⟩ := x - · cases hab - · cases hab - · cases hab - · rfl +@[simp] lemma logEquiv_apply (x : (Gᵐ⁰)ˣ) : logEquiv x = log x := toAdd_unzero_eq_log x.ne_zero lemma logEquiv_unitsMk0 (x : Gᵐ⁰) (hx) : logEquiv (.mk0 x hx) = log x := logEquiv_apply _ diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean index 5928ae2e20b..e6ec658728e 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean @@ -527,23 +527,23 @@ variable {G : Type*} [Preorder G] {a b : G} variable [AddGroup G] {x y : Gᵐ⁰} -@[simp] lemma log_le_log (hx : x ≠ 0) (hy : y ≠ 0) : log x ≤ log y ↔ x ≤ y := by - lift x to Multiplicative G using hx; lift y to Multiplicative G using hy; simp [log] - -@[simp] lemma log_lt_log (hx : x ≠ 0) (hy : y ≠ 0) : log x < log y ↔ x < y := by - lift x to Multiplicative G using hx; lift y to Multiplicative G using hy; simp [log] - lemma log_le_iff_le_exp (hx : x ≠ 0) : log x ≤ a ↔ x ≤ exp a := by - lift x to Multiplicative G using hx; simpa [log, exp] using .rfl + rw [← toAdd_unzero_eq_log hx, ← le_ofAdd_iff hx, exp] lemma log_lt_iff_lt_exp (hx : x ≠ 0) : log x < a ↔ x < exp a := by - lift x to Multiplicative G using hx; simpa [log, exp] using .rfl + rw [← toAdd_unzero_eq_log hx, ← lt_ofAdd_iff hx, exp] + +@[simp] lemma log_le_log (hx : x ≠ 0) (hy : y ≠ 0) : log x ≤ log y ↔ x ≤ y := by + rw [log_le_iff_le_exp hx, exp_log hy] + +@[simp] lemma log_lt_log (hx : x ≠ 0) (hy : y ≠ 0) : log x < log y ↔ x < y := by + rw [log_lt_iff_lt_exp hx, exp_log hy] lemma le_log_iff_exp_le (hx : x ≠ 0) : a ≤ log x ↔ exp a ≤ x := by - lift x to Multiplicative G using hx; simpa [log, exp] using .rfl + rw [← log_le_log exp_ne_zero hx, log_exp] lemma lt_log_iff_exp_lt (hx : x ≠ 0) : a < log x ↔ exp a < x := by - lift x to Multiplicative G using hx; simpa [log, exp] using .rfl + rw [← log_lt_log exp_ne_zero hx, log_exp] lemma le_exp_of_log_le (hxa : log x ≤ a) : x ≤ exp a := by obtain rfl | hx := eq_or_ne x 0 <;> simp [← log_le_iff_le_exp, *] diff --git a/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean b/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean index b969772f948..4d2f68028c6 100644 --- a/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean +++ b/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean @@ -53,10 +53,7 @@ lemma valueGroup₀_equiv_withZeroMulInt_apply_zero : lemma valueGroup₀_equiv_withZeroMulInt_apply_zpow (k : ℤ) : valueGroup₀_equiv_withZeroMulInt v (hv.generator' ^ k) = WithZero.exp (- k) := by - simp only [map_zpow₀, valueGroup₀_equiv_withZeroMulInt_apply, WithZero.map'_coe, - MonoidHom.coe_coe] - rw [← WithZero.coe_zpow, WithZero.exp, WithZero.coe_inj, ← map_zpow] - simp [← mulintEquivOfZPowersEqTop_symm_apply_zpow + simp [WithZero.exp, ← mulintEquivOfZPowersEqTop_symm_apply_zpow (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)] lemma valueGroup₀_equiv_withZeroMulInt_strictMono : @@ -88,22 +85,12 @@ lemma valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective (hsurj : F split_ifs with h0 <;> simp only [MonoidWithZeroHom.coe_ofClass] at h0 · simp [h0] - · simp only [WithZero.map'_coe, MonoidHom.coe_coe] - conv_rhs => rw [← coe_unzero h0] - rw [WithZero.coe_inj, ← (MulEquiv.injective (intEquivOfZPowersEqTop _ - (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top))).eq_iff, - MulEquiv.apply_symm_apply] + · rw [WithZero.map'_coe, ← coe_unzero h0, WithZero.coe_inj, + ← (MulEquiv.injective (intEquivOfZPowersEqTop _ + (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top))).eq_iff] ext - simp only [Units.val_mk0, intEquivOfZPowersEqTop_apply, inv_zpow', generator', - SubgroupClass.coe_zpow] - have hg : hv.generator = Units.mk0 (WithZero.exp (-1 : ℤ) : ℤᵐ⁰) (by simp) := - generator_eq_exp_neg_one_of_surjective hsurj - rw [hg] - conv_lhs => rw [MonoidWithZeroHom.coe_ofClass, ← coe_unzero h0] - simp only [coe_unzero, Int.reduceNeg, exp_neg, zpow_neg, Units.val_inv_eq_inv_val, - Units.val_zpow_eq_zpow_val, Units.val_mk0, inv_zpow', ← exp_zsmul, Int.zsmul_eq_mul, mul_one, - inv_inv] - simp [WithZero.exp] + simp [generator', generator_eq_exp_neg_one_of_surjective hsurj, toAdd_unzero_eq_log h0, + exp_log h0] end WithZeroMulInt From 077102ea18686f6e3bfd60206f5b6c12adfd1859 Mon Sep 17 00:00:00 2001 From: Artie Khovanov <17950993+artie2000@users.noreply.github.com> Date: Wed, 29 Jul 2026 18:35:49 +0000 Subject: [PATCH 12/20] feat(LinearAlgebra/Dimension/Free): isomorphic to base ring iff rank is one (#37959) Co-authored-by: artie2000 --- Mathlib/LinearAlgebra/Dimension/Free.lean | 29 +++++++++++++++-------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean index 151eb9748ca..73bcc777f8d 100644 --- a/Mathlib/LinearAlgebra/Dimension/Free.lean +++ b/Mathlib/LinearAlgebra/Dimension/Free.lean @@ -219,15 +219,12 @@ theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq [Module.Finite R M [Module.Finite R M'] : Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M' := ⟨fun ⟨h⟩ => h.finrank_eq, fun h => nonempty_linearEquiv_of_finrank_eq h⟩ -variable (M M') - +variable (M M') in /-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/ noncomputable def LinearEquiv.ofFinrankEq [Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') : M ≃ₗ[R] M' := Classical.choice <| FiniteDimensional.nonempty_linearEquiv_of_finrank_eq cond -variable {M M'} - namespace Module /-- A free module of rank zero is trivial. -/ @@ -286,6 +283,24 @@ lemma finrank_bot_le_finrank_of_isScalarTower_of_free (S T : Type*) [Semiring S] · exact zero_le · rwa [← not_lt, Module.rank_lt_aleph0_iff] +theorem nonempty_linearEquiv_iff_rank_eq_one : + Nonempty (R ≃ₗ[R] M) ↔ Module.rank R M = 1 := by + simp [nonempty_linearEquiv_iff_lift_rank_eq, eq_comm] + +/-- See also `finrank_eq_one_iff` -/ +theorem nonempty_linearEquiv_iff_finrank_eq_one : + Nonempty (R ≃ₗ[R] M) ↔ finrank R M = 1 := by + simp [nonempty_linearEquiv_iff_rank_eq_one, finrank] + +alias ⟨_, nonempty_linearEquiv_of_finrank_eq_one⟩ := nonempty_linearEquiv_iff_finrank_eq_one + +theorem nonempty_algEquiv_iff_finrank_eq_one + {R S : Type*} [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] + [Free R S] : Nonempty (R ≃ₐ[R] S) ↔ finrank R S = 1 := by + rw [← nonempty_linearEquiv_iff_finrank_eq_one] + exact ⟨fun ⟨e⟩ ↦ ⟨e⟩, fun ⟨e⟩ ↦ + ⟨.ofBijective (Algebra.ofId R S) (bijective_algebraMap_of_linearEquiv e)⟩⟩ + variable (R M) /-- A finite rank free module has a basis indexed by `Fin (finrank R M)`. -/ @@ -320,12 +335,6 @@ theorem Basis.nonempty_unique_index_of_finrank_eq_one have : Fintype ι := Fintype.ofFinite ι rwa [Module.finrank_eq_card_basis b, Fintype.card_eq_one_iff_nonempty_unique] at d1 -theorem nonempty_linearEquiv_of_finrank_eq_one (d1 : Module.finrank R M = 1) : - Nonempty (R ≃ₗ[R] M) := by - let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some - have : Unique ι := (b.nonempty_unique_index_of_finrank_eq_one d1).some - exact ⟨((b.equivFun).trans (LinearEquiv.funUnique ι R R)).symm⟩ - @[simp] theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι] {h : finrank R M = 1} {v : M} {i : ι} : From af3493fa1f9bd52f91089dcb38f12301c2948b30 Mon Sep 17 00:00:00 2001 From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com> Date: Wed, 29 Jul 2026 19:03:52 +0000 Subject: [PATCH 13/20] feat(MeasureTheory): prove regular measures have conull support (#41473) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR proves in `MeasureTheory.Measure.Support` that any measure which is compact-inner-regular on open sets has conull support. It also records the consequences for `[μ.InnerRegular]` on spaces with `[OpensMeasurableSpace X]` and for `[μ.Regular]`. It first proves compact subsets of `μ.supportᶜ` have measure zero, then applies `InnerRegularWRT IsCompact IsOpen`. The inner-regular and regular statements are corollaries. Created with the help of codex. Co-authored-by: Yongxi Lin --- Mathlib/MeasureTheory/Measure/Support.lean | 55 +++++++++++++++++++++- 1 file changed, 53 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Support.lean b/Mathlib/MeasureTheory/Measure/Support.lean index 37c3278a70d..168de187f78 100644 --- a/Mathlib/MeasureTheory/Measure/Support.lean +++ b/Mathlib/MeasureTheory/Measure/Support.lean @@ -6,6 +6,7 @@ Authors: Jon Bannon, Jireh Loreaux module public import Mathlib.MeasureTheory.Measure.OpenPos +public import Mathlib.MeasureTheory.Measure.Regular /-! # Support of a Measure @@ -14,7 +15,7 @@ This file develops the theory of the **support** of a measure `μ` on a topological measurable space. The support is defined as the set of points whose every open neighborhood has positive measure. We give equivalent characterizations, prove basic measure-theoretic properties, and study interactions with sums, restrictions, and -absolute continuity. Under various Lindelöf conditions, the support is conull, +absolute continuity. Under various Lindelöf or regularity conditions, the support is conull, and various descriptions of the complement of the support are provided. ## Main definitions @@ -31,6 +32,9 @@ and various descriptions of the complement of the support are provided. * `isClosed_support` : the support is a closed set. * `support_mem_ae_of_isLindelof` and `support_mem_ae` : under Lindelöf (or hereditarily Lindelöf) hypotheses, the support is conull. +* `support_mem_ae_of_innerRegularWRT_isCompact_isOpen` and + `measure_compl_support_of_innerRegularWRT_isCompact_isOpen` : inner regularity by compact + sets on open sets imply that the support is conull. ## Tags @@ -45,7 +49,7 @@ namespace MeasureTheory namespace Measure -open scoped Topology +open scoped Topology ENNReal variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X] @@ -133,6 +137,53 @@ lemma support_eq_sInter : μ.support = ⋂₀ {t : Set X | IsClosed t ∧ μ t convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ) all_goals simp [Set.compl_sUnion, compl_involutive.image_eq_preimage_symm] +section Regular + +/-- Any compact set contained in the complement of the support has zero measure. -/ +lemma measure_eq_zero_of_isCompact_subset_compl_support {K : Set X} (hK : IsCompact K) + (hKsub : K ⊆ μ.supportᶜ) : μ K = 0 := by + refine hK.induction_on measure_empty ?_ ?_ ?_ + · exact fun _ _ hst ht ↦ measure_mono_null hst ht + · exact fun _ _ hs ht ↦ measure_union_null hs ht + · intro x hxK + obtain ⟨U, hUnhds, hU0⟩ := notMem_support_iff_exists.1 (hKsub hxK) + exact ⟨U, mem_nhdsWithin_of_mem_nhds hUnhds, hU0⟩ + +/-- A measure which is compact-inner-regular on open sets has conull support. -/ +lemma support_mem_ae_of_innerRegularWRT_isCompact_isOpen + (hμ : μ.InnerRegularWRT IsCompact IsOpen) : μ.support ∈ ae μ := by + by_contra hne + obtain ⟨K, hKsub, hKcompact, hKpos⟩ := hμ isOpen_compl_support 0 (pos_iff_ne_zero.2 hne) + simp [measure_eq_zero_of_isCompact_subset_compl_support hKcompact hKsub] at hKpos + +/-- A measure which is compact-inner-regular on open sets has conull support. -/ +@[simp] +lemma measure_compl_support_of_innerRegularWRT_isCompact_isOpen + (hμ : μ.InnerRegularWRT IsCompact IsOpen) : μ μ.supportᶜ = 0 := + support_mem_ae_of_innerRegularWRT_isCompact_isOpen hμ + +/-- An inner regular measure has conull support when open sets are measurable. -/ +lemma support_mem_ae_of_innerRegular [OpensMeasurableSpace X] [μ.InnerRegular] : + μ.support ∈ ae μ := + support_mem_ae_of_innerRegularWRT_isCompact_isOpen fun _ hU r hr => + InnerRegular.innerRegular hU.measurableSet r hr + +/-- An inner regular measure has conull support when open sets are measurable. -/ +@[simp] +lemma measure_compl_support_of_innerRegular [OpensMeasurableSpace X] [μ.InnerRegular] : + μ μ.supportᶜ = 0 := support_mem_ae_of_innerRegular + +/-- A regular measure has conull support. -/ +lemma support_mem_ae_of_regular [μ.Regular] : μ.support ∈ ae μ := + support_mem_ae_of_innerRegularWRT_isCompact_isOpen Regular.innerRegular + +/-- A regular measure has conull support. -/ +@[simp] +lemma measure_compl_support_of_regular [μ.Regular] : μ μ.supportᶜ = 0 := + support_mem_ae_of_regular + +end Regular + section Lindelof /-- If the complement of the support is Lindelöf, then the support of a measure is conull. -/ From 30696563acb0596ab44d272bc5dfee96b2e72263 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Wed, 29 Jul 2026 20:08:20 +0000 Subject: [PATCH 14/20] feat: `haveI`/`letI` tactic linter (#41657) This PR implements a variation on the linter that was written by Claude in #41562. It suggest to use `have`/`let` instead of `haveI`/`letI` whenever the goal is a proposition. See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/surprising.20have.2FhaveI.20kernel.20phenomenon/with/609718493 --- Archive/Imo/Imo2008Q3.lean | 2 +- Archive/Imo/Imo2019Q2.lean | 8 +- Archive/Wiedijk100Theorems/BallotProblem.lean | 6 +- Archive/Wiedijk100Theorems/CubingACube.lean | 2 +- .../Wiedijk100Theorems/FriendshipGraphs.lean | 2 +- .../CliffordAlgebraNotInjective.lean | 2 +- Counterexamples/Phillips.lean | 2 +- Counterexamples/SorgenfreyLine.lean | 4 +- .../ZeroDivisorsInAddMonoidAlgebras.lean | 4 +- Mathlib.lean | 1 + Mathlib/Analysis/Convex/Side.lean | 2 +- Mathlib/Geometry/Manifold/Instances/Icc.lean | 2 +- Mathlib/GroupTheory/CommutingProbability.lean | 2 +- Mathlib/Init.lean | 1 + .../MeasureTheory/VectorMeasure/Basic.lean | 2 +- Mathlib/Tactic.lean | 1 + Mathlib/Tactic/Linter/HaveILetI.lean | 78 +++++++++++++++++++ MathlibTest/InstanceDiamonds.lean | 2 +- MathlibTest/Linter/HaveILetI.lean | 28 +++++++ MathlibTest/Tactic/ITauto.lean | 6 +- MathlibTest/TransImports.lean | 4 +- 21 files changed, 135 insertions(+), 26 deletions(-) create mode 100644 Mathlib/Tactic/Linter/HaveILetI.lean create mode 100644 MathlibTest/Linter/HaveILetI.lean diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean index fcb23b005b7..3542bbdbf4b 100644 --- a/Archive/Imo/Imo2008Q3.lean +++ b/Archive/Imo/Imo2008Q3.lean @@ -34,7 +34,7 @@ namespace Imo2008Q3 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) : ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt (2 * n) := by - haveI := Fact.mk hpp + have := Fact.mk hpp have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1] obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3 let m := ZMod.valMinAbs y diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean index e8d16c06c90..c6aedbb2246 100644 --- a/Archive/Imo/Imo2019Q2.lean +++ b/Archive/Imo/Imo2019Q2.lean @@ -275,7 +275,7 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _) hwbtw.mem_affineSpan] exact cfg.PQ_parallel_AB.direction_eq - haveI := someOrientation V + have := someOrientation V have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B] rw [Set.pair_comm, Set.insert_comm] @@ -389,7 +389,7 @@ end Oriented theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by - haveI := someOrientation V + have := someOrientation V rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ← affineIndependent_iff_not_collinear_set] have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by @@ -515,13 +515,13 @@ end Oriented theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by - haveI := someOrientation V + have := someOrientation V rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA, Set.pair_comm, Set.insert_comm, Set.pair_comm] exact cfg.not_collinear_ABC theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by - haveI := someOrientation V + have := someOrientation V rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁, Set.pair_comm] exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean index 3d65be551a9..77c891c0bd2 100644 --- a/Archive/Wiedijk100Theorems/BallotProblem.lean +++ b/Archive/Wiedijk100Theorems/BallotProblem.lean @@ -315,9 +315,9 @@ theorem ballot_problem' : rw [div_self] exact Nat.cast_add_one_ne_zero p · intro q p qp h₁ h₂ - haveI := isProbabilityMeasure_uniformOn + have := isProbabilityMeasure_uniformOn (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _) - haveI := isProbabilityMeasure_uniformOn + have := isProbabilityMeasure_uniformOn (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _) have h₃ : 0 < p + 1 + (q + 1) := Nat.add_pos_left (Nat.succ_pos _) _ rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _), @@ -344,7 +344,7 @@ theorem ballot_problem' : theorem ballot_problem : ∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by intro q p qp - haveI := + have := isProbabilityMeasure_uniformOn (countedSequence_finite p q) (countedSequence_nonempty _ _) have : (uniformOn (countedSequence p q) staysPositive).toReal = diff --git a/Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/Wiedijk100Theorems/CubingACube.lean index b9fa47e86ab..079d3ddb658 100644 --- a/Archive/Wiedijk100Theorems/CubingACube.lean +++ b/Archive/Wiedijk100Theorems/CubingACube.lean @@ -378,7 +378,7 @@ variable (h v) direction will intersect one of the neighbouring cubes on the same boundary as `mi`. -/ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈ _) j := by let i := mi h v; have hi : i ∈ bcubes cs c := mi_mem_bcubes - haveI := h.nontrivial_fin + have := h.nontrivial_fin rcases exists_ne j with ⟨j', hj'⟩ intro hj rcases smallest_onBoundary hj with ⟨x, ⟨hx, h2x⟩, h3x⟩ diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean index 7c4c125c004..506a8f6f9f8 100644 --- a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean +++ b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean @@ -250,7 +250,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa have p_dvd_d_pred := (ZMod.natCast_eq_zero_iff _ _).mpr (d - 1).minFac_dvd have dpos : 1 ≤ d := by lia have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast - haveI : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩ + have : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩ have hp2 : 2 ≤ p := (Fact.out (p := p.Prime)).two_le have dmod : (d : ZMod p) = 1 := by rw [← Nat.succ_pred_eq_of_pos dpos, Nat.succ_eq_add_one, Nat.pred_eq_sub_one] diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean index f6c2d638551..d06713dea37 100644 --- a/Counterexamples/CliffordAlgebraNotInjective.lean +++ b/Counterexamples/CliffordAlgebraNotInjective.lean @@ -155,7 +155,7 @@ theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a theorem sq_map_sub_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) : sq i (a - b) = sq i a - sq i b := by - haveI : Nonempty ι := ⟨i⟩ + have : Nonempty ι := ⟨i⟩ rw [CharTwo.sub_eq_add, CharTwo.sub_eq_add, sq_map_add_char_two] /-- The quadratic form (metric) is just Euclidean -/ diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean index f45f6e352eb..84de25c1c14 100644 --- a/Counterexamples/Phillips.lean +++ b/Counterexamples/Phillips.lean @@ -248,7 +248,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) : -- convenient to formalize the inductive construction. let A : Set (Set α) := {t | t.Countable} let empty : A := ⟨∅, countable_empty⟩ - haveI : Nonempty A := ⟨empty⟩ + have : Nonempty A := ⟨empty⟩ -- given a countable set `s`, one can find a set `t` in its complement with measure close to -- maximal. have : ∀ s : A, ∃ t : A, ∀ u : A, f (↑u \ ↑s) ≤ 2 * f (↑t \ ↑s) := by diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean index 40a7a881d66..2a906717221 100644 --- a/Counterexamples/SorgenfreyLine.lean +++ b/Counterexamples/SorgenfreyLine.lean @@ -68,7 +68,7 @@ theorem isOpen_Ici (a : ℝₗ) : IsOpen (Ici a) := theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := by rw [TopologicalSpace.nhds_generateFrom] - haveI : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype + have : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by refine (IsLeast.isGLB ?_).iInf_eq exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_mem_range.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩ @@ -313,7 +313,7 @@ theorem not_separatedNhds_rat_irrational_antidiag : /-- Topology on the Sorgenfrey line is not metrizable. -/ theorem not_metrizableSpace : ¬MetrizableSpace ℝₗ := by intro - letI := metrizableSpaceMetric ℝₗ + let := metrizableSpaceMetric ℝₗ exact not_normalSpace_prod inferInstance /-- Topology on the Sorgenfrey line is not second countable. -/ diff --git a/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean b/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean index 8243f4b33dd..16fa954c1de 100644 --- a/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean +++ b/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean @@ -244,8 +244,8 @@ example : ¬UniqueProds ℕ := by /-- Some Types that do not have `UniqueSums`. -/ example (n : ℕ) (n2 : 2 ≤ n) : ¬UniqueSums (ZMod n) := by - haveI : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩ - haveI : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne' + have : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩ + have : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne' rintro ⟨h⟩ refine not_not.mpr (h Finset.univ_nonempty Finset.univ_nonempty) ?_ suffices ∀ x y : ZMod n, ∃ x' y' : ZMod n, x' + y' = x + y ∧ (x' = x → ¬y' = y) by diff --git a/Mathlib.lean b/Mathlib.lean index d5e389a4ee4..3afd48340dc 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7421,6 +7421,7 @@ public import Mathlib.Tactic.Linter.FindDeprecations public import Mathlib.Tactic.Linter.FlexibleLinter public import Mathlib.Tactic.Linter.GlobalAttributeIn public import Mathlib.Tactic.Linter.HashCommandLinter +public import Mathlib.Tactic.Linter.HaveILetI public import Mathlib.Tactic.Linter.HaveLetLinter public import Mathlib.Tactic.Linter.Header public import Mathlib.Tactic.Linter.Lint diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean index 91a26699bf8..46445050bec 100644 --- a/Mathlib/Analysis/Convex/Side.lean +++ b/Mathlib/Analysis/Convex/Side.lean @@ -882,7 +882,7 @@ alias isPreconnected_setOf_wOppSide := isPreconnected_setOfPred_wOppSide theorem isConnected_setOfPred_sOppSide {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (s : Set P).Nonempty) : IsConnected { y | s.SOppSide x y } := by obtain ⟨p, hp⟩ := h - haveI : Nonempty s := ⟨⟨p, hp⟩⟩ + have : Nonempty s := ⟨⟨p, hp⟩⟩ rw [setOfPred_sOppSide_eq_image2 hx hp, ← Set.image_prod] refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _ ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean index 41b2d5055e1..c25eb932b6f 100644 --- a/Mathlib/Geometry/Manifold/Instances/Icc.lean +++ b/Mathlib/Geometry/Manifold/Instances/Icc.lean @@ -73,7 +73,7 @@ open Manifold IsManifold lemma isImmersionOfComplement_subtypeVal_Icc : IsImmersionOfComplement Unit (𝓡∂ 1) 𝓘(ℝ) n (fun (z : Icc x y) ↦ (z : ℝ)) := by intro z - letI φ₀ := ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit + let φ₀ := ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit let φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ (fun (_ : Fin 1) ↦ ℝ)) by_cases hz : ↑z < y diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean index 08069325e3a..f9814addf3e 100644 --- a/Mathlib/GroupTheory/CommutingProbability.lean +++ b/Mathlib/GroupTheory/CommutingProbability.lean @@ -81,7 +81,7 @@ variable {M} theorem commProb_eq_one_iff [h : Nonempty M] : commProb M = 1 ↔ IsMulCommutative M := by classical - haveI := Fintype.ofFinite M + have := Fintype.ofFinite M rw [commProb, ← Set.coe_ofPred, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card] rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod, set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall] diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index be658564cb7..f80c0643d8d 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -13,6 +13,7 @@ public import Mathlib.Tactic.Linter.DocString public import Mathlib.Tactic.Linter.EmptyLine public import Mathlib.Tactic.Linter.GlobalAttributeIn public import Mathlib.Tactic.Linter.HashCommandLinter +public import Mathlib.Tactic.Linter.HaveILetI public import Mathlib.Tactic.Linter.Header public import Mathlib.Tactic.Linter.FlexibleLinter public import Mathlib.Tactic.Linter.Multigoal diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean index 223244e95bd..3d94406c186 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean @@ -146,7 +146,7 @@ theorem of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Dis theorem of_biUnion {ι : Type*} {s : Set ι} {f : ι → Set α} (hs : s.Countable) (hd : s.Pairwise (Disjoint on f)) (h : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑' p : s, v (f p) := by - haveI := hs.toEncodable + have := hs.toEncodable rw [biUnion_eq_iUnion] apply of_disjoint_iUnion · exact fun x ↦ h x x.2 diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 2b01d7d338d..506ca9ab5e4 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -191,6 +191,7 @@ public import Mathlib.Tactic.Linter.FindDeprecations public import Mathlib.Tactic.Linter.FlexibleLinter public import Mathlib.Tactic.Linter.GlobalAttributeIn public import Mathlib.Tactic.Linter.HashCommandLinter +public import Mathlib.Tactic.Linter.HaveILetI public import Mathlib.Tactic.Linter.HaveLetLinter public import Mathlib.Tactic.Linter.Header public import Mathlib.Tactic.Linter.Lint diff --git a/Mathlib/Tactic/Linter/HaveILetI.lean b/Mathlib/Tactic/Linter/HaveILetI.lean new file mode 100644 index 00000000000..91f579fa41c --- /dev/null +++ b/Mathlib/Tactic/Linter/HaveILetI.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Jovan Gerbscheid. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jovan Gerbscheid +-/ +module + +public meta import Lean.Meta.Hint +-- Import this linter explicitly to ensure that +-- this file has a valid copyright header and module docstring. +public import Mathlib.Tactic.Linter.Header -- shake: keep + +/-! +# The `haveI`/`letI` linter + +The tactics `haveI` and `letI` differ from `have` and `let` only in that they inline +the given value into the term being constructed, instead of binding it with a +`have`/`let` binder. (In Lean 3, `haveI`/`letI` were additionally needed to make the new +hypothesis available to instance resolution; in Lean 4, `have` and `let` register local +instances themselves, so inlining is the only remaining difference.) + +Inside the proof of a proposition this difference is invisible: proofs are irrelevant, +so nothing can depend on whether a value was inlined into the proof term. Hence +`haveI`/`letI` are never needed in tactic proofs of propositions, and `have`/`let` +should be used instead. + +This linter flags every use of the `haveI` or `letI` tactic whose main goal is a +proposition. + +TODO: +* also lint the term-mode `haveI`/`letI` +-/ + +meta section + +open Lean Elab Meta Parser.Term Tactic Linter + +namespace Mathlib.Linter.HaveILetI + +/-- The `haveILetI` linter flags uses of the `haveI` or `letI` tactic in a proof of a +proposition. Since proofs are irrelevant, the value-inlining behaviour of `haveI`/`letI` +can have no effect there, and `have`/`let` should be used instead. -/ +public register_option linter.style.haveILetI : Bool := { + defValue := true + descr := "enable the `haveILetI` linter" +} + +/-- Run the `haveI` tactic, with a try this suggestion when the goal is a `Prop`. -/ +def runHaveI (tk : Syntax) (c : TSyntax ``letConfig) (d : TSyntax ``letDecl) : TacticM Unit := do + evalTactic (← `(tactic| haveI $c:letConfig $d:letDecl)) + if getLinterValue linter.style.haveILetI (← getLinterOptions) then + withMainContext do + if ← isProp (← getMainTarget) then + let suggs ← Hint.mkSuggestionsMessage #[{toTryThisSuggestion := "have"}] tk none false + logLint linter.style.haveILetI (← getRef) m!"Try this: {suggs}\n\n\ + The goal is a proposition, so `have` is preferred over `haveI`.\n\ + The difference between `have` and `haveI` is that `haveI` inlines the value.\n\ + But this is not relevant for proofs because of proof irrelevance." + +@[tactic_alt Parser.Tactic.tacticHaveI__] +elab (priority := high) tk:"haveI" c:letConfig d:letDecl : tactic => runHaveI tk c d + +/-- Run the `letI` tactic, with a try this suggestion when the goal is a `Prop`. -/ +def runLetI (tk : Syntax) (c : TSyntax ``letConfig) (d : TSyntax ``letDecl) : TacticM Unit := do + evalTactic (← `(tactic| letI $c:letConfig $d:letDecl)) + if getLinterValue linter.style.haveILetI (← getLinterOptions) then + withMainContext do + if ← isProp (← getMainTarget) then + let suggs ← Hint.mkSuggestionsMessage #[{toTryThisSuggestion := "let"}] tk none false + logLint linter.style.haveILetI (← getRef) m!"Try this: {suggs}\n\n\ + The goal is a proposition, so `let` is preferred over `letI`.\n\ + The difference between `let` and `letI` is that `letI` inlines the value.\n\ + But this is not relevant for proofs because of proof irrelevance." + +@[tactic_alt Parser.Tactic.tacticLetI__] +elab (priority := high) tk:"letI" c:letConfig d:letDecl : tactic => runLetI tk c d + +end Mathlib.Linter.HaveILetI diff --git a/MathlibTest/InstanceDiamonds.lean b/MathlibTest/InstanceDiamonds.lean index 1e75f7ca3ce..327a41be8d4 100644 --- a/MathlibTest/InstanceDiamonds.lean +++ b/MathlibTest/InstanceDiamonds.lean @@ -154,7 +154,7 @@ the domain is a group. -/ example {k : Type _} [Semiring k] [Nontrivial kˣ] : (Finsupp.comapSMul : SMul kˣ (kˣ →₀ k)) ≠ Finsupp.smulZeroClass.toSMul := by obtain ⟨u : kˣ, hu⟩ := exists_ne (1 : kˣ) - haveI : Nontrivial k := Units.val_injective.nontrivial + have : Nontrivial k := Units.val_injective.nontrivial intro h simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, DFunLike.ext_iff] at h replace h := h u (Finsupp.single 1 1) u diff --git a/MathlibTest/Linter/HaveILetI.lean b/MathlibTest/Linter/HaveILetI.lean new file mode 100644 index 00000000000..793d3d2f5cc --- /dev/null +++ b/MathlibTest/Linter/HaveILetI.lean @@ -0,0 +1,28 @@ +module + +public import Mathlib.Tactic.Linter.HaveILetI + +/-- +warning: Try this: ⏎ + haveI̵ + +The goal is a proposition, so `have` is preferred over `haveI`. +The difference between `have` and `haveI` is that `haveI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +--- +warning: Try this: ⏎ + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +-/ +#guard_msgs in +example : True := by + haveI : True := trivial + letI : True := trivial + trivial diff --git a/MathlibTest/Tactic/ITauto.lean b/MathlibTest/Tactic/ITauto.lean index 177ded212ae..d18466aad26 100644 --- a/MathlibTest/Tactic/ITauto.lean +++ b/MathlibTest/Tactic/ITauto.lean @@ -60,9 +60,9 @@ set_option linter.unusedVariables false in set_option linter.unusedTactic false in -- failure tests example (p q r : Prop) : True := by - haveI : p ∨ ¬p := by (fail_if_success itauto); sorry - clear this; haveI : ¬(p ↔ q) → ¬p → q := by (fail_if_success itauto); sorry - clear this; haveI : ¬(p ↔ q) → (r ↔ q) → (p ↔ ¬r) := by (fail_if_success itauto); sorry + have : p ∨ ¬p := by (fail_if_success itauto); grind + clear this; have : ¬(p ↔ q) → ¬p → q := by (fail_if_success itauto); grind + clear this; have : ¬(p ↔ q) → (r ↔ q) → (p ↔ ¬r) := by (fail_if_success itauto); grind trivial example (P : Nat → Prop) (n : Nat) diff --git a/MathlibTest/TransImports.lean b/MathlibTest/TransImports.lean index 3f91b2bfb62..3bcad6d0bbf 100644 --- a/MathlibTest/TransImports.lean +++ b/MathlibTest/TransImports.lean @@ -3,8 +3,8 @@ import Mathlib.Util.TransImports /-- info: 'MathlibTest.TransImports' has at most 2000 transitive imports -2 starting with "Mathlib.Tactic.Linter.H": -[Mathlib.Tactic.Linter.HashCommandLinter, Mathlib.Tactic.Linter.Header] +3 starting with "Mathlib.Tactic.Linter.H": +[Mathlib.Tactic.Linter.HashCommandLinter, Mathlib.Tactic.Linter.HaveILetI, Mathlib.Tactic.Linter.Header] -/ #guard_msgs in #trans_imports "Mathlib.Tactic.Linter.H" at_most 2000 From 8f845ad22e5caace30bf431f91c084bb309bec77 Mon Sep 17 00:00:00 2001 From: "mathlib-update-dependencies[bot]" <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Date: Wed, 29 Jul 2026 21:14:39 +0000 Subject: [PATCH 15/20] chore: update Mathlib dependencies 2026-07-29 (#42259) 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 f7e0737aa17..43aaa30cab5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d60e6444e6fd881dfa077ff36e96de75753afa28", + "rev": "41bd267b3f6b7252f6676af46d4ffc6783b64de9", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 80a3b5d91985b3c50e59239bbe5fa08613b5ec31 Mon Sep 17 00:00:00 2001 From: Noah Walker <30136151+NoahW314@users.noreply.github.com> Date: Wed, 29 Jul 2026 22:06:16 +0000 Subject: [PATCH 16/20] chore: address comments from #42114 (#42257) Addresses comments from #42114. In particular, we add docstrings for `isOpen_Ioo'` (and `isOpen_Iio'`, `isOpen_Ioi'`) and use dot notation. Co-authored-by: NoahW314 --- Mathlib/Topology/Order/Basic.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 1c668250cd8..66db37930cd 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -114,12 +114,14 @@ theorem isOpen_iff_generate_intervals [t : OrderTopology α] {s : Set α} : theorem isOpen_lt' [OrderTopology α] (a : α) : IsOpen { b : α | a < b } := isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inl rfl⟩ -@[to_dual] +/-- A version of `isOpen_Ioi` that doesn't require a `LinearOrder`. -/ +@[to_dual /-- A version of `isOpen_Iio` that doesn't require a `LinearOrder`. -/] theorem isOpen_Ioi' [OrderTopology α] (a : α) : IsOpen (Ioi a) := isOpen_lt' a +/-- A version of `isOpen_Ioo` that doesn't require a `LinearOrder`. -/ @[to_dual self] theorem isOpen_Ioo' [OrderTopology α] (a b : α) : IsOpen (Ioo a b) := - IsOpen.inter (isOpen_Ioi' a) (isOpen_Iio' b) + (isOpen_Ioi' a).inter (isOpen_Iio' b) @[to_dual gt_mem_nhds] theorem lt_mem_nhds [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x := From ad7bd8f3609cf7c05fa69c804ec1a0e7de25dbaf Mon Sep 17 00:00:00 2001 From: Thomas Browning <13339017+tb65536@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:30:22 +0000 Subject: [PATCH 17/20] chore(Analysis/Convex/Continuous): fix proof wanted (#42234) Kevin's Claude noticed that the first two commented out `proof_wanted`s should say `LocallyLipschitzOn` (currently they are identical to the last two commented out `proof_wanted`s which say `ContinuousOn`). Co-authored-by: tb65536 --- Mathlib/Analysis/Convex/Continuous.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean index 5c6ace7d827..da39705b256 100644 --- a/Mathlib/Analysis/Convex/Continuous.lean +++ b/Mathlib/Analysis/Convex/Continuous.lean @@ -223,10 +223,10 @@ protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : Locally -- Commented out since `intrinsicInterior` is not imported (but should be once these are proved) -- proof_wanted ConvexOn.locallyLipschitzOn_intrinsicInterior (hf : ConvexOn ℝ C f) : --- ContinuousOn f (intrinsicInterior ℝ C) +-- LocallyLipschitzOn (intrinsicInterior ℝ C) f -- proof_wanted ConcaveOn.locallyLipschitzOn_intrinsicInterior (hf : ConcaveOn ℝ C f) : --- ContinuousOn f (intrinsicInterior ℝ C) +-- LocallyLipschitzOn (intrinsicInterior ℝ C) f -- proof_wanted ConvexOn.continuousOn_intrinsicInterior (hf : ConvexOn ℝ C f) : -- ContinuousOn f (intrinsicInterior ℝ C) From 481daa6fe9ab148e2cc3f9a667298edbbcba3ee0 Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Thu, 30 Jul 2026 00:05:45 +0000 Subject: [PATCH 18/20] feat(RingTheory/Algebraic): tower law for Module.finrank over domains (#41614) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `Module.finrank_mul_finrank'`, a variant of the tower law `finrank R S * finrank S T = finrank R T` for a tower of domains `R → S → T`. --- Mathlib/LinearAlgebra/Dimension/Free.lean | 5 ++++- Mathlib/RingTheory/Algebraic/Integral.lean | 24 +++++++++++++++++++--- 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean index 73bcc777f8d..691e13d49d4 100644 --- a/Mathlib/LinearAlgebra/Dimension/Free.lean +++ b/Mathlib/LinearAlgebra/Dimension/Free.lean @@ -61,7 +61,10 @@ theorem rank_mul_rank (A : Type v) [AddCommMonoid A] convert! lift_rank_mul_lift_rank F K A <;> rw [lift_id] /-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then -$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/ +$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. + +See `Module.finrank_mul_finrank'` for a variant over a tower of domains that assumes the rings are +module-finite rather than the modules being free. -/ theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := by simp_rw [finrank] rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul, diff --git a/Mathlib/RingTheory/Algebraic/Integral.lean b/Mathlib/RingTheory/Algebraic/Integral.lean index 1dd7574f73f..9ef1db23b5d 100644 --- a/Mathlib/RingTheory/Algebraic/Integral.lean +++ b/Mathlib/RingTheory/Algebraic/Integral.lean @@ -5,12 +5,11 @@ Authors: Johan Commelin -/ module +public import Mathlib.Algebra.Ring.Hom.InjSurj public import Mathlib.LinearAlgebra.Dimension.Localization public import Mathlib.RingTheory.Algebraic.Basic public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic -public import Mathlib.RingTheory.Localization.BaseChange - -import Mathlib.RingTheory.Polynomial.Subring +public import Mathlib.RingTheory.Polynomial.Subring /-! # Algebraic elements and integral elements @@ -563,6 +562,25 @@ theorem rank_fractionRing [IsDomain S] : end Algebra.IsAlgebraic +attribute [local instance] FractionRing.liftAlgebra in +/-- Tower law for `Module.finrank` in a tower of domains `R → S → T`. This is a variant of +`Module.finrank_mul_finrank` that assumes the rings are domains instead of the modules being +free. -/ +theorem Module.finrank_mul_finrank' (T : Type*) [CommRing T] [IsDomain T] + [Algebra S T] [Algebra R T] [IsScalarTower R S T] [FaithfulSMul S T] : + Module.finrank R S * Module.finrank S T = Module.finrank R T := by + by_cases h : FaithfulSMul R S + · have : FaithfulSMul R T := .trans R S T + have : IsDomain R := (FaithfulSMul.algebraMap_injective R T).isDomain + have : IsDomain S := (FaithfulSMul.algebraMap_injective S T).isDomain + rw [← IsFractionRing.finrank_eq R (FractionRing R) S (FractionRing S), + ← IsFractionRing.finrank_eq S (FractionRing S) T (FractionRing T), + ← IsFractionRing.finrank_eq R (FractionRing R) T (FractionRing T), + Module.finrank_mul_finrank (FractionRing R) (FractionRing S) (FractionRing T)] + · rw [Module.finrank_eq_zero_of_not_faithfulSMul h, zero_mul, + Module.finrank_eq_zero_of_not_faithfulSMul] + exact fun _ ↦ h (FaithfulSMul.tower_bot R S T) + section Polynomial attribute [local instance] Polynomial.algebra MvPolynomial.algebraMvPolynomial From ccedd504126da4c77960a5c726b90ef554156fdd Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Thu, 30 Jul 2026 03:14:59 +0000 Subject: [PATCH 19/20] chore(CategoryTheory/Monoidal/Cartesian/Over): remove most backward options (#42267) This PR uses `implicit_reducible` to remove some backward options that currently block the use of `scripts/rm_set_option.py`. --- .../Limits/Constructions/Over/Products.lean | 7 +-- Mathlib/CategoryTheory/Limits/HasLimits.lean | 2 + .../Monoidal/Cartesian/Over.lean | 52 ------------------- 3 files changed, 3 insertions(+), 58 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean index 41d85225189..215af251749 100644 --- a/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean @@ -56,10 +56,9 @@ namespace CategoryTheory.Limits section Over variable {f : Y ⟶ X} {g : Z ⟶ X} -set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- Pullback cones to `X` are the same thing as binary fans in `Over X`. -/ -@[simps] +@[implicit_reducible, simps] def pullbackConeEquivBinaryFan : PullbackCone f g ≌ BinaryFan (Over.mk f) (.mk g) where functor.obj c := .mk (Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk f) c.fst rfl) (Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk g) c.snd c.condition.symm) @@ -94,9 +93,6 @@ def IsLimit.pullbackConeEquivBinaryFanFunctor {c : PullbackCone f g} (hc : IsLim · simpa using! congr(($e₁).left) · simpa using! congr(($e₂).left) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency.types false in /-- A pullback cone to `X` is a limit if its corresponding binary fan in `Over X` is a limit. -/ -- This could also be `(IsLimit.ofConeEquiv pullbackConeEquivBinaryFan.symm).symm hc`, but possibly -- bad defeqs? @@ -186,7 +182,6 @@ variable {X : C} {Y Z : Over X} open Limits set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in lemma isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) : IsPullback c.fst.left c.snd.left Y.hom Z.hom := ⟨by simp, ⟨hc.pullbackConeEquivBinaryFanInverse⟩⟩ diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean index daf22dcd488..b92a031ebd3 100644 --- a/Mathlib/CategoryTheory/Limits/HasLimits.lean +++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean @@ -142,6 +142,7 @@ def limit (F : J ⥤ C) [HasLimit F] := (limit.cone F).pt /-- The projection from the limit object to a value of the functor. -/ +@[implicit_reducible] def limit.π (F : J ⥤ C) [HasLimit F] (j : J) : limit F ⟶ F.obj j := (limit.cone F).π.app j @@ -704,6 +705,7 @@ def colimit (F : J ⥤ C) [HasColimit F] := (colimit.cocone F).pt /-- The coprojection from a value of the functor to the colimit object. -/ +@[implicit_reducible] def colimit.ι (F : J ⥤ C) [HasColimit F] (j : J) : F.obj j ⟶ colimit F := (colimit.cocone F).ι.app j diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean index 1d995fe3a43..04966938bfe 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean @@ -29,8 +29,6 @@ open CategoryTheory.Functor Limits CartesianMonoidalCategory variable {C : Type*} [Category* C] [HasPullbacks C] -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- A choice of finite products of `Over X` given by `Limits.pullback`. -/ abbrev cartesianMonoidalCategory (X : C) : CartesianMonoidalCategory (Over X) := .ofChosenFiniteProducts @@ -41,7 +39,6 @@ abbrev cartesianMonoidalCategory (X : C) : CartesianMonoidalCategory (Over X) := attribute [local instance] cartesianMonoidalCategory -set_option backward.isDefEq.respectTransparency.types false in /-- `Over X` is braided w.r.t. the Cartesian monoidal structure given by `Limits.pullback`. -/ abbrev braidedCategory (X : C) : BraidedCategory (Over X) := .ofCartesianMonoidalCategory @@ -52,200 +49,162 @@ open MonoidalCategory variable {X : C} -set_option backward.isDefEq.respectTransparency.types false in @[ext] lemma tensorObj_ext {R : C} {S T : Over X} (f₁ f₂ : R ⟶ (S ⊗ T).left) (e₁ : f₁ ≫ pullback.fst _ _ = f₂ ≫ pullback.fst _ _) (e₂ : f₁ ≫ pullback.snd _ _ = f₂ ≫ pullback.snd _ _) : f₁ = f₂ := pullback.hom_ext e₁ e₂ -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma tensorObj_left (R S : Over X) : (R ⊗ S).left = Limits.pullback R.hom S.hom := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma tensorObj_hom (R S : Over X) : (R ⊗ S).hom = pullback.fst R.hom S.hom ≫ R.hom := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma tensorUnit_left : (𝟙_ (Over X)).left = X := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma tensorUnit_hom : (𝟙_ (Over X)).hom = 𝟙 X := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma lift_left {R S T : Over X} (f : R ⟶ S) (g : R ⟶ T) : (lift f g).left = pullback.lift f.left g.left (f.w.trans g.w.symm) := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma fst_left {R S : Over X} : (fst R S).left = pullback.fst _ _ := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma snd_left {R S : Over X} : (snd R S).left = pullback.snd _ _ := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma toUnit_left {R : Over X} : (toUnit R).left = R.hom := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_hom_left_fst (R S T : Over X) : (α_ R S T).hom.left ≫ pullback.fst _ (pullback.fst _ _ ≫ _) = pullback.fst _ _ ≫ pullback.fst _ _ := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_hom_left_snd_fst (R S T : Over X) : (α_ R S T).hom.left ≫ pullback.snd _ (pullback.fst _ _ ≫ _) ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.snd _ _ := (limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _) -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_hom_left_snd_snd (R S T : Over X) : (α_ R S T).hom.left ≫ pullback.snd _ (pullback.fst _ _ ≫ _) ≫ pullback.snd _ _ = pullback.snd _ _ := (limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _) -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_inv_left_fst_fst (R S T : Over X) : (α_ R S T).inv.left ≫ pullback.fst (pullback.fst _ _ ≫ _) _ ≫ pullback.fst _ _ = pullback.fst _ _ := (limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _) -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_inv_left_fst_snd (R S T : Over X) : (α_ R S T).inv.left ≫ pullback.fst (pullback.fst _ _ ≫ _) _ ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.fst _ _ := (limit.lift_π_assoc _ _ _).trans (limit.lift_π _ _) -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma associator_inv_left_snd (R S T : Over X) : (α_ R S T).inv.left ≫ pullback.snd (pullback.fst _ _ ≫ _) _ = pullback.snd _ _ ≫ pullback.snd _ _ := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma leftUnitor_hom_left (Y : Over X) : (λ_ Y).hom.left = pullback.snd _ _ := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma leftUnitor_inv_left_fst (Y : Over X) : (λ_ Y).inv.left ≫ pullback.fst (𝟙 X) _ = Y.hom := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma leftUnitor_inv_left_snd (Y : Over X) : (λ_ Y).inv.left ≫ pullback.snd (𝟙 X) _ = 𝟙 Y.left := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma rightUnitor_hom_left (Y : Over X) : (ρ_ Y).hom.left = pullback.fst _ (𝟙 X) := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma rightUnitor_inv_left_fst (Y : Over X) : (ρ_ Y).inv.left ≫ pullback.fst _ (𝟙 X) = 𝟙 _ := limit.lift_π _ _ -#adaptation_note -/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma rightUnitor_inv_left_snd (Y : Over X) : (ρ_ Y).inv.left ≫ pullback.snd _ (𝟙 X) = Y.hom := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in lemma whiskerLeft_left {R S T : Over X} (f : S ⟶ T) : (R ◁ f).left = pullback.map _ _ _ _ (𝟙 _) f.left (𝟙 _) (by simp) (by simp) := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma whiskerLeft_left_fst {R S T : Over X} (f : S ⟶ T) : (R ◁ f).left ≫ pullback.fst _ _ = pullback.fst _ _ := (limit.lift_π _ _).trans (Category.comp_id _) -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma whiskerLeft_left_snd {R S T : Over X} (f : S ⟶ T) : (R ◁ f).left ≫ pullback.snd _ _ = pullback.snd _ _ ≫ f.left := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in lemma whiskerRight_left {R S T : Over X} (f : S ⟶ T) : (f ▷ R).left = pullback.map _ _ _ _ f.left (𝟙 _) (𝟙 _) (by simp) (by simp) := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma whiskerRight_left_fst {R S T : Over X} (f : S ⟶ T) : (f ▷ R).left ≫ pullback.fst _ _ = pullback.fst _ _ ≫ f.left := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma whiskerRight_left_snd {R S T : Over X} (f : S ⟶ T) : (f ▷ R).left ≫ pullback.snd _ _ = pullback.snd _ _ := (limit.lift_π _ _).trans (Category.comp_id _) -set_option backward.isDefEq.respectTransparency.types false in lemma tensorHom_left {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) : (f ⊗ₘ g).left = pullback.map _ _ _ _ f.left g.left (𝟙 _) (by simp) (by simp) := rfl -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma tensorHom_left_fst {S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) : (f ⊗ₘ g).left ≫ pullback.fst fS fU = pullback.fst R.hom T.hom ≫ f.left := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[reassoc (attr := simp)] lemma tensorHom_left_snd {S U : C} {R T : Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ mk fS) (g : T ⟶ mk fU) : (f ⊗ₘ g).left ≫ pullback.snd fS fU = pullback.snd R.hom T.hom ≫ g.left := limit.lift_π _ _ -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma braiding_hom_left {R S : Over X} : (β_ R S).hom.left = (pullbackSymmetry _ _).hom := rfl -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma braiding_inv_left {R S : Over X} : (β_ R S).inv.left = (pullbackSymmetry _ _).hom := rfl variable {A B R S Y Z : C} {f : R ⟶ X} {g : S ⟶ X} -set_option backward.isDefEq.respectTransparency.types false in instance : (Over.pullback f).Braided := .ofChosenFiniteProducts _ -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma η_pullback_left : (OplaxMonoidal.η (Over.pullback f)).left = (pullback.snd (𝟙 _) f) := rfl -set_option backward.isDefEq.respectTransparency false in @[simp] lemma ε_pullback_left : (LaxMonoidal.ε (Over.pullback f)).left = inv (pullback.snd (𝟙 _) f) := by apply IsIso.eq_inv_of_hom_inv_id rw [← η_pullback_left, ← Over.comp_left, Monoidal.η_ε, Over.id_left] -set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma μ_pullback_left_fst_fst (R S : Over X) : (LaxMonoidal.μ (Over.pullback f) R S).left ≫ @@ -255,7 +214,6 @@ lemma μ_pullback_left_fst_fst (R S : Over X) : Iso.hom_inv_id] simp [CartesianMonoidalCategory.prodComparison, fst] -set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma μ_pullback_left_fst_snd (R S : Over X) : (LaxMonoidal.μ (Over.pullback f) R S).left ≫ @@ -274,7 +232,6 @@ lemma μ_pullback_left_snd (R S : Over X) : ← Over.comp_left_assoc, Iso.hom_inv_id] simp [CartesianMonoidalCategory.prodComparison] -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma μ_pullback_left_fst_fst' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫ @@ -282,7 +239,6 @@ lemma μ_pullback_left_fst_fst' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : pullback.fst _ _ ≫ pullback.fst _ _ := μ_pullback_left_fst_fst .. -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma μ_pullback_left_fst_snd' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫ @@ -290,21 +246,18 @@ lemma μ_pullback_left_fst_snd' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : pullback.snd _ _ ≫ pullback.fst _ _ := μ_pullback_left_fst_snd .. -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma μ_pullback_left_snd' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫ pullback.snd (pullback.fst g₁ g₂ ≫ g₁) f = pullback.snd _ _ ≫ pullback.snd _ _ := μ_pullback_left_snd .. -set_option backward.isDefEq.respectTransparency false in @[simp] lemma preservesTerminalIso_pullback (f : R ⟶ S) : preservesTerminalIso (Over.pullback f) = Over.isoMk (asIso (pullback.snd (𝟙 _) f)) (by simp) := by ext1; exact toUnit_unique _ _ -set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in @[simp] lemma prodComparisonIso_pullback_inv_left_fst_fst (f : X ⟶ Y) (A B : Over Y) : @@ -315,7 +268,6 @@ lemma prodComparisonIso_pullback_inv_left_fst_fst (f : X ⟶ Y) (A B : Over Y) : Over.hom_left_inv_left_assoc] simp [CartesianMonoidalCategory.prodComparison, fst] -set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma prodComparisonIso_pullback_Spec_inv_left_fst_fst' (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : (prodComparisonIso (Over.pullback f) (.mk gA) (.mk gB)).inv.left ≫ @@ -323,7 +275,6 @@ lemma prodComparisonIso_pullback_Spec_inv_left_fst_fst' (f : X ⟶ Y) (gA : A pullback.fst (pullback.snd gA f) (pullback.snd gB f) ≫ pullback.fst _ _ := prodComparisonIso_pullback_inv_left_fst_fst .. -set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in @[simp] lemma prodComparisonIso_pullback_inv_left_fst_snd' (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : @@ -343,7 +294,6 @@ lemma prodComparisonIso_pullback_inv_left_snd' (f : X ⟶ Y) (gA : A ⟶ Y) (gB Over.hom_left_inv_left_assoc] simp [CartesianMonoidalCategory.prodComparison] -set_option backward.isDefEq.respectTransparency.types false in /-- The pullback of a monoid object is a monoid object. -/ @[simps! -isSimp mul one] abbrev monObjMkPullbackSnd [MonObj (Over.mk f)] : MonObj (Over.mk <| pullback.snd f g) := @@ -351,12 +301,10 @@ abbrev monObjMkPullbackSnd [MonObj (Over.mk f)] : MonObj (Over.mk <| pullback.sn attribute [local instance] monObjMkPullbackSnd -set_option backward.isDefEq.respectTransparency.types false in instance isCommMonObj_mk_pullbackSnd [MonObj (Over.mk f)] [IsCommMonObj (Over.mk f)] : IsCommMonObj (Over.mk <| pullback.snd f g) := ((Over.pullback g).mapCommMon.obj <| .mk <| .mk f).comm -set_option backward.isDefEq.respectTransparency.types false in /-- The pullback of a monoid object is a monoid object. -/ @[simps! -isSimp mul one] abbrev grpObjMkPullbackSnd [GrpObj (Over.mk f)] : GrpObj (Over.mk (pullback.snd f g)) := From 60af7185ecf32ed5cab100f9960f1d588b9a6cab Mon Sep 17 00:00:00 2001 From: Chris Henson <46805207+chenson2018@users.noreply.github.com> Date: Thu, 30 Jul 2026 04:22:55 +0000 Subject: [PATCH 20/20] fix: increase priority of show elaboration (#42264) See [this thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Performance.20cost.20of.20info.20tree.20traversal/with/610705175) for discussion. This prevents a confusing lack of messages for the `show` tactic introduced in #41761. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> --- Mathlib/Tactic/Linter/Style.lean | 4 +++- MathlibTest/Linter/Show.lean | 21 +++++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 MathlibTest/Linter/Show.lean diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index 8e1d4af6bcd..ccfca84e020 100644 --- a/Mathlib/Tactic/Linter/Style.lean +++ b/Mathlib/Tactic/Linter/Style.lean @@ -647,8 +647,10 @@ def elabShow (newType : Term) : TacticM Unit := do readability.\nHowever, this tactic invocation changed the goal. Please use `change` \ instead for these purposes." +-- `(priority := high)` ensures we avoid producing choice nodes, and thereby avoid unexpected +-- behavior arising from choice node elaboration @[tactic_alt Tactic.show] -elab (name := «show») "show " newType:term : tactic => elabShow newType +elab (name := «show») (priority := high) "show " newType:term : tactic => elabShow newType end Style diff --git a/MathlibTest/Linter/Show.lean b/MathlibTest/Linter/Show.lean new file mode 100644 index 00000000000..ae04e466c83 --- /dev/null +++ b/MathlibTest/Linter/Show.lean @@ -0,0 +1,21 @@ +module +import Mathlib.Tactic.Linter.Style + +set_option linter.style.show true + +/- +Check that logged messages appear when errors with synthetic `sorry` are thrown. + +If a choice node is produced, `evalChoice` (currently) resets the state, erasing logs, and +re-throwing the produced error. And if the error contains a synthetic sorry, Lean will not log it, +trusting that the (now-erased) logged errors that preceded it are sufficient. As such, a choice +node may ultimately produce a state with no visible errors at the tactic, since the logged ones +have been erased and the thrown ones are not rendered in expectation of the logged ones appearing. + +This test fails correctly now because the parser avoids producing a choice node in the first place, +via `(priority := high)`. +-/ + +/-- error: Unknown identifier `arbitrary_ident` -/ +#guard_msgs in +example : False := by show arbitrary_ident