diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean index fcb23b005b..3542bbdbf4 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 e8d16c06c9..c6aedbb224 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 3d65be551a..77c891c0bd 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 b9fa47e86a..079d3ddb65 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 7c4c125c00..506a8f6f9f 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.lean b/Counterexamples.lean index 7a514ba1e0..80c2aea1ae 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 a7f42ed111..25abfb4d36 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 16029d0bd9..fc6001a207 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 fcb0eb5e25..4532e2e779 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 f47f319b0e..d06713dea3 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 @@ -154,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/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean index 8d32ce2328..abf3c54a2e 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 e3b0ec0ba2..7777b22e58 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 b2f95cb70a..638eaae576 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 bd6548b6cf..1458342e80 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 69b1fba2b1..1e8e2baef7 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 16ea6890ec..961031ec7d 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 0d199e6a6a..a909e32afb 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 f6ad1b8b76..7b997682cd 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 bf54f34f6c..8fb5981cf3 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 f61b83cdfc..1598c78874 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 9edd2ddce5..ccd46ac7f4 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 7efe730dd0..d32455f99d 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 77498fd660..f7b96bf226 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 2e1abcba12..ec3671ccf3 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 b534672524..c1d6097a05 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 cf18431253..87c36c62a5 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 53f57c8e18..84de25c1c1 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 := α @@ -247,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 @@ -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 5f0ecfbb6b..4e24bff1a2 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 2bc8b8fc8a..0924871e0c 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 b6466778a9..16210d6f98 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 536a6c30ea..5ea73a444e 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 bdc8853b91..a3a19c7f0f 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 6618e73e90..2a90671722 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`. -/ @@ -67,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⟩ @@ -312,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. -/ @@ -321,6 +322,4 @@ theorem not_secondCountableTopology : ¬SecondCountableTopology ℝₗ := end SorgenfreyLine -end - end Counterexample diff --git a/Counterexamples/TopologistsSineCurve.lean b/Counterexamples/TopologistsSineCurve.lean index 15f0293b58..218afac81a 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 5b0f8d98d0..16fa954c1d 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 @@ -242,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 d5e389a4ee..3afd48340d 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/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 3111721ff6..72942dc542 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/GroupWithZero/WithZero.lean b/Mathlib/Algebra/GroupWithZero/WithZero.lean index 5b62e51974..508b4790bf 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 5928ae2e20..e6ec658728 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/Algebra/SkewMonoidAlgebra/Basic.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean index 1defc05fd5..ce9b801073 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 eef257f5ab..fef916f767 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] @@ -745,7 +739,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/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean index 5c6ace7d82..da39705b25 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) diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean index 91a26699bf..46445050be 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/CategoryTheory/ConcreteCategory/ReflectsIso.lean b/Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean index f847a89d7e..92375dd901 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/CategoryTheory/Limits/Constructions/Over/Products.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean index 41d8522518..215af25174 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 daf22dcd48..b92a031ebd 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 1d995fe3a4..04966938bf 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)) := diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean index f982dd2b27..9bea39c519 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] diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean index 847080985a..3c837b046b 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/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean index 41b2d5055e..c25eb932b6 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 08069325e3..f9814addf3 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/GroupTheory/Coset/Defs.lean b/Mathlib/GroupTheory/Coset/Defs.lean index 2af03b2d5f..e50fde599d 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 diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean index 5306d9a770..2e510e6fa9 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/Init.lean b/Mathlib/Init.lean index be658564cb..f80c0643d8 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/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean index 151eb9748c..691e13d49d 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, @@ -219,15 +222,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 +286,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 +338,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 : ι} : diff --git a/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean b/Mathlib/LinearAlgebra/Matrix/Nonsingular.lean index 68ef3c3b93..4bd0342823 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 diff --git a/Mathlib/MeasureTheory/Measure/Support.lean b/Mathlib/MeasureTheory/Measure/Support.lean index 37c3278a70..168de187f7 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. -/ diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean index 223244e95b..3d94406c18 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/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean index 3b52650f79..970a536cb9 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/NumberField/AdeleRing.lean b/Mathlib/NumberTheory/NumberField/AdeleRing.lean index fc0c726777..c88b458310 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 a1cd977f3b..e2e126fb60 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/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean index 39a7c21aa4..508511d234 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) * diff --git a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean index 3c893ab7a5..2e66a2bfa5 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/RingTheory/Algebraic/Integral.lean b/Mathlib/RingTheory/Algebraic/Integral.lean index 1dd7574f73..9ef1db23b5 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 diff --git a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean index 0cda4b73f6..7d3a06d38f 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 diff --git a/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean b/Mathlib/RingTheory/Valuation/Discrete/RankOne.lean index b969772f94..4d2f68028c 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 diff --git a/Mathlib/SetTheory/Cardinal/NatCard.lean b/Mathlib/SetTheory/Cardinal/NatCard.lean index ee56380d8b..c238a719a3 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 diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 2b01d7d338..506ca9ab5e 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 0000000000..91f579fa41 --- /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/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index 8e1d4af6bc..ccfca84e02 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/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 1c668250cd..66db37930c 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 := diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean index 811b88bf42..b5087dd23e 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 ‹_› diff --git a/Mathlib/Topology/UniformSpace/Ascoli.lean b/Mathlib/Topology/UniformSpace/Ascoli.lean index 716a7b82de..5c7c248f62 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 diff --git a/MathlibTest/InstanceDiamonds.lean b/MathlibTest/InstanceDiamonds.lean index 1e75f7ca3c..327a41be8d 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 0000000000..793d3d2f5c --- /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/Linter/Show.lean b/MathlibTest/Linter/Show.lean new file mode 100644 index 0000000000..ae04e466c8 --- /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 diff --git a/MathlibTest/Tactic/ITauto.lean b/MathlibTest/Tactic/ITauto.lean index 177ded212a..d18466aad2 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 3f91b2bfb6..3bcad6d0bb 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 diff --git a/lake-manifest.json b/lake-manifest.json index f7e0737aa1..43aaa30cab 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", diff --git a/upstream_sha b/upstream_sha index 22681d1d19..63df27b53e 100644 --- a/upstream_sha +++ b/upstream_sha @@ -1 +1 @@ -12ab8e82f8447fa639dabe9ffeda74436b72be31 +60af7185ecf32ed5cab100f9960f1d588b9a6cab