diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 24afa16185062..63659be3aa6e1 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -224,12 +224,6 @@ jobs: lake build --no-build fi - - name: find `#`-commands - id: hash_commands - run: | - chmod u+x scripts/lint_hash_commands.sh - ./scripts/lint_hash_commands.sh - - name: build archive id: archive run: | diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 10590803248f5..201c075a32be2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -231,12 +231,6 @@ jobs: lake build --no-build fi - - name: find `#`-commands - id: hash_commands - run: | - chmod u+x scripts/lint_hash_commands.sh - ./scripts/lint_hash_commands.sh - - name: build archive id: archive run: | diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index 1ee3f32a4b4e2..3ecf1f47bfd46 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -210,12 +210,6 @@ jobs: lake build --no-build fi - - name: find `#`-commands - id: hash_commands - run: | - chmod u+x scripts/lint_hash_commands.sh - ./scripts/lint_hash_commands.sh - - name: build archive id: archive run: | diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 4fa4beff88dcd..f08a4ed49461a 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -228,12 +228,6 @@ jobs: lake build --no-build fi - - name: find `#`-commands - id: hash_commands - run: | - chmod u+x scripts/lint_hash_commands.sh - ./scripts/lint_hash_commands.sh - - name: build archive id: archive run: | diff --git a/.github/workflows/label_new_contributor.yml b/.github/workflows/label_new_contributor.yml index f3690fcef1316..b480b3439f971 100644 --- a/.github/workflows/label_new_contributor.yml +++ b/.github/workflows/label_new_contributor.yml @@ -42,7 +42,7 @@ jobs: } // Create a check run with a message about the PR count by this author - const message = `Found ${pullRequestCount} PRs by this author.`; + const message = `Found ${pullRequestCount} PRs by ${creator}.`; await github.rest.checks.create({ owner, repo, diff --git a/.vscode/deprecated-alias.code-snippets b/.vscode/deprecated-alias.code-snippets new file mode 100644 index 0000000000000..c760b46045763 --- /dev/null +++ b/.vscode/deprecated-alias.code-snippets @@ -0,0 +1,9 @@ +{ + "Deprecated alias for mathlib": { + "scope": "lean4", + "prefix": "deprecated alias", + "body": [ + "@[deprecated (since := \"${CURRENT_YEAR}-${CURRENT_MONTH}-${CURRENT_DATE}\")] alias $1 := $2" + ] + } +} diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean index 1c65ea043659f..52dd51500bda3 100644 --- a/Archive/Wiedijk100Theorems/Partition.lean +++ b/Archive/Wiedijk100Theorems/Partition.lean @@ -201,8 +201,8 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ) simp only [smul_eq_mul, ne_eq, mul_eq_zero, Multiset.count_eq_zero] rw [not_or, not_not] simp only [Multiset.mem_toFinset, not_not, mem_filter] } - refine Finset.card_congr φ ?_ ?_ ?_ - · intro a ha + refine Finset.card_bij φ ?_ ?_ ?_ + · intro a ha simp only [φ, not_forall, not_exists, not_and, exists_prop, mem_filter] rw [mem_piAntidiagonal'] dsimp only [ne_eq, smul_eq_mul, id_eq, eq_mpr_eq_cast, le_eq_subset, Finsupp.coe_mk] @@ -221,7 +221,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ) apply ha.2 · exact fun i _ => ⟨Multiset.count i a.parts, ha.1 i, rfl⟩ · dsimp only - intro p₁ p₂ hp₁ hp₂ h + intro p₁ hp₁ p₂ hp₂ h apply Nat.Partition.ext simp only [true_and_iff, mem_univ, mem_filter] at hp₁ hp₂ ext i diff --git a/Mathlib.lean b/Mathlib.lean index 3884a8feccce1..30aec0034855d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -265,6 +265,7 @@ import Mathlib.Algebra.GroupWithZero.NonZeroDivisors import Mathlib.Algebra.GroupWithZero.Pi import Mathlib.Algebra.GroupWithZero.Prod import Mathlib.Algebra.GroupWithZero.Semiconj +import Mathlib.Algebra.GroupWithZero.ULift import Mathlib.Algebra.GroupWithZero.Units.Basic import Mathlib.Algebra.GroupWithZero.Units.Equiv import Mathlib.Algebra.GroupWithZero.Units.Lemmas @@ -1079,6 +1080,7 @@ import Mathlib.Analysis.NormedSpace.Star.Spectrum import Mathlib.Analysis.NormedSpace.Star.Unitization import Mathlib.Analysis.NormedSpace.TrivSqZeroExt import Mathlib.Analysis.NormedSpace.Unitization +import Mathlib.Analysis.NormedSpace.UnitizationL1 import Mathlib.Analysis.NormedSpace.Units import Mathlib.Analysis.NormedSpace.WeakDual import Mathlib.Analysis.NormedSpace.WithLp @@ -1975,6 +1977,7 @@ import Mathlib.Data.List.Indexes import Mathlib.Data.List.Infix import Mathlib.Data.List.InsertNth import Mathlib.Data.List.Intervals +import Mathlib.Data.List.Iterate import Mathlib.Data.List.Join import Mathlib.Data.List.Lattice import Mathlib.Data.List.Lemmas @@ -3081,6 +3084,7 @@ import Mathlib.NumberTheory.LSeries.Convergence import Mathlib.NumberTheory.LSeries.Convolution import Mathlib.NumberTheory.LSeries.Deriv import Mathlib.NumberTheory.LSeries.Dirichlet +import Mathlib.NumberTheory.LSeries.HurwitzZeta import Mathlib.NumberTheory.LSeries.HurwitzZetaEven import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd import Mathlib.NumberTheory.LSeries.Linearity @@ -3780,6 +3784,7 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter +import Mathlib.Tactic.Linter.AttributeInstanceIn import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint import Mathlib.Tactic.Linter.TextBased diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean index c06311fb1ff1b..0953aae7d8d2b 100644 --- a/Mathlib/Algebra/BigOperators/Finsupp.lean +++ b/Mathlib/Algebra/BigOperators/Finsupp.lean @@ -166,7 +166,7 @@ theorem onFinset_prod {s : Finset α} {f : α → M} {g : α → M → N} (hf : /-- Taking a product over `f : α →₀ M` is the same as multiplying the value on a single element `y ∈ f.support` by the product over `erase y f`. -/ @[to_additive - " Taking a sum over over `f : α →₀ M` is the same as adding the value on a + " Taking a sum over `f : α →₀ M` is the same as adding the value on a single element `y ∈ f.support` to the sum over `erase y f`. "] theorem mul_prod_erase (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) : g y (f y) * (erase y f).prod g = f.prod g := by diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean index 73a12759cbadb..636bc00ed574e 100644 --- a/Mathlib/Algebra/BigOperators/Intervals.lean +++ b/Mathlib/Algebra/BigOperators/Intervals.lean @@ -146,6 +146,11 @@ theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : #align finset.prod_Ioc_succ_top Finset.prod_Ioc_succ_top #align finset.sum_Ioc_succ_top Finset.sum_Ioc_succ_top +@[to_additive] +theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : + (∏ k in Icc a (b + 1), f k) = (∏ k in Icc a b, f k) * f (b + 1) := by + rw [← Nat.Ico_succ_right, prod_Ico_succ_top hab, Nat.Ico_succ_right] + @[to_additive] theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : ((∏ k in range m, f k) * ∏ k in Ico m n, f k) = ∏ k in range n, f k := diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean index a1559d8a93b06..d2332d61bef96 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean @@ -95,9 +95,9 @@ theorem nth_stream_fr_lt_one {ifp_n : IntFractPair K} theorem one_le_succ_nth_stream_b {ifp_succ_n : IntFractPair K} (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : 1 ≤ ifp_succ_n.b := by obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ : - ∃ ifp_n, - IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n - · exact succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq + ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 + ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n := + succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq suffices 1 ≤ ifp_n.fr⁻¹ by rwa [IntFractPair.of, le_floor, cast_one] suffices ifp_n.fr ≤ 1 by have h : 0 < ifp_n.fr := @@ -473,9 +473,9 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) : ∃ ifp_succ_n, IntFractPair.stream v (n + 1) = some ifp_succ_n ∧ (ifp_succ_n.b : K) = gp.b := IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some s_nth_eq obtain ⟨ifp_n, stream_nth_eq, stream_nth_fr_ne_zero, if_of_eq_ifp_succ_n⟩ : - ∃ ifp_n, - IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n - · exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq + ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 + ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n := + IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq let denom' := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b) -- now we can use `sub_convergents_eq` to simplify our goal suffices |(-1) ^ n / denom'| ≤ 1 / denom by diff --git a/Mathlib/Algebra/Field/ULift.lean b/Mathlib/Algebra/Field/ULift.lean index bf03b5ea4b8e4..1f1e68eb002d1 100644 --- a/Mathlib/Algebra/Field/ULift.lean +++ b/Mathlib/Algebra/Field/ULift.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ import Mathlib.Algebra.Field.Basic -import Mathlib.Algebra.Group.ULift +import Mathlib.Algebra.GroupWithZero.ULift #align_import algebra.field.ulift from "leanprover-community/mathlib"@"13e18cfa070ea337ea960176414f5ae3a1534aae" diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 7022b2e4779ee..bf143a412f44c 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/Mathlib/Algebra/GCDMonoid/Basic.lean @@ -925,9 +925,9 @@ theorem lcm_eq_of_associated_right [NormalizedGCDMonoid α] {m n : α} (h : Asso end LCM -@[deprecated] alias GCDMonoid.prime_of_irreducible := Irreducible.prime +@[deprecated (since := "2024-02-12")] alias GCDMonoid.prime_of_irreducible := Irreducible.prime #align gcd_monoid.prime_of_irreducible Irreducible.prime -@[deprecated] alias GCDMonoid.irreducible_iff_prime := irreducible_iff_prime +@[deprecated (since := "2024-02-12")] alias GCDMonoid.irreducible_iff_prime := irreducible_iff_prime #align gcd_monoid.irreducible_iff_prime irreducible_iff_prime end GCDMonoid diff --git a/Mathlib/Algebra/Group/Aut.lean b/Mathlib/Algebra/Group/Aut.lean index b3a86a3f08ff0..d08ca486b6c95 100644 --- a/Mathlib/Algebra/Group/Aut.lean +++ b/Mathlib/Algebra/Group/Aut.lean @@ -27,6 +27,9 @@ equivalences (and other files that use them) before the group structure is defin MulAut, AddAut -/ +-- TODO after #13161 +-- assert_not_exists MonoidWithZero +assert_not_exists Ring variable {A : Type*} {M : Type*} {G : Type*} diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 982435dc36c1f..9bd20e5d61cfc 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/Mathlib/Algebra/Group/Basic.lean @@ -22,6 +22,8 @@ one-liners from the corresponding axioms. For the definitions of semigroups, mon `Algebra/Group/Defs.lean`. -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered open Function @@ -1134,14 +1136,14 @@ theorem leftInverse_inv_mul_mul_right (c : G) : lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1 := by cases n <;> simp set_option linter.existingAttributeWarning false in -@[to_additive, deprecated pow_natAbs_eq_one] +@[to_additive, deprecated pow_natAbs_eq_one (since := "2024-02-14")] lemma exists_pow_eq_one_of_zpow_eq_one (hn : n ≠ 0) (h : a ^ n = 1) : ∃ n : ℕ, 0 < n ∧ a ^ n = 1 := ⟨_, Int.natAbs_pos.2 hn, pow_natAbs_eq_one.2 h⟩ #align exists_npow_eq_one_of_zpow_eq_one exists_pow_eq_one_of_zpow_eq_one #align exists_nsmul_eq_zero_of_zsmul_eq_zero exists_nsmul_eq_zero_of_zsmul_eq_zero --- 2024-02-14 -attribute [deprecated natAbs_nsmul_eq_zero] exists_nsmul_eq_zero_of_zsmul_eq_zero +attribute [deprecated natAbs_nsmul_eq_zero (since := "2024-02-14")] +exists_nsmul_eq_zero_of_zsmul_eq_zero @[to_additive sub_nsmul] lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := diff --git a/Mathlib/Algebra/Group/Commutator.lean b/Mathlib/Algebra/Group/Commutator.lean index da8ced243a55e..e5d9c59e159c4 100644 --- a/Mathlib/Algebra/Group/Commutator.lean +++ b/Mathlib/Algebra/Group/Commutator.lean @@ -12,6 +12,9 @@ import Mathlib.Data.Bracket # The bracket on a group given by commutator. -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + /-- The commutator of two elements `g₁` and `g₂`. -/ instance commutatorElement {G : Type*} [Group G] : Bracket G G := ⟨fun g₁ g₂ ↦ g₁ * g₂ * g₁⁻¹ * g₂⁻¹⟩ diff --git a/Mathlib/Algebra/Group/ConjFinite.lean b/Mathlib/Algebra/Group/ConjFinite.lean index 22d4d01d0f40c..a3a572573e444 100644 --- a/Mathlib/Algebra/Group/ConjFinite.lean +++ b/Mathlib/Algebra/Group/ConjFinite.lean @@ -13,6 +13,8 @@ import Mathlib.Data.Fintype.Units # Conjugacy of elements of finite groups -/ +-- TODO: After #13027, +-- assert_not_exists MonoidWithZero variable {α : Type*} [Monoid α] diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 81a02bb829d63..21ed6414fdeb2 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -46,6 +46,9 @@ See the module `Algebra.AddTorsor` for a motivating example for the name `VAdd` -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + universe u v w open Function diff --git a/Mathlib/Algebra/Group/Embedding.lean b/Mathlib/Algebra/Group/Embedding.lean index 640621ad8f42c..4c7c2dfac7e2c 100644 --- a/Mathlib/Algebra/Group/Embedding.lean +++ b/Mathlib/Algebra/Group/Embedding.lean @@ -12,6 +12,8 @@ import Mathlib.Logic.Embedding.Basic # The embedding of a cancellative semigroup into itself by multiplication by a fixed element. -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered variable {G : Type*} diff --git a/Mathlib/Algebra/Group/Even.lean b/Mathlib/Algebra/Group/Even.lean index 7b29192b52221..0cf2efecf7fe1 100644 --- a/Mathlib/Algebra/Group/Even.lean +++ b/Mathlib/Algebra/Group/Even.lean @@ -32,6 +32,7 @@ This file defines square and even elements in a monoid. -/ assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered open MulOpposite diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean index 5ab9b96ea7658..4785a3aac44b0 100644 --- a/Mathlib/Algebra/Group/Ext.lean +++ b/Mathlib/Algebra/Group/Ext.lean @@ -27,6 +27,9 @@ former uses `HMul.hMul` which is the canonical spelling. monoid, group, extensionality -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + open Function universe u diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean index 17c38a3e825a4..4391444980ece 100644 --- a/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/Mathlib/Algebra/Group/Hom/Defs.lean @@ -620,84 +620,96 @@ end MonoidHom section Deprecated /-- Deprecated: use `DFunLike.congr_fun` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_fun` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_fun` instead."] theorem OneHom.congr_fun [One M] [One N] {f g : OneHom M N} (h : f = g) (x : M) : f x = g x := DFunLike.congr_fun h x #align one_hom.congr_fun OneHom.congr_fun #align zero_hom.congr_fun ZeroHom.congr_fun /-- Deprecated: use `DFunLike.congr_fun` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_fun` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_fun` instead."] theorem MulHom.congr_fun [Mul M] [Mul N] {f g : M →ₙ* N} (h : f = g) (x : M) : f x = g x := DFunLike.congr_fun h x #align mul_hom.congr_fun MulHom.congr_fun #align add_hom.congr_fun AddHom.congr_fun /-- Deprecated: use `DFunLike.congr_fun` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_fun` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_fun` instead."] theorem MonoidHom.congr_fun [MulOneClass M] [MulOneClass N] {f g : M →* N} (h : f = g) (x : M) : f x = g x := DFunLike.congr_fun h x #align monoid_hom.congr_fun MonoidHom.congr_fun #align add_monoid_hom.congr_fun AddMonoidHom.congr_fun /-- Deprecated: use `DFunLike.congr_arg` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_arg` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_arg` instead."] theorem OneHom.congr_arg [One M] [One N] (f : OneHom M N) {x y : M} (h : x = y) : f x = f y := DFunLike.congr_arg f h #align one_hom.congr_arg OneHom.congr_arg #align zero_hom.congr_arg ZeroHom.congr_arg /-- Deprecated: use `DFunLike.congr_arg` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_arg` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_arg` instead."] theorem MulHom.congr_arg [Mul M] [Mul N] (f : M →ₙ* N) {x y : M} (h : x = y) : f x = f y := DFunLike.congr_arg f h #align mul_hom.congr_arg MulHom.congr_arg #align add_hom.congr_arg AddHom.congr_arg /-- Deprecated: use `DFunLike.congr_arg` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.congr_arg` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.congr_arg` instead."] theorem MonoidHom.congr_arg [MulOneClass M] [MulOneClass N] (f : M →* N) {x y : M} (h : x = y) : f x = f y := DFunLike.congr_arg f h #align monoid_hom.congr_arg MonoidHom.congr_arg #align add_monoid_hom.congr_arg AddMonoidHom.congr_arg /-- Deprecated: use `DFunLike.coe_injective` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.coe_injective` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.coe_injective` instead."] theorem OneHom.coe_inj [One M] [One N] ⦃f g : OneHom M N⦄ (h : (f : M → N) = g) : f = g := DFunLike.coe_injective h #align one_hom.coe_inj OneHom.coe_inj #align zero_hom.coe_inj ZeroHom.coe_inj /-- Deprecated: use `DFunLike.coe_injective` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.coe_injective` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.coe_injective` instead."] theorem MulHom.coe_inj [Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : (f : M → N) = g) : f = g := DFunLike.coe_injective h #align mul_hom.coe_inj MulHom.coe_inj #align add_hom.coe_inj AddHom.coe_inj /-- Deprecated: use `DFunLike.coe_injective` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.coe_injective` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.coe_injective` instead."] theorem MonoidHom.coe_inj [MulOneClass M] [MulOneClass N] ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g := DFunLike.coe_injective h #align monoid_hom.coe_inj MonoidHom.coe_inj #align add_monoid_hom.coe_inj AddMonoidHom.coe_inj /-- Deprecated: use `DFunLike.ext_iff` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.ext_iff` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.ext_iff` instead."] theorem OneHom.ext_iff [One M] [One N] {f g : OneHom M N} : f = g ↔ ∀ x, f x = g x := DFunLike.ext_iff #align one_hom.ext_iff OneHom.ext_iff #align zero_hom.ext_iff ZeroHom.ext_iff /-- Deprecated: use `DFunLike.ext_iff` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.ext_iff` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.ext_iff` instead."] theorem MulHom.ext_iff [Mul M] [Mul N] {f g : M →ₙ* N} : f = g ↔ ∀ x, f x = g x := DFunLike.ext_iff #align mul_hom.ext_iff MulHom.ext_iff #align add_hom.ext_iff AddHom.ext_iff /-- Deprecated: use `DFunLike.ext_iff` instead. -/ -@[to_additive (attr := deprecated) "Deprecated: use `DFunLike.ext_iff` instead."] +@[to_additive (attr := deprecated (since := "2022-12-03")) + "Deprecated: use `DFunLike.ext_iff` instead."] theorem MonoidHom.ext_iff [MulOneClass M] [MulOneClass N] {f g : M →* N} : f = g ↔ ∀ x, f x = g x := DFunLike.ext_iff #align monoid_hom.ext_iff MonoidHom.ext_iff diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean index 9cc36891c8f0d..5cddfdee71b35 100644 --- a/Mathlib/Algebra/Group/InjSurj.lean +++ b/Mathlib/Algebra/Group/InjSurj.lean @@ -44,6 +44,8 @@ namespace Function ### Injective -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered namespace Injective diff --git a/Mathlib/Algebra/Group/MinimalAxioms.lean b/Mathlib/Algebra/Group/MinimalAxioms.lean index c631b801a8b8b..c4021598ec5ba 100644 --- a/Mathlib/Algebra/Group/MinimalAxioms.lean +++ b/Mathlib/Algebra/Group/MinimalAxioms.lean @@ -21,6 +21,9 @@ equalities. -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + universe u /-- Define a `Group` structure on a Type by proving `∀ a, 1 * a = a` and diff --git a/Mathlib/Algebra/Group/Nat.lean b/Mathlib/Algebra/Group/Nat.lean index c71f440f5ec23..c0b4e542b6893 100644 --- a/Mathlib/Algebra/Group/Nat.lean +++ b/Mathlib/Algebra/Group/Nat.lean @@ -17,7 +17,8 @@ This file contains the additive and multiplicative monoid instances on the natur See note [foundational algebra order theory]. -/ -assert_not_exists Ring +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered open Multiplicative diff --git a/Mathlib/Algebra/Group/NatPowAssoc.lean b/Mathlib/Algebra/Group/NatPowAssoc.lean index c1663f1cd8a05..fec3507c7b217 100644 --- a/Mathlib/Algebra/Group/NatPowAssoc.lean +++ b/Mathlib/Algebra/Group/NatPowAssoc.lean @@ -34,6 +34,8 @@ We also produce the following instances: -/ +assert_not_exists DenselyOrdered + variable {M : Type*} /-- A mixin for power-associative multiplication. -/ diff --git a/Mathlib/Algebra/Group/Opposite.lean b/Mathlib/Algebra/Group/Opposite.lean index 79799a4e30be1..4c0e2cb5035c3 100644 --- a/Mathlib/Algebra/Group/Opposite.lean +++ b/Mathlib/Algebra/Group/Opposite.lean @@ -17,6 +17,9 @@ import Mathlib.Tactic.Spread # Group structures on the multiplicative and additive opposites -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + variable {α : Type*} namespace MulOpposite diff --git a/Mathlib/Algebra/Group/Pi/Basic.lean b/Mathlib/Algebra/Group/Pi/Basic.lean index 8d79b935e57ff..4908949209457 100644 --- a/Mathlib/Algebra/Group/Pi/Basic.lean +++ b/Mathlib/Algebra/Group/Pi/Basic.lean @@ -150,7 +150,7 @@ theorem pow_comp [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) Porting note: `bit0` and `bit1` are deprecated. This section can be removed entirely (without replacement?). -/ -section deprecated +section deprecated -- since the port, 2022-11-28 set_option linter.deprecated false diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 860da445fbcf0..c757eb6783c1a 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/Mathlib/Algebra/Group/Prod.lean @@ -34,6 +34,7 @@ We also prove trivial `simp` lemmas, and define the following operations on `Mon assert_not_exists MonoidWithZero -- TODO: -- assert_not_exists AddMonoidWithOne +assert_not_exists DenselyOrdered variable {A : Type*} {B : Type*} {G : Type*} {H : Type*} {M : Type*} {N : Type*} {P : Type*} diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean index b51927f7ca4b4..bbea749a4e42c 100644 --- a/Mathlib/Algebra/Group/TypeTags.lean +++ b/Mathlib/Algebra/Group/TypeTags.lean @@ -32,6 +32,9 @@ This file is similar to `Order.Synonym`. -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered + universe u v variable {α : Type u} {β : Type v} diff --git a/Mathlib/Algebra/Group/ULift.lean b/Mathlib/Algebra/Group/ULift.lean index 78df422df7eb3..63cfb7412a220 100644 --- a/Mathlib/Algebra/Group/ULift.lean +++ b/Mathlib/Algebra/Group/ULift.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import Mathlib.Algebra.Group.Equiv.Basic -import Mathlib.Algebra.GroupWithZero.InjSurj -import Mathlib.Data.Int.Cast.Defs +import Mathlib.Algebra.Group.InjSurj import Mathlib.Logic.Nontrivial.Basic #align_import algebra.group.ulift from "leanprover-community/mathlib"@"564bcc44d2b394a50c0cd6340c14a6b02a50a99a" @@ -20,6 +19,8 @@ This file defines instances for group, monoid, semigroup and related structures We also provide `MulEquiv.ulift : ULift R ≃* R` (and its additive analogue). -/ +assert_not_exists MonoidWithZero +assert_not_exists DenselyOrdered universe u v @@ -127,10 +128,6 @@ instance mulOneClass [MulOneClass α] : MulOneClass (ULift α) := #align ulift.mul_one_class ULift.mulOneClass #align ulift.add_zero_class ULift.addZeroClass -instance mulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass (ULift α) := - Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl) -#align ulift.mul_zero_one_class ULift.mulZeroOneClass - @[to_additive] instance monoid [Monoid α] : Monoid (ULift α) := Equiv.ulift.injective.monoid _ rfl (fun _ _ => rfl) fun _ _ => rfl @@ -191,14 +188,6 @@ instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne ( { ULift.addMonoidWithOne, ULift.addCommMonoid with } #align ulift.add_comm_monoid_with_one ULift.addCommMonoidWithOne -instance monoidWithZero [MonoidWithZero α] : MonoidWithZero (ULift α) := - Equiv.ulift.injective.monoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl -#align ulift.monoid_with_zero ULift.monoidWithZero - -instance commMonoidWithZero [CommMonoidWithZero α] : CommMonoidWithZero (ULift α) := - Equiv.ulift.injective.commMonoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl -#align ulift.comm_monoid_with_zero ULift.commMonoidWithZero - @[to_additive] instance divInvMonoid [DivInvMonoid α] : DivInvMonoid (ULift α) := Equiv.ulift.injective.divInvMonoid _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) @@ -231,16 +220,6 @@ instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne (ULi { ULift.addGroupWithOne, ULift.addCommGroup with } #align ulift.add_comm_group_with_one ULift.addCommGroupWithOne -instance groupWithZero [GroupWithZero α] : GroupWithZero (ULift α) := - Equiv.ulift.injective.groupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) - (fun _ _ => rfl) fun _ _ => rfl -#align ulift.group_with_zero ULift.groupWithZero - -instance commGroupWithZero [CommGroupWithZero α] : CommGroupWithZero (ULift α) := - Equiv.ulift.injective.commGroupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) - (fun _ _ => rfl) fun _ _ => rfl -#align ulift.comm_group_with_zero ULift.commGroupWithZero - @[to_additive] instance leftCancelSemigroup [LeftCancelSemigroup α] : LeftCancelSemigroup (ULift α) := Equiv.ulift.injective.leftCancelSemigroup _ fun _ _ => rfl diff --git a/Mathlib/Algebra/Group/UniqueProds.lean b/Mathlib/Algebra/Group/UniqueProds.lean index 3f7074753a490..2bb53a72a536b 100644 --- a/Mathlib/Algebra/Group/UniqueProds.lean +++ b/Mathlib/Algebra/Group/UniqueProds.lean @@ -458,8 +458,8 @@ open UniqueMul in obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i)) rw [mem_image, ← filter_nonempty_iff] at hA hB let A' := A.filter (· i = ai); let B' := B.filter (· i = bi) - obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 - · rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB + obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 := by + rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB by_cases hA' : A' = A · rw [hA'] exact ihB B' (hc.2 bi) hB diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean index d4df28f51c18e..d7431e4fc1541 100644 --- a/Mathlib/Algebra/Group/Units.lean +++ b/Mathlib/Algebra/Group/Units.lean @@ -35,6 +35,7 @@ The results here should be used to golf the basic `Group` lemmas. -/ assert_not_exists Multiplicative +assert_not_exists MonoidWithZero assert_not_exists DenselyOrdered open Function diff --git a/Mathlib/Algebra/GroupWithZero/Hom.lean b/Mathlib/Algebra/GroupWithZero/Hom.lean index 9bf365b7100d4..f6e8883cfee37 100644 --- a/Mathlib/Algebra/GroupWithZero/Hom.lean +++ b/Mathlib/Algebra/GroupWithZero/Hom.lean @@ -145,7 +145,7 @@ lemma toMonoidHom_coe (f : α →*₀ β) : f.toMonoidHom.toFun = f := rfl @[ext] lemma ext ⦃f g : α →*₀ β⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h #align monoid_with_zero_hom.ext MonoidWithZeroHom.ext -section Deprecated +section Deprecated -- since 2022-12-03 @[deprecated DFunLike.congr_fun] lemma congr_fun {f g : α →*₀ β} (h : f = g) (x : α) : f x = g x := DFunLike.congr_fun h x diff --git a/Mathlib/Algebra/GroupWithZero/ULift.lean b/Mathlib/Algebra/GroupWithZero/ULift.lean new file mode 100644 index 0000000000000..115d3406dc4f6 --- /dev/null +++ b/Mathlib/Algebra/GroupWithZero/ULift.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2020 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import Mathlib.Algebra.Group.ULift +import Mathlib.Algebra.GroupWithZero.InjSurj + +#align_import algebra.group.ulift from "leanprover-community/mathlib"@"564bcc44d2b394a50c0cd6340c14a6b02a50a99a" + +/-! +# `ULift` instances for groups and monoids with zero + +This file defines instances for group and monoid with zero and related structures on `ULift` types. + +(Recall `ULift α` is just a "copy" of a type `α` in a higher universe.) +-/ + + +universe u + +variable {α : Type u} + +namespace ULift + +instance mulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass (ULift α) := + Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl) +#align ulift.mul_zero_one_class ULift.mulZeroOneClass + +instance monoidWithZero [MonoidWithZero α] : MonoidWithZero (ULift α) := + Equiv.ulift.injective.monoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl +#align ulift.monoid_with_zero ULift.monoidWithZero + +instance commMonoidWithZero [CommMonoidWithZero α] : CommMonoidWithZero (ULift α) := + Equiv.ulift.injective.commMonoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl +#align ulift.comm_monoid_with_zero ULift.commMonoidWithZero + +instance groupWithZero [GroupWithZero α] : GroupWithZero (ULift α) := + Equiv.ulift.injective.groupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) + (fun _ _ => rfl) fun _ _ => rfl +#align ulift.group_with_zero ULift.groupWithZero + +instance commGroupWithZero [CommGroupWithZero α] : CommGroupWithZero (ULift α) := + Equiv.ulift.injective.commGroupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) + (fun _ _ => rfl) fun _ _ => rfl +#align ulift.comm_group_with_zero ULift.commGroupWithZero + +end ULift diff --git a/Mathlib/Algebra/Lie/Sl2.lean b/Mathlib/Algebra/Lie/Sl2.lean index e9219d1f6d0d2..ebc408c9554e0 100644 --- a/Mathlib/Algebra/Lie/Sl2.lean +++ b/Mathlib/Algebra/Lie/Sl2.lean @@ -106,7 +106,11 @@ lemma lie_h_pow_toEnd_f (n : ℕ) : congr ring -lemma lie_f_pow_toEnd_f (n : ℕ) : +-- Although this is true by definition, we include this lemma (and the assumption) to mirror the API +-- for `lie_h_pow_toEnd_f` and `lie_e_pow_succ_toEnd_f`. +set_option linter.unusedVariables false in +@[nolint unusedArguments] +lemma lie_f_pow_toEnd_f (P : HasPrimitiveVectorWith t m μ) (n : ℕ) : ⁅f, ψ n⁆ = ψ (n + 1) := by simp [pow_succ'] @@ -117,7 +121,7 @@ lemma lie_e_pow_succ_toEnd_f (n : ℕ) : pow_zero, LinearMap.one_apply, leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero, add_zero] · rw [pow_succ', LinearMap.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f, - lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f, ← add_smul, + lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul, Nat.cast_add, Nat.cast_one] congr ring @@ -141,6 +145,33 @@ lemma exists_nat [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZ (fun ⟨r, hr⟩ ↦ by simp [lie_h_pow_toEnd_f P, Classical.choose_spec hr, contra, Module.End.HasEigenvector, Module.End.mem_eigenspace_iff])).finite +lemma pow_toEnd_f_ne_zero_of_eq_nat + [CharZero R] [NoZeroSMulDivisors R M] + {n : ℕ} (hn : μ = n) {i} (hi : i ≤ n) : (ψ i) ≠ 0 := by + intro H + induction i + · exact P.ne_zero (by simpa using H) + · next i IH => + have : ((i + 1) * (n - i) : ℤ) • (toEnd R L M f ^ i) m = 0 := by + have := congr_arg (⁅e, ·⁆) H + simpa [zsmul_eq_smul_cast R, P.lie_e_pow_succ_toEnd_f, hn] using this + rw [zsmul_eq_smul_cast R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero, + Nat.cast_inj, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this + simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this + exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_lt i.lt_succ_self + +lemma pow_toEnd_f_eq_zero_of_eq_nat + [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] + {n : ℕ} (hn : μ = n) : (ψ (n + 1)) = 0 := by + by_contra h + have : t.HasPrimitiveVectorWith (ψ (n + 1)) (n - 2 * (n + 1) : R) := + { ne_zero := h + lie_h := (P.lie_h_pow_toEnd_f _).trans (by simp [hn]) + lie_e := (P.lie_e_pow_succ_toEnd_f _).trans (by simp [hn]) } + obtain ⟨m, hm⟩ := this.exists_nat + have : (n : ℤ) < m + 2 * (n + 1) := by linarith + exact this.ne (Int.cast_injective (α := R) <| by simpa [sub_eq_iff_eq_add] using hm) + end HasPrimitiveVectorWith end IsSl2Triple diff --git a/Mathlib/Algebra/Lie/Weights/Cartan.lean b/Mathlib/Algebra/Lie/Weights/Cartan.lean index e89e610c0d1cb..f69840bd74c32 100644 --- a/Mathlib/Algebra/Lie/Weights/Cartan.lean +++ b/Mathlib/Algebra/Lie/Weights/Cartan.lean @@ -69,6 +69,17 @@ theorem lie_mem_weightSpace_of_mem_weightSpace {χ₁ χ₂ : H → R} {x : L} { exact lie_mem_maxGenEigenspace_toEnd hx hm #align lie_algebra.lie_mem_weight_space_of_mem_weight_space LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace +lemma toEnd_pow_apply_mem {χ₁ χ₂ : H → R} {x : L} {m : M} + (hx : x ∈ rootSpace H χ₁) (hm : m ∈ weightSpace M χ₂) (n) : + (toEnd R L M x ^ n : Module.End R M) m ∈ weightSpace M (n • χ₁ + χ₂) := by + induction n + · simpa using hm + · next n IH => + simp only [pow_succ', LinearMap.mul_apply, toEnd_apply_apply, + Nat.cast_add, Nat.cast_one, rootSpace] + convert lie_mem_weightSpace_of_mem_weightSpace hx IH using 2 + rw [succ_nsmul, ← add_assoc, add_comm (n • _)] + variable (R L H M) /-- Auxiliary definition for `rootSpaceWeightSpaceProduct`, diff --git a/Mathlib/Algebra/Module/Submodule/Pointwise.lean b/Mathlib/Algebra/Module/Submodule/Pointwise.lean index 792b833e77324..a6299a7f6bf0e 100644 --- a/Mathlib/Algebra/Module/Submodule/Pointwise.lean +++ b/Mathlib/Algebra/Module/Submodule/Pointwise.lean @@ -379,8 +379,8 @@ instance : CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le := ⟨fun _ _ _ le => set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := le hm)⟩ --- 2024-03-31 -@[deprecated smul_mono_right] theorem set_smul_mono_right {p q : Submodule R M} (le : p ≤ q) : +@[deprecated smul_mono_right (since := "2024-03-31")] +theorem set_smul_mono_right {p q : Submodule R M} (le : p ≤ q) : s • p ≤ s • q := smul_mono_right s le diff --git a/Mathlib/Algebra/Module/ULift.lean b/Mathlib/Algebra/Module/ULift.lean index f46cf482dc2e6..dfacff0ab1c32 100644 --- a/Mathlib/Algebra/Module/ULift.lean +++ b/Mathlib/Algebra/Module/ULift.lean @@ -3,6 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ +import Mathlib.Algebra.GroupWithZero.ULift import Mathlib.Algebra.Ring.ULift import Mathlib.Algebra.Module.Equiv diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 93724265e04b5..6d389b8494e2d 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -299,7 +299,7 @@ lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / @[deprecated] alias div_le_div_of_le_left := div_le_div_of_nonneg_left @[deprecated] alias div_lt_div_of_lt_left := div_lt_div_of_pos_left -@[deprecated div_le_div_of_nonneg_right] +@[deprecated div_le_div_of_nonneg_right (since := "2024-02-16")] lemma div_le_div_of_le (hc : 0 ≤ c) (hab : a ≤ b) : a / c ≤ b / c := div_le_div_of_nonneg_right hab hc #align div_le_div_of_le div_le_div_of_le @@ -946,7 +946,7 @@ theorem IsLUB.mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => b * a) '' s) (b * a) := by simpa [mul_comm] using hs.mul_left ha #align is_lub.mul_right IsLUB.mul_right -/-! ### Miscellaneous lemmmas -/ +/-! ### Miscellaneous lemmas -/ theorem mul_sub_mul_div_mul_neg_iff (hc : c ≠ 0) (hd : d ≠ 0) : diff --git a/Mathlib/Algebra/Order/Group/Cone.lean b/Mathlib/Algebra/Order/Group/Cone.lean index 32c975c4d77e5..8c18fe36e97d0 100644 --- a/Mathlib/Algebra/Order/Group/Cone.lean +++ b/Mathlib/Algebra/Order/Group/Cone.lean @@ -12,7 +12,7 @@ import Mathlib.Algebra.Order.Group.Defs In this file we provide structures `PositiveCone` and `TotalPositiveCone` that encode axioms of `OrderedAddCommGroup` and `LinearOrderedAddCommGroup` -in terms of the the `(0 ≤ ·)` predicate. +in terms of the `(0 ≤ ·)` predicate. We also provide two constructors, `OrderedAddCommGroup.mkOfPositiveCone` and `LinearOrderedAddCommGroup.mkOfPositiveCone`, diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean index b6f980e56bbee..7480c539444e5 100644 --- a/Mathlib/Algebra/Polynomial/Laurent.lean +++ b/Mathlib/Algebra/Polynomial/Laurent.lean @@ -350,12 +350,10 @@ def trunc : R[T;T⁻¹] →+ R[X] := @[simp] theorem trunc_C_mul_T (n : ℤ) (r : R) : trunc (C r * T n) = ite (0 ≤ n) (monomial n.toNat r) 0 := by - -- Porting note: added. Should move elsewhere after the port. - have : Function.Injective Int.ofNat := fun x y h => Int.ofNat_inj.mp h apply (toFinsuppIso R).injective rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply] -- Porting note (#10691): was `rw` - erw [comapDomain.addMonoidHom_apply this] + erw [comapDomain.addMonoidHom_apply Int.ofNat_injective] rw [toFinsuppIso_apply] -- Porting note: rewrote proof below relative to mathlib3. by_cases n0 : 0 ≤ n diff --git a/Mathlib/Algebra/Polynomial/PartialFractions.lean b/Mathlib/Algebra/Polynomial/PartialFractions.lean index cc45918eb8d8d..55cbc67771c39 100644 --- a/Mathlib/Algebra/Polynomial/PartialFractions.lean +++ b/Mathlib/Algebra/Polynomial/PartialFractions.lean @@ -1,5 +1,5 @@ /- -Copyright (c) Sidharth Hariharan. All rights reserved. +Copyright (c) 2023 Sidharth Hariharan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kevin Buzzard, Sidharth Hariharan -/ diff --git a/Mathlib/Algebra/Star/Pointwise.lean b/Mathlib/Algebra/Star/Pointwise.lean index 4071fae8e5235..6ba000b8748c6 100644 --- a/Mathlib/Algebra/Star/Pointwise.lean +++ b/Mathlib/Algebra/Star/Pointwise.lean @@ -13,7 +13,7 @@ import Mathlib.Data.Set.Pointwise.Basic # Pointwise star operation on sets This file defines the star operation pointwise on sets and provides the basic API. -Besides basic facts about about how the star operation acts on sets (e.g., `(s ∩ t)⋆ = s⋆ ∩ t⋆`), +Besides basic facts about how the star operation acts on sets (e.g., `(s ∩ t)⋆ = s⋆ ∩ t⋆`), if `s t : Set α`, then under suitable assumption on `α`, it is shown * `(s + t)⋆ = s⋆ + t⋆` diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean index 897eb528fd7ce..ae5d5280a4b4c 100644 --- a/Mathlib/AlgebraicGeometry/Gluing.lean +++ b/Mathlib/AlgebraicGeometry/Gluing.lean @@ -95,7 +95,7 @@ variable (D : GlueData.{u}) local notation "𝖣" => D.toGlueData -/-- The glue data of locally ringed spaces spaces associated to a family of glue data of schemes. -/ +/-- The glue data of locally ringed spaces associated to a family of glue data of schemes. -/ abbrev toLocallyRingedSpaceGlueData : LocallyRingedSpace.GlueData := { f_open := D.f_open toGlueData := 𝖣.mapGlueData forgetToLocallyRingedSpace } diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean index d270ff0a7132e..7ac483f8631a1 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean @@ -202,7 +202,7 @@ set_option linter.uppercaseLean3 false in attribute [nolint simpNF] AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_map_apply -/-- Some glue, verifying that that structure presheaf valued in `CommRing` agrees with the `Type` +/-- Some glue, verifying that the structure presheaf valued in `CommRing` agrees with the `Type` valued structure presheaf. -/ def structurePresheafCompForget : structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat ≅ (structureSheafInType 𝒜).1 := diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean index 9cd13f24c9382..b5d56757ba737 100644 --- a/Mathlib/AlgebraicGeometry/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/Scheme.lean @@ -39,7 +39,7 @@ namespace AlgebraicGeometry /-- We define `Scheme` as an `X : LocallyRingedSpace`, along with a proof that every point has an open neighbourhood `U` -so that that the restriction of `X` to `U` is isomorphic, +so that the restriction of `X` to `U` is isomorphic, as a locally ringed space, to `Spec.toLocallyRingedSpace.obj (op R)` for some `R : CommRingCat`. -/ diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index fd3887822e940..6390da9f03714 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -250,7 +250,7 @@ set_option linter.uppercaseLean3 false in -- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing attribute [nolint simpNF] AlgebraicGeometry.structurePresheafInCommRing_map_apply -/-- Some glue, verifying that that structure presheaf valued in `CommRingCat` agrees +/-- Some glue, verifying that the structure presheaf valued in `CommRingCat` agrees with the `Type` valued structure presheaf. -/ def structurePresheafCompForget : diff --git a/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean b/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean index 2f90ef1515b8c..ec520c14e4640 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean @@ -90,7 +90,7 @@ obtained by composing the previous equivalence with the equivalences `SimplicialObject C ≌ Karoubi (SimplicialObject C)` and `Karoubi (ChainComplex C ℕ) ≌ ChainComplex C ℕ`. Instead, we polish this construction in `Compatibility.lean` by ensuring good definitional properties of the equivalence (e.g. -the inverse functor is definitionallly equal to +the inverse functor is definitionally equal to `Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject C`) and showing compatibilities for the unit and counit isomorphisms. diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean index 59d3d124b0613..75e1e77b26478 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean @@ -306,9 +306,9 @@ def biUnion (πi : ∀ J : Box ι, Prepartition J) : Prepartition I where rintro J₁' ⟨J₁, hJ₁, hJ₁'⟩ J₂' ⟨J₂, hJ₂, hJ₂'⟩ Hne rw [Function.onFun, Set.disjoint_left] rintro x hx₁ hx₂; apply Hne - obtain rfl : J₁ = J₂ - · exact π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂) - · exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂ + obtain rfl : J₁ = J₂ := + π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂) + exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂ #align box_integral.prepartition.bUnion BoxIntegral.Prepartition.biUnion variable {πi πi₁ πi₂ : ∀ J : Box ι, Prepartition J} diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean index 3039744f62616..60498ebed74b4 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean @@ -217,5 +217,5 @@ theorem isOpenMap_of_hasStrictFDerivAt_equiv [CompleteSpace E] {f : E → F} {f' (hf : ∀ x, HasStrictFDerivAt f (f' x : E →L[𝕜] F) x) : IsOpenMap f := isOpenMap_iff_nhds_le.2 fun x => (hf x).map_nhds_eq_of_equiv.ge #align open_map_of_strict_fderiv_equiv isOpenMap_of_hasStrictFDerivAt_equiv -@[deprecated] -- 2024-03-23 +@[deprecated (since := "2024-03-23")] alias open_map_of_strict_fderiv_equiv := isOpenMap_of_hasStrictFDerivAt_equiv diff --git a/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean b/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean index 936c72d70644c..4503981dbd049 100644 --- a/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean +++ b/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean @@ -79,7 +79,7 @@ theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, deriv f c = 0 := by by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x · exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt - · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x - · push_neg at h; exact h + · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := by + push_neg at h; exact h exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩ #align exists_deriv_eq_zero' exists_deriv_eq_zero' diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean index 32c18a5ea18b9..97753ae714196 100644 --- a/Mathlib/Analysis/Calculus/MeanValue.lean +++ b/Mathlib/Analysis/Calculus/MeanValue.lean @@ -931,7 +931,7 @@ lemma strictMonoOn_of_hasDerivWithinAt_pos {D : Set ℝ} (hD : Convex ℝ D) {f strictMonoOn_of_deriv_pos hD hf fun x hx ↦ by rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx -@[deprecated] -- 2024-03-02 +@[deprecated (since := "2024-03-02")] alias StrictMonoOn_of_hasDerivWithinAt_pos := strictMonoOn_of_hasDerivWithinAt_pos /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then @@ -1007,7 +1007,7 @@ lemma strictAntiOn_of_hasDerivWithinAt_neg {D : Set ℝ} (hD : Convex ℝ D) {f strictAntiOn_of_deriv_neg hD hf fun x hx ↦ by rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx -@[deprecated] -- 2024-03-02 +@[deprecated (since := "2024-03-02")] alias StrictAntiOn_of_hasDerivWithinAt_pos := strictAntiOn_of_hasDerivWithinAt_neg /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then @@ -1016,7 +1016,7 @@ lemma strictAnti_of_hasDerivAt_neg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt (hf' : ∀ x, f' x < 0) : StrictAnti f := strictAnti_of_deriv_neg fun x ↦ by rw [(hf _).deriv]; exact hf' _ -@[deprecated] -- 2024-03-02 +@[deprecated (since := "2024-03-02")] alias strictAnti_of_hasDerivAt_pos := strictAnti_of_hasDerivAt_neg /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D` diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean index 87f4e4690649b..98a3a242d52c0 100644 --- a/Mathlib/Analysis/Complex/Basic.lean +++ b/Mathlib/Analysis/Complex/Basic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) Sébastien Gouëzel. All rights reserved. +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ diff --git a/Mathlib/Analysis/Complex/OperatorNorm.lean b/Mathlib/Analysis/Complex/OperatorNorm.lean index 36294f0fe07fa..8c7ef1743c0af 100644 --- a/Mathlib/Analysis/Complex/OperatorNorm.lean +++ b/Mathlib/Analysis/Complex/OperatorNorm.lean @@ -1,5 +1,5 @@ /- -Copyright (c) Sébastien Gouëzel. All rights reserved. +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel -/ diff --git a/Mathlib/Analysis/Complex/RealDeriv.lean b/Mathlib/Analysis/Complex/RealDeriv.lean index 8b8bfd0cb08d2..dea7dc9f9b3dd 100644 --- a/Mathlib/Analysis/Complex/RealDeriv.lean +++ b/Mathlib/Analysis/Complex/RealDeriv.lean @@ -1,5 +1,5 @@ /- -Copyright (c) Sébastien Gouëzel. All rights reserved. +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel, Yourong Zang -/ diff --git a/Mathlib/Analysis/Convex/Jensen.lean b/Mathlib/Analysis/Convex/Jensen.lean index cc361854aedfa..32eac80fc2afe 100644 --- a/Mathlib/Analysis/Convex/Jensen.lean +++ b/Mathlib/Analysis/Convex/Jensen.lean @@ -273,15 +273,15 @@ theorem ConvexOn.exists_ge_of_centerMass (h : ConvexOn 𝕜 s f) (hw₀ : ∀ i (hw₁ : 0 < ∑ i in t, w i) (hp : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i) := by set y := t.centerMass w p - obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i - rotate_left - · rw [mem_filter] at hi - exact ⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩ - have hw' : (0 : 𝕜) < ∑ i in filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero] - refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_ - rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ← - centerMass, centerMass_filter_ne_zero] - exact h.map_centerMass_le hw₀ hw₁ hp + -- TODO: can `rsuffices` be used to write the `exact` first, then the proof of this obtain? + obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i := by + have hw' : (0 : 𝕜) < ∑ i in filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero] + refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_ + rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ← + centerMass, centerMass_filter_ne_zero] + exact h.map_centerMass_le hw₀ hw₁ hp + rw [mem_filter] at hi + exact ⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩ #align convex_on.exists_ge_of_center_mass ConvexOn.exists_ge_of_centerMass /-- If a function `f` is concave on `s`, then the value it takes at some center of mass of points of diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean index d5e9ddbcf243f..50c45a6b71135 100644 --- a/Mathlib/Analysis/Fourier/FourierTransform.lean +++ b/Mathlib/Analysis/Fourier/FourierTransform.lean @@ -147,7 +147,7 @@ theorem fourierIntegral_convergent_iff (he : Continuous e) exact this #align vector_fourier.fourier_integral_convergent_iff VectorFourier.fourierIntegral_convergent_iff -@[deprecated] -- 2024-03-29 +@[deprecated (since := "2024-03-29")] alias fourier_integral_convergent_iff := VectorFourier.fourierIntegral_convergent_iff variable [CompleteSpace E] diff --git a/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean b/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean index c09b8e4bf6651..fa3acadf037d8 100644 --- a/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean +++ b/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean @@ -82,7 +82,7 @@ theorem isClosed_range (coercive : IsCoercive B) : IsClosed (range B♯ : Set V) exact antilipschitz.isClosed_range B♯.uniformContinuous #align is_coercive.closed_range IsCoercive.isClosed_range -@[deprecated] alias closed_range := isClosed_range -- 2024-03-29 +@[deprecated (since := "2024-03-19")] alias closed_range := isClosed_range theorem range_eq_top (coercive : IsCoercive B) : range B♯ = ⊤ := by haveI := coercive.isClosed_range.completeSpace_coe diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean index 9232781597d11..49d05076dcdfd 100644 --- a/Mathlib/Analysis/LocallyConvex/Bounded.lean +++ b/Mathlib/Analysis/LocallyConvex/Bounded.lean @@ -160,9 +160,9 @@ alias ⟨IsVonNBounded.tendsto_smallSets_nhds, _⟩ := isVonNBounded_iff_tendsto lemma isVonNBounded_pi_iff {𝕜 ι : Type*} {E : ι → Type*} [NormedDivisionRing 𝕜] [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)] {S : Set (∀ i, E i)} : IsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S) := by - simp only [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf, - smallSets_comap, tendsto_iInf, tendsto_lift', comp_apply, mem_powerset_iff, ← image_subset_iff, - ← image_smul, image_image, tendsto_smallSets_iff]; rfl + simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf, + smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp, + ← image_smul, image_image]; rfl section Image diff --git a/Mathlib/Analysis/NormedSpace/Unitization.lean b/Mathlib/Analysis/NormedSpace/Unitization.lean index 9966fa546a5d0..0a2171eca286f 100644 --- a/Mathlib/Analysis/NormedSpace/Unitization.lean +++ b/Mathlib/Analysis/NormedSpace/Unitization.lean @@ -18,14 +18,17 @@ two properties: - The embedding of `A` in `Unitization 𝕜 A` is an isometry. (i.e., `Isometry Unitization.inr`) One way to do this is to pull back the norm from `WithLp 1 (𝕜 × A)`, that is, -`‖(k, a)‖ = ‖k‖ + ‖a‖` using `Unitization.addEquiv` (i.e., the identity map). However, when the norm -on `A` is *regular* (i.e., `ContinuousLinearMap.mul` is an isometry), there is another natural -choice: the pullback of the norm on `𝕜 × (A →L[𝕜] A)` under the map +`‖(k, a)‖ = ‖k‖ + ‖a‖` using `Unitization.addEquiv` (i.e., the identity map). +This is implemented for the type synonym `WithLp 1 (Unitization 𝕜 A)` in +`WithLp.instUnitizationNormedAddCommGroup`, and it is shown there that this is a Banach algebra. +However, when the norm on `A` is *regular* (i.e., `ContinuousLinearMap.mul` is an isometry), there +is another natural choice: the pullback of the norm on `𝕜 × (A →L[𝕜] A)` under the map `(k, a) ↦ (k, k • 1 + ContinuousLinearMap.mul 𝕜 A a)`. It turns out that among all norms on the unitization satisfying the properties specified above, the norm inherited from `WithLp 1 (𝕜 × A)` is maximal, and the norm inherited from this pullback is minimal. +Of course, this means that `WithLp.equiv : WithLp 1 (Unitization 𝕜 A) → Unitization 𝕜 A` can be +upgraded to a continuous linear equivalence (when `𝕜` and `A` are complete). -For possibly non-unital `RegularNormedAlgebra`s `A` (over `𝕜`), we construct a `NormedAlgebra` structure on `Unitization 𝕜 A` using the pullback described above. The reason for choosing this norm is that for a C⋆-algebra `A` its norm is always regular, and the pullback norm on `Unitization 𝕜 A` is then also a C⋆-norm. diff --git a/Mathlib/Analysis/NormedSpace/UnitizationL1.lean b/Mathlib/Analysis/NormedSpace/UnitizationL1.lean new file mode 100644 index 0000000000000..1b074ef996d59 --- /dev/null +++ b/Mathlib/Analysis/NormedSpace/UnitizationL1.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2024 Jireh Loreaux. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jireh Loreaux +-/ +import Mathlib.Algebra.Algebra.Unitization +import Mathlib.Analysis.NormedSpace.ProdLp + +/-! # Unitization equipped with the $L^1$ norm + +In another file, the `Unitization 𝕜 A` of a non-unital normed `𝕜`-algebra `A` is equipped with the +norm inherited as the pullback via a map (closely related to) the left-regular representation of the +algebra on itself (see `Unitization.instNormedRing`). + +However, this construction is only valid (and an isometry) when `A` is a `RegularNormedAlgebra`. +Sometimes it is useful to consider the unitization of a non-unital algebra with the $L^1$ norm +instead. This file provides that norm on the type synonym `WithLp 1 (Unitization 𝕜 A)`, along +with the algebra isomomorphism between `Unitization 𝕜 A` and `WithLp 1 (Unitization 𝕜 A)`. +Note that `TrivSqZeroExt` is also equipped with the $L^1$ norm in the analogous way, but it is +registered as an instance without the type synonym. + +One application of this is a straightforward proof that the quasispectrum of an element in a +non-unital Banach algebra is compact, which can be established by passing to the unitization. +-/ + +variable (𝕜 A : Type*) [NormedField 𝕜] [NonUnitalNormedRing A] +variable [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] + +namespace WithLp + +open Unitization + +/-- The natural map between `Unitization 𝕜 A` and `𝕜 × A`, transferred to their `WithLp 1` +synonyms. -/ +noncomputable def unitization_addEquiv_prod : WithLp 1 (Unitization 𝕜 A) ≃+ WithLp 1 (𝕜 × A) := + (WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).toAddEquiv.trans <| + (addEquiv 𝕜 A).trans (WithLp.linearEquiv 1 𝕜 (𝕜 × A)).symm.toAddEquiv + +noncomputable instance instUnitizationNormedAddCommGroup : + NormedAddCommGroup (WithLp 1 (Unitization 𝕜 A)) := + NormedAddCommGroup.induced (WithLp 1 (Unitization 𝕜 A)) (WithLp 1 (𝕜 × A)) + (unitization_addEquiv_prod 𝕜 A) (AddEquiv.injective _) + +/-- Bundle `WithLp.unitization_addEquiv_prod` as a `UniformEquiv`. -/ +noncomputable def uniformEquiv_unitization_addEquiv_prod : + WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A) := + { unitization_addEquiv_prod 𝕜 A with + uniformContinuous_invFun := uniformContinuous_comap' uniformContinuous_id + uniformContinuous_toFun := uniformContinuous_iff.mpr le_rfl } + +instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] : + CompleteSpace (WithLp 1 (Unitization 𝕜 A)) := + completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).uniformEmbedding |>.mpr + CompleteSpace.prod + +variable {𝕜 A} + +open ENNReal in +lemma unitization_norm_def (x : WithLp 1 (Unitization 𝕜 A)) : + ‖x‖ = ‖(WithLp.equiv 1 _ x).fst‖ + ‖(WithLp.equiv 1 _ x).snd‖ := calc + ‖x‖ = (‖(WithLp.equiv 1 _ x).fst‖ ^ (1 : ℝ≥0∞).toReal + + ‖(WithLp.equiv 1 _ x).snd‖ ^ (1 : ℝ≥0∞).toReal) ^ (1 / (1 : ℝ≥0∞).toReal) := + WithLp.prod_norm_eq_add (by simp : 0 < (1 : ℝ≥0∞).toReal) _ + _ = ‖(WithLp.equiv 1 _ x).fst‖ + ‖(WithLp.equiv 1 _ x).snd‖ := by simp + +lemma unitization_nnnorm_def (x : WithLp 1 (Unitization 𝕜 A)) : + ‖x‖₊ = ‖(WithLp.equiv 1 _ x).fst‖₊ + ‖(WithLp.equiv 1 _ x).snd‖₊ := + Subtype.ext <| unitization_norm_def x + +lemma unitization_norm_inr (x : A) : ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm x‖ = ‖x‖ := by + simp [unitization_norm_def] + +lemma unitization_nnnorm_inr (x : A) : ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm x‖₊ = ‖x‖₊ := by + simp [unitization_nnnorm_def] + +lemma unitization_isometry_inr : + Isometry (fun x : A ↦ (WithLp.equiv 1 (Unitization 𝕜 A)).symm x) := + AddMonoidHomClass.isometry_of_norm + ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 A) + unitization_norm_inr + +instance instUnitizationRing : Ring (WithLp 1 (Unitization 𝕜 A)) := + inferInstanceAs (Ring (Unitization 𝕜 A)) + +@[simp] +lemma unitization_mul (x y : WithLp 1 (Unitization 𝕜 A)) : + WithLp.equiv 1 _ (x * y) = (WithLp.equiv 1 _ x) * (WithLp.equiv 1 _ y) := + rfl + +instance {R : Type*} [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] : + Algebra R (WithLp 1 (Unitization 𝕜 A)) := + inferInstanceAs (Algebra R (Unitization 𝕜 A)) + +@[simp] +lemma unitization_algebraMap (r : 𝕜) : + WithLp.equiv 1 _ (algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) r) = + algebraMap 𝕜 (Unitization 𝕜 A) r := + rfl + +/-- `WithLp.equiv` bundled as an algebra isomorphism with `Unitization 𝕜 A`. -/ +@[simps!] +def unitizationAlgEquiv (R : Type*) [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] + [IsScalarTower R 𝕜 A] : WithLp 1 (Unitization 𝕜 A) ≃ₐ[R] Unitization 𝕜 A := + { WithLp.equiv 1 (Unitization 𝕜 A) with + map_mul' := fun _ _ ↦ rfl + map_add' := fun _ _ ↦ rfl + commutes' := fun _ ↦ rfl } + +noncomputable instance instUnitizationNormedRing : NormedRing (WithLp 1 (Unitization 𝕜 A)) where + dist_eq := dist_eq_norm + norm_mul x y := by + simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul] + rw [add_assoc, add_assoc] + gcongr + · exact norm_mul_le _ _ + · apply (norm_add_le _ _).trans + gcongr + · simp [norm_smul] + · apply (norm_add_le _ _).trans + gcongr + · simp [norm_smul, mul_comm] + · exact norm_mul_le _ _ + +noncomputable instance instUnitizationNormedAlgebra : + NormedAlgebra 𝕜 (WithLp 1 (Unitization 𝕜 A)) where + norm_smul_le r x := by + simp_rw [unitization_norm_def, equiv_smul, fst_smul, snd_smul, norm_smul, mul_add] + exact le_rfl + +end WithLp diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean index 8d0bc0a6ef26e..3beb361bf6d6a 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exp.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exp.lean @@ -274,7 +274,7 @@ theorem tendsto_pow_mul_exp_neg_atTop_nhds_zero (n : ℕ) : (tendsto_inv_atTop_zero.comp (tendsto_exp_div_pow_atTop n)).congr fun x => by rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg] #align real.tendsto_pow_mul_exp_neg_at_top_nhds_0 Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_pow_mul_exp_neg_atTop_nhds_0 := tendsto_pow_mul_exp_neg_atTop_nhds_zero /-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any natural number diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index d9d5b6d4e5f2b..010df1dbae18b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -427,7 +427,7 @@ theorem GammaIntegral_eq_mellin : GammaIntegral = mellin fun x => ↑(Real.exp ( funext fun s => by simp only [mellin, GammaIntegral, smul_eq_mul, mul_comm] #align complex.Gamma_integral_eq_mellin Complex.GammaIntegral_eq_mellin -/-- The derivative of the `Γ` integral, at any `s ∈ ℂ` with `1 < re s`, is given by the Melllin +/-- The derivative of the `Γ` integral, at any `s ∈ ℂ` with `1 < re s`, is given by the Mellin transform of `log t * exp (-t)`. -/ theorem hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) : HasDerivAt GammaIntegral (∫ t : ℝ in Ioi 0, t ^ (s - 1) * (Real.log t * Real.exp (-t))) s := by diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean index 2ed07ba9680c6..903cf561423f9 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean @@ -152,7 +152,7 @@ theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s : ℝ) (b : ℝ) (hb : 0 refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_ filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)] #align tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero -@[deprecated] --2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero nonrec theorem NNReal.tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 3c8a35376f5e8..e4bc99918070d 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -33,19 +33,19 @@ variable {α : Type*} {β : Type*} {ι : Type*} theorem tendsto_inverse_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop #align tendsto_inverse_at_top_nhds_0_nat tendsto_inverse_atTop_nhds_zero_nat -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_inverse_atTop_nhds_0_nat := tendsto_inverse_atTop_nhds_zero_nat theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_zero_nat #align tendsto_const_div_at_top_nhds_0_nat tendsto_const_div_atTop_nhds_zero_nat -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_const_div_atTop_nhds_0_nat := tendsto_const_div_atTop_nhds_zero_nat theorem tendsto_one_div_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ 1/(n : ℝ)) atTop (𝓝 0) := tendsto_const_div_atTop_nhds_zero_nat 1 -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_one_div_atTop_nhds_0_nat := tendsto_one_div_atTop_nhds_zero_nat theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat : @@ -53,14 +53,14 @@ theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat : rw [← NNReal.tendsto_coe] exact _root_.tendsto_inverse_atTop_nhds_zero_nat #align nnreal.tendsto_inverse_at_top_nhds_0_nat NNReal.tendsto_inverse_atTop_nhds_zero_nat -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NNReal.tendsto_inverse_atTop_nhds_0_nat := NNReal.tendsto_inverse_atTop_nhds_zero_nat theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat #align nnreal.tendsto_const_div_at_top_nhds_0_nat NNReal.tendsto_const_div_atTop_nhds_zero_nat -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NNReal.tendsto_const_div_atTop_nhds_0_nat := NNReal.tendsto_const_div_atTop_nhds_zero_nat theorem tendsto_one_div_add_atTop_nhds_zero_nat : @@ -68,7 +68,7 @@ theorem tendsto_one_div_add_atTop_nhds_zero_nat : suffices Tendsto (fun n : ℕ ↦ 1 / (↑(n + 1) : ℝ)) atTop (𝓝 0) by simpa (tendsto_add_atTop_iff_nat 1).2 (_root_.tendsto_const_div_atTop_nhds_zero_nat 1) #align tendsto_one_div_add_at_top_nhds_0_nat tendsto_one_div_add_atTop_nhds_zero_nat -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_one_div_add_atTop_nhds_0_nat := tendsto_one_div_add_atTop_nhds_zero_nat theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜] @@ -77,7 +77,7 @@ theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Se convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp tendsto_inverse_atTop_nhds_zero_nat rw [map_zero] -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat := NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat @@ -85,7 +85,7 @@ theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] : Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) := NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜 -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_algebraMap_inverse_atTop_nhds_0_nat := _root_.tendsto_algebraMap_inverse_atTop_nhds_zero_nat @@ -142,7 +142,7 @@ theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type*} [LinearOrderedField have := one_lt_inv hr h₂ |> tendsto_pow_atTop_atTop_of_one_lt (tendsto_inv_atTop_zero.comp this).congr fun n ↦ by simp) #align tendsto_pow_at_top_nhds_0_of_lt_1 tendsto_pow_atTop_nhds_zero_of_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_pow_atTop_nhds_0_of_lt_1 := tendsto_pow_atTop_nhds_zero_of_lt_one @[simp] theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type*} [LinearOrderedField 𝕜] [Archimedean 𝕜] @@ -170,7 +170,7 @@ theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type*} [LinearOrdere ⟨tendsto_pow_atTop_nhds_zero_of_lt_one h₁.le h₂, tendsto_principal.2 <| eventually_of_forall fun _ ↦ pow_pos h₁ _⟩ #align tendsto_pow_at_top_nhds_within_0_of_lt_1 tendsto_pow_atTop_nhdsWithin_zero_of_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_pow_atTop_nhdsWithin_0_of_lt_1 := tendsto_pow_atTop_nhdsWithin_zero_of_lt_one theorem uniformity_basis_dist_pow_of_lt_one {α : Type*} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) @@ -179,7 +179,7 @@ theorem uniformity_basis_dist_pow_of_lt_one {α : Type*} [PseudoMetricSpace α] Metric.mk_uniformity_basis (fun _ _ ↦ pow_pos h₀ _) fun _ ε0 ↦ (exists_pow_lt_of_lt_one ε0 h₁).imp fun _ hk ↦ ⟨trivial, hk.le⟩ #align uniformity_basis_dist_pow_of_lt_1 uniformity_basis_dist_pow_of_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias uniformity_basis_dist_pow_of_lt_1 := uniformity_basis_dist_pow_of_lt_one theorem geom_lt {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n) @@ -222,7 +222,7 @@ theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) simp only [NNReal.coe_pow, NNReal.coe_zero, _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr] #align nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 := NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[simp] @@ -238,7 +238,7 @@ theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < norm_cast at * apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr #align ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 := ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one @[simp] diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 9485acfc06f1b..fea0a8b8b2355 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -272,14 +272,14 @@ theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type*} [NormedRing R] {x apply squeeze_zero_norm' (eventually_norm_pow_le x) exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h #align tendsto_pow_at_top_nhds_0_of_norm_lt_1 tendsto_pow_atTop_nhds_zero_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_pow_atTop_nhds_0_of_norm_lt_1 := tendsto_pow_atTop_nhds_zero_of_norm_lt_one theorem tendsto_pow_atTop_nhds_zero_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) := tendsto_pow_atTop_nhds_zero_of_norm_lt_one h #align tendsto_pow_at_top_nhds_0_of_abs_lt_1 tendsto_pow_atTop_nhds_zero_of_abs_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tendsto_pow_atTop_nhds_0_of_abs_lt_1 := tendsto_pow_atTop_nhds_zero_of_abs_lt_one /-! ### Geometric series-/ @@ -304,7 +304,7 @@ theorem hasSum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : HasSum (fun n : ℕ theorem summable_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : Summable fun n : ℕ ↦ ξ ^ n := ⟨_, hasSum_geometric_of_norm_lt_one h⟩ #align summable_geometric_of_norm_lt_1 summable_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias summable_geometric_of_norm_lt_1 := summable_geometric_of_norm_lt_one theorem tsum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : ∑' n : ℕ, ξ ^ n = (1 - ξ)⁻¹ := @@ -321,7 +321,7 @@ theorem hasSum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : theorem summable_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Summable fun n : ℕ ↦ r ^ n := summable_geometric_of_norm_lt_one h #align summable_geometric_of_abs_lt_1 summable_geometric_of_abs_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias summable_geometric_of_abs_lt_1 := summable_geometric_of_abs_lt_one theorem tsum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := @@ -340,7 +340,7 @@ theorem summable_geometric_iff_norm_lt_one : (Summable fun n : ℕ ↦ ξ ^ n) rw [← one_pow k] at hk exact lt_of_pow_lt_pow_left _ zero_le_one hk #align summable_geometric_iff_norm_lt_1 summable_geometric_iff_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias summable_geometric_iff_norm_lt_1 := summable_geometric_iff_norm_lt_one end Geometric @@ -353,14 +353,14 @@ theorem summable_norm_pow_mul_geometric_of_norm_lt_one {R : Type*} [NormedRing R exact summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h) (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt _ hrr').isBigO.norm_left #align summable_norm_pow_mul_geometric_of_norm_lt_1 summable_norm_pow_mul_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias summable_norm_pow_mul_geometric_of_norm_lt_1 := summable_norm_pow_mul_geometric_of_norm_lt_one theorem summable_pow_mul_geometric_of_norm_lt_one {R : Type*} [NormedRing R] [CompleteSpace R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable (fun n ↦ (n : R) ^ k * r ^ n : ℕ → R) := .of_norm <| summable_norm_pow_mul_geometric_of_norm_lt_one _ hr #align summable_pow_mul_geometric_of_norm_lt_1 summable_pow_mul_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias summable_pow_mul_geometric_of_norm_lt_1 := summable_pow_mul_geometric_of_norm_lt_one /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version. -/ @@ -390,7 +390,7 @@ theorem hasSum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type*} [NormedDivisionRi simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_mul_eq_div_div_swap] #align has_sum_coe_mul_geometric_of_norm_lt_1 hasSum_coe_mul_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias hasSum_coe_mul_geometric_of_norm_lt_1 := hasSum_coe_mul_geometric_of_norm_lt_one /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`. -/ @@ -398,7 +398,7 @@ theorem tsum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type*} [NormedDivisionRing {r : 𝕜} (hr : ‖r‖ < 1) : (∑' n : ℕ, n * r ^ n : 𝕜) = r / (1 - r) ^ 2 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).tsum_eq #align tsum_coe_mul_geometric_of_norm_lt_1 tsum_coe_mul_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias tsum_coe_mul_geometric_of_norm_lt_1 := tsum_coe_mul_geometric_of_norm_lt_one end MulGeometric @@ -501,7 +501,7 @@ theorem NormedRing.summable_geometric_of_norm_lt_one (x : R) (h : ‖x‖ < 1) : have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) h h1.of_norm_bounded_eventually_nat _ (eventually_norm_pow_le x) #align normed_ring.summable_geometric_of_norm_lt_1 NormedRing.summable_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NormedRing.summable_geometric_of_norm_lt_1 := NormedRing.summable_geometric_of_norm_lt_one /-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the @@ -517,7 +517,7 @@ theorem NormedRing.tsum_geometric_of_norm_lt_one (x : R) (h : ‖x‖ < 1) : simp linarith #align normed_ring.tsum_geometric_of_norm_lt_1 NormedRing.tsum_geometric_of_norm_lt_one -@[deprecated] -- 2024-01-31 +@[deprecated (since := "2024-01-31")] alias NormedRing.tsum_geometric_of_norm_lt_1 := NormedRing.tsum_geometric_of_norm_lt_one theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1 := by diff --git a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean index 52bece8de302f..9285590718aaf 100644 --- a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean +++ b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean @@ -322,7 +322,7 @@ lemma ofCocomplex_d_0_1 : (ofCocomplex Z).d 0 1 = d (Injective.ι Z) := by simp [ofCocomplex] -#adaptation_note /-- Since nightly-2024-03-11, this takes takes forever now -/ +#adaptation_note /-- Since nightly-2024-03-11, this takes forever now -/ lemma ofCocomplex_exactAt_succ (n : ℕ) : (ofCocomplex Z).ExactAt (n + 1) := by rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)] diff --git a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean index 96b5df2a9020c..04bc52f65fe78 100644 --- a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean @@ -63,7 +63,7 @@ def closedCounit (F : D ⥤ C) : closedIhom F ⋙ tensorLeft F ⟶ 𝟭 (D ⥤ C /-- If `C` is a monoidal closed category and `D` is a groupoid, then every functor `F : D ⥤ C` is closed in the functor category `F : D ⥤ C` with the pointwise monoidal structure. -/ -- Porting note: removed `@[simps]`, as some of the generated lemmas were failing the simpNF linter, --- and none of the generated lemmmas was actually used in mathlib3. +-- and none of the generated lemmas was actually used in mathlib3. instance closed (F : D ⥤ C) : Closed F where rightAdj := closedIhom F adj := diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean index 87b652609fa69..8798e24eea101 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean @@ -1,5 +1,5 @@ /- -Copyright (c) Markus Himmel. All rights reserved. +Copyright (c) 2022 Markus Himmel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index 39e426cc38c6f..a172313e0cf2e 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -61,8 +61,16 @@ def comp (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) : functor := Φ.functor ⋙ Ψ.functor map _ _ _ hf := Ψ.map _ (Φ.map _ hf) -variable (Φ : LocalizerMorphism W₁ W₂) (L₁ : C₁ ⥤ D₁) [L₁.IsLocalization W₁] - (L₂ : C₂ ⥤ D₂) [L₂.IsLocalization W₂] +variable (Φ : LocalizerMorphism W₁ W₂) + +/-- The opposite localizer morphism `LocalizerMorphism W₁.op W₂.op` deduced +from `Φ : LocalizerMorphism W₁ W₂`. -/ +@[simps] +def op : LocalizerMorphism W₁.op W₂.op where + functor := Φ.functor.op + map _ _ _ hf := Φ.map _ hf + +variable (L₁ : C₁ ⥤ D₁) [L₁.IsLocalization W₁] (L₂ : C₂ ⥤ D₂) [L₂.IsLocalization W₂] lemma inverts : W₁.IsInvertedBy (Φ.functor ⋙ L₂) := fun _ _ _ hf => Localization.inverts L₂ W₂ _ (Φ.map _ hf) diff --git a/Mathlib/CategoryTheory/Localization/Resolution.lean b/Mathlib/CategoryTheory/Localization/Resolution.lean index b449230196563..fce7904a80544 100644 --- a/Mathlib/CategoryTheory/Localization/Resolution.lean +++ b/Mathlib/CategoryTheory/Localization/Resolution.lean @@ -19,6 +19,8 @@ A right resolution consists of an object `X₁ : C₁` and a morphism The type of right resolutions `Φ.RightResolution X₂` is endowed with a category structure when the morphism property `W₁` is multiplicative. +Similiar definitions are done from left resolutions. + ## Future works * formalize right derivability structures as localizer morphisms admitting right resolutions @@ -47,7 +49,8 @@ namespace LocalizerMorphism variable (Φ : LocalizerMorphism W₁ W₂) -/-- The category of resolutions of an object in the target category of a localizer morphism. -/ +/-- The category of right resolutions of an object in the target category +of a localizer morphism. -/ structure RightResolution (X₂ : C₂) where /-- an object in the source category -/ {X₁ : C₁} @@ -55,14 +58,31 @@ structure RightResolution (X₂ : C₂) where w : X₂ ⟶ Φ.functor.obj X₁ hw : W₂ w +/-- The category of left resolutions of an object in the target category +of a localizer morphism. -/ +structure LeftResolution (X₂ : C₂) where + /-- an object in the source category -/ + {X₁ : C₁} + /-- a morphism from an object of the form `Φ.functor.obj X₁` -/ + w : Φ.functor.obj X₁ ⟶ X₂ + hw : W₂ w + variable {Φ X₂} in lemma RightResolution.mk_surjective (R : Φ.RightResolution X₂) : ∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w), R = RightResolution.mk w hw := ⟨_, R.w, R.hw, rfl⟩ +variable {Φ X₂} in +lemma LeftResolution.mk_surjective (L : Φ.LeftResolution X₂) : + ∃ (X₁ : C₁) (w : Φ.functor.obj X₁ ⟶ X₂) (hw : W₂ w), L = LeftResolution.mk w hw := + ⟨_, L.w, L.hw, rfl⟩ + /-- A localizer morphism has right resolutions when any object has a right resolution. -/ abbrev HasRightResolutions := ∀ (X₂ : C₂), Nonempty (Φ.RightResolution X₂) +/-- A localizer morphism has right resolutions when any object has a right resolution. -/ +abbrev HasLeftResolutions := ∀ (X₂ : C₂), Nonempty (Φ.LeftResolution X₂) + namespace RightResolution variable {Φ} {X₂ : C₂} @@ -112,17 +132,156 @@ lemma hom_ext {R R' : Φ.RightResolution X₂} {φ₁ φ₂ : R ⟶ R'} (h : φ end RightResolution +namespace LeftResolution + +variable {Φ} {X₂ : C₂} + +/-- The type of morphisms in the category `Φ.LeftResolution X₂` (when `W₁` is multiplicative). -/ +@[ext] +structure Hom (L L' : Φ.LeftResolution X₂) where + /-- a morphism in the source category -/ + f : L.X₁ ⟶ L'.X₁ + hf : W₁ f + comm : Φ.functor.map f ≫ L'.w = L.w := by aesop_cat + +attribute [reassoc (attr := simp)] Hom.comm + +/-- The identity of a object in `Φ.LeftResolution X₂`. -/ +@[simps] +def Hom.id [W₁.ContainsIdentities] (L : Φ.LeftResolution X₂) : Hom L L where + f := 𝟙 _ + hf := W₁.id_mem _ + +variable [W₁.IsMultiplicative] + +/-- The composition of morphisms in `Φ.LeftResolution X₂`. -/ +@[simps] +def Hom.comp {L L' L'' : Φ.LeftResolution X₂} + (φ : Hom L L') (ψ : Hom L' L'') : + Hom L L'' where + f := φ.f ≫ ψ.f + hf := W₁.comp_mem _ _ φ.hf ψ.hf + +instance : Category (Φ.LeftResolution X₂) where + Hom := Hom + id := Hom.id + comp := Hom.comp + +@[simp] +lemma id_f (L : Φ.LeftResolution X₂) : Hom.f (𝟙 L) = 𝟙 L.X₁ := rfl + +@[simp, reassoc] +lemma comp_f {L L' L'' : Φ.LeftResolution X₂} (φ : L ⟶ L') (ψ : L' ⟶ L'') : + (φ ≫ ψ).f = φ.f ≫ ψ.f := rfl + +@[ext] +lemma hom_ext {L L' : Φ.LeftResolution X₂} {φ₁ φ₂ : L ⟶ L'} (h : φ₁.f = φ₂.f) : + φ₁ = φ₂ := + Hom.ext _ _ h + +end LeftResolution + +variable {Φ} + +/-- The canonical map `Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂)`. -/ +@[simps] +def LeftResolution.op {X₂ : C₂} (L : Φ.LeftResolution X₂) : + Φ.op.RightResolution (Opposite.op X₂) where + X₁ := Opposite.op L.X₁ + w := L.w.op + hw := L.hw + +/-- The canonical map `Φ.op.LeftResolution X₂ → Φ.RightResolution X₂`. -/ +@[simps] +def LeftResolution.unop {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) : + Φ.RightResolution X₂.unop where + X₁ := Opposite.unop L.X₁ + w := L.w.unop + hw := L.hw + +/-- The canonical map `Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂)`. -/ +@[simps] +def RightResolution.op {X₂ : C₂} (L : Φ.RightResolution X₂) : + Φ.op.LeftResolution (Opposite.op X₂) where + X₁ := Opposite.op L.X₁ + w := L.w.op + hw := L.hw + +/-- The canonical map `Φ.op.RightResolution X₂ → Φ.LeftResolution X₂`. -/ +@[simps] +def RightResolution.unop {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) : + Φ.LeftResolution X₂.unop where + X₁ := Opposite.unop L.X₁ + w := L.w.unop + hw := L.hw + +variable (Φ) + +lemma nonempty_leftResolution_iff_op (X₂ : C₂) : + Nonempty (Φ.LeftResolution X₂) ↔ Nonempty (Φ.op.RightResolution (Opposite.op X₂)) := + Equiv.nonempty_congr + { toFun := fun L => L.op + invFun := fun R => R.unop + left_inv := fun _ => rfl + right_inv := fun _ => rfl } + +lemma nonempty_rightResolution_iff_op (X₂ : C₂) : + Nonempty (Φ.RightResolution X₂) ↔ Nonempty (Φ.op.LeftResolution (Opposite.op X₂)) := + Equiv.nonempty_congr + { toFun := fun R => R.op + invFun := fun L => L.unop + left_inv := fun _ => rfl + right_inv := fun _ => rfl } + +lemma hasLeftResolutions_iff_op : Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions := + ⟨fun _ X₂ => ⟨(Classical.arbitrary (Φ.LeftResolution X₂.unop)).op⟩, + fun _ X₂ => ⟨(Classical.arbitrary (Φ.op.RightResolution (Opposite.op X₂))).unop⟩⟩ + +lemma hasRightResolutions_iff_op : Φ.HasRightResolutions ↔ Φ.op.HasLeftResolutions := + ⟨fun _ X₂ => ⟨(Classical.arbitrary (Φ.RightResolution X₂.unop)).op⟩, + fun _ X₂ => ⟨(Classical.arbitrary (Φ.op.LeftResolution (Opposite.op X₂))).unop⟩⟩ + +/-- The functor `(Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂)`. -/ +@[simps] +def LeftResolution.opFunctor (X₂ : C₂) [W₁.IsMultiplicative] : + (Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂) where + obj L := L.unop.op + map φ := + { f := φ.unop.f.op + hf := φ.unop.hf + comm := Quiver.Hom.unop_inj φ.unop.comm } + +/-- The functor `(Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop`. -/ +@[simps] +def RightResolution.unopFunctor (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] : + (Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop where + obj R := R.unop.unop + map φ := + { f := φ.unop.f.unop + hf := φ.unop.hf + comm := Quiver.Hom.op_inj φ.unop.comm } + +/-- The equivalence of categories +`(Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)`. -/ +@[simps] +def LeftResolution.opEquivalence (X₂ : C₂) [W₁.IsMultiplicative] : + (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂) where + functor := LeftResolution.opFunctor Φ X₂ + inverse := (RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp + unitIso := Iso.refl _ + counitIso := Iso.refl _ + section -variable [Φ.HasRightResolutions] (L₂ : C₂ ⥤ D₂) [L₂.IsLocalization W₂] +variable (L₂ : C₂ ⥤ D₂) [L₂.IsLocalization W₂] -lemma essSurj_of_hasRightResolutions : (Φ.functor ⋙ L₂).EssSurj where +lemma essSurj_of_hasRightResolutions [Φ.HasRightResolutions] : (Φ.functor ⋙ L₂).EssSurj where mem_essImage X₂ := by have := Localization.essSurj L₂ W₂ have R : Φ.RightResolution (L₂.objPreimage X₂) := Classical.arbitrary _ exact ⟨R.X₁, ⟨(Localization.isoOfHom L₂ W₂ _ R.hw).symm ≪≫ L₂.objObjPreimageIso X₂⟩⟩ -lemma isIso_iff_of_hasRightResolutions {F G : D₂ ⥤ H} (α : F ⟶ G) : +lemma isIso_iff_of_hasRightResolutions [Φ.HasRightResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) : IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁))) := by constructor · intros @@ -134,6 +293,24 @@ lemma isIso_iff_of_hasRightResolutions {F G : D₂ ⥤ H} (α : F ⟶ G) : apply hα exact NatIso.isIso_of_isIso_app α +lemma essSurj_of_hasLeftResolutions [Φ.HasLeftResolutions] : (Φ.functor ⋙ L₂).EssSurj where + mem_essImage X₂ := by + have := Localization.essSurj L₂ W₂ + have L : Φ.LeftResolution (L₂.objPreimage X₂) := Classical.arbitrary _ + exact ⟨L.X₁, ⟨Localization.isoOfHom L₂ W₂ _ L.hw ≪≫ L₂.objObjPreimageIso X₂⟩⟩ + +lemma isIso_iff_of_hasLeftResolutions [Φ.HasLeftResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) : + IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁))) := by + constructor + · intros + infer_instance + · intro hα + have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ => by + have := Φ.essSurj_of_hasLeftResolutions L₂ + rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)] + apply hα + exact NatIso.isIso_of_isIso_app α + end end LocalizerMorphism diff --git a/Mathlib/Combinatorics/Additive/Energy.lean b/Mathlib/Combinatorics/Additive/Energy.lean index 7d0ad4dc109ac..27326f7e2059b 100644 --- a/Mathlib/Combinatorics/Additive/Energy.lean +++ b/Mathlib/Combinatorics/Additive/Energy.lean @@ -134,9 +134,8 @@ variable {s t} #align finset.additive_energy_eq_zero_iff Finset.addEnergy_eq_zero_iff @[to_additive] lemma mulEnergy_eq_card_filter (s t : Finset α) : - Eₘ[s, t] = (((s ×ˢ t) ×ˢ s ×ˢ t).filter fun ((a, b), c, d) ↦ a * b = c * d).card := by - refine Finset.card_congr (fun ((a, b), c, d) _ ↦ ((a, c), b, d)) (by aesop) (by aesop) - fun ((a, b), c, d) h ↦ ⟨((a, c), b, d), by simpa [and_and_and_comm] using h⟩ + Eₘ[s, t] = (((s ×ˢ t) ×ˢ s ×ˢ t).filter fun ((a, b), c, d) ↦ a * b = c * d).card := + card_equiv (.prodProdProdComm _ _ _ _) (by simp [and_and_and_comm]) @[to_additive] lemma mulEnergy_eq_sum_sq' (s t : Finset α) : Eₘ[s, t] = ∑ a in s * t, ((s ×ˢ t).filter fun (x, y) ↦ x * y = a).card ^ 2 := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index cb51b99272064..ef66fc148c130 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean @@ -166,15 +166,15 @@ lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) : rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos] rw [← this, add_left_inj] choose f hf hf' using (hG.existsUnique_path · default) - refine Eq.symm <| Finset.card_congr + refine Eq.symm <| Finset.card_bij (fun w hw => ((f w).firstDart <| ?notNil).edge) (fun a ha => ?memEdges) ?inj ?surj case notNil => exact not_nil_of_ne (by simpa using hw) case memEdges => simp case inj => - intros a b ha hb h + intros a ha b hb h wlog h' : (f a).length ≤ (f b).length generalizing a b - · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h')) + · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_le h')) rw [dart_edge_eq_iff] at h obtain (h | h) := h · exact (congrArg (·.fst) h) diff --git a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean index cc554235bd650..efed30a6a774a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean +++ b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean @@ -118,8 +118,8 @@ theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * G.edgeFinset.c lemma two_mul_card_edgeFinset : 2 * G.edgeFinset.card = (univ.filter fun (x, y) ↦ G.Adj x y).card := by rw [← dart_card_eq_twice_card_edges, ← card_univ] - refine card_congr (fun d _ ↦ (d.fst, d.snd)) (by simp) (by simp [Dart.ext_iff, ← and_imp]) ?_ - exact fun xy h ↦ ⟨⟨xy, (mem_filter.1 h).2⟩, mem_univ _, Prod.mk.eta⟩ + refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_ + <;> simp end DegreeSum diff --git a/Mathlib/Combinatorics/SimpleGraph/Density.lean b/Mathlib/Combinatorics/SimpleGraph/Density.lean index 03d82490609bd..f80b53f8ab5a3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Density.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Density.lean @@ -281,7 +281,7 @@ theorem mk_mem_interedges_comm : (a, b) ∈ interedges r s t ↔ (b, a) ∈ inte #align rel.mk_mem_interedges_comm Rel.mk_mem_interedges_comm theorem card_interedges_comm (s t : Finset α) : (interedges r s t).card = (interedges r t s).card := - Finset.card_congr (fun (x : α × α) _ ↦ x.swap) (fun _ ↦ (swap_mem_interedges_iff hr).2) + Finset.card_bij (fun (x : α × α) _ ↦ x.swap) (fun _ ↦ (swap_mem_interedges_iff hr).2) (fun _ _ _ _ h ↦ Prod.swap_injective h) fun x h ↦ ⟨x.swap, (swap_mem_interedges_iff hr).2 h, x.swap_swap⟩ #align rel.card_interedges_comm Rel.card_interedges_comm diff --git a/Mathlib/Data/Finmap.lean b/Mathlib/Data/Finmap.lean index 101b9a391c8f9..54c6a085e24de 100644 --- a/Mathlib/Data/Finmap.lean +++ b/Mathlib/Data/Finmap.lean @@ -398,7 +398,6 @@ def any (f : ∀ x, β x → Bool) (s : Finmap β) : Bool := (fun _ _ _ _ => by simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]) false #align finmap.any Finmap.any --- TODO: should this really return `false` if `s` is empty? /-- `all f s` returns `true` iff `f v = true` for all values `v` in `s`. -/ def all (f : ∀ x, β x → Bool) (s : Finmap β) : Bool := s.foldl (fun x y z => x && f y z) diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index c7143585bc7ae..2548e15c595e8 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -355,23 +355,88 @@ theorem card_eq_of_bijective (f : ∀ i, i < n → α) (hf : ∀ a ∈ s, ∃ i, exact Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq #align finset.card_eq_of_bijective Finset.card_eq_of_bijective -theorem card_congr {t : Finset β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha ∈ t) - (h₂ : ∀ a b ha hb, f a ha = f b hb → a = b) (h₃ : ∀ b ∈ t, ∃ a ha, f a ha = b) : - s.card = t.card := by +section bij +variable {t : Finset β} + +/-- Reorder a finset. + +The difference with `Finset.card_bij'` is that the bijection is specified as a surjective injection, +rather than by an inverse function. + +The difference with `Finset.card_nbij` is that the bijection is allowed to use membership of the +domain, rather than being a non-dependent function. -/ +lemma card_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) + (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) + (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : s.card = t.card := by classical calc s.card = s.attach.card := card_attach.symm - _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card := Eq.symm ?_ + _ = (s.attach.image fun a : { a // a ∈ s } => i a.1 a.2).card := Eq.symm ?_ _ = t.card := ?_ · apply card_image_of_injective intro ⟨_, _⟩ ⟨_, _⟩ h - simpa using h₂ _ _ _ _ h + simpa using i_inj _ _ _ _ h · congr 1 ext b - constructor - · intro h; obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply h₁ - · intro h; obtain ⟨a, ha, rfl⟩ := h₃ b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩ -#align finset.card_congr Finset.card_congr + constructor <;> intro h + · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi + · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩ +#align finset.card_bij Finset.card_bij + +@[deprecated (since := "2024-05-04")] alias card_congr := card_bij + +/-- Reorder a finset. + +The difference with `Finset.card_bij` is that the bijection is specified with an inverse, rather +than as a surjective injection. + +The difference with `Finset.card_nbij'` is that the bijection and its inverse are allowed to use +membership of the domains, rather than being non-dependent functions. -/ +lemma card_bij' (i : ∀ a ∈ s, β) (j : ∀ a ∈ t, α) (hi : ∀ a ha, i a ha ∈ t) + (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) + (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) : s.card = t.card := by + refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) + rw [← left_inv a1 h1, ← left_inv a2 h2] + simp only [eq] + +/-- Reorder a finset. + +The difference with `Finset.card_nbij'` is that the bijection is specified as a surjective +injection, rather than by an inverse function. + +The difference with `Finset.card_bij` is that the bijection is a non-dependent function, rather than +being allowed to use membership of the domain. -/ +lemma card_nbij (i : α → β) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set α).InjOn i) + (i_surj : (s : Set α).SurjOn i t) : s.card = t.card := + card_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj) + +/-- Reorder a finset. + +The difference with `Finset.card_nbij` is that the bijection is specified with an inverse, rather +than as a surjective injection. + +The difference with `Finset.card_bij'` is that the bijection and its inverse are non-dependent +functions, rather than being allowed to use membership of the domains. + +The difference with `Finset.card_equiv` is that bijectivity is only required to hold on the domains, +rather than on the entire types. -/ +lemma card_nbij' (i : α → β) (j : β → α) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) + (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) : s.card = t.card := + card_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv + +/-- Specialization of `Finset.card_nbij'` that automatically fills in most arguments. + +See `Fintype.card_equiv` for the version where `s` and `t` are `univ`. -/ +lemma card_equiv (e : α ≃ β) (hst : ∀ i, i ∈ s ↔ e i ∈ t) : s.card = t.card := by + refine card_nbij' e e.symm ?_ ?_ ?_ ?_ <;> simp [hst] + +/-- Specialization of `Finset.card_nbij` that automatically fills in most arguments. + +See `Fintype.card_bijective` for the version where `s` and `t` are `univ`. -/ +lemma card_bijective (e : α → β) (he : e.Bijective) (hst : ∀ i, i ∈ s ↔ e i ∈ t) : + s.card = t.card := card_equiv (.ofBijective e he) hst + +end bij theorem card_le_card_of_inj_on {t : Finset β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : ∀ a₁ ∈ s, ∀ a₂ ∈ s, f a₁ = f a₂ → a₁ = a₂) : s.card ≤ t.card := by diff --git a/Mathlib/Data/Fintype/Quotient.lean b/Mathlib/Data/Fintype/Quotient.lean index 10fdd1ee9a80e..739d938ec813d 100644 --- a/Mathlib/Data/Fintype/Quotient.lean +++ b/Mathlib/Data/Fintype/Quotient.lean @@ -84,3 +84,14 @@ theorem Quotient.finChoice_eq {ι : Type*} [DecidableEq ι] [Fintype ι] {α : exact Quotient.inductionOn (@Finset.univ ι _).1 fun l => Quotient.finChoiceAux_eq _ _ rfl #align quotient.fin_choice_eq Quotient.finChoice_eq + +/-- Given a function that for each `i : ι` gives a term of the corresponding +truncation type, then there is corresponding term in the truncation of the product. -/ +def Trunc.finChoice {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*} + (f : ∀ i, Trunc (α i)) : Trunc (∀ i, α i) := + Quotient.map' id (fun _ _ _ => trivial) + (Quotient.finChoice f (S := fun _ => trueSetoid)) + +theorem Trunc.finChoice_eq {ι : Type*} [DecidableEq ι] [Fintype ι] {α : ι → Type*} + (f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f := + Subsingleton.elim _ _ diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index ebde1145605d6..67d71cb4aebec 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -68,7 +68,7 @@ def lnot : ℤ → ℤ | -[m +1] => m #align int.lnot Int.lnot -/--`lor` takes two integers and returns their bitwise `or`-/ +/-- `lor` takes two integers and returns their bitwise `or`-/ def lor : ℤ → ℤ → ℤ | (m : ℕ), (n : ℕ) => m ||| n | (m : ℕ), -[n +1] => -[Nat.ldiff n m +1] @@ -76,7 +76,7 @@ def lor : ℤ → ℤ → ℤ | -[m +1], -[n +1] => -[m &&& n +1] #align int.lor Int.lor -/--`land` takes two integers and returns their bitwise `and`-/ +/-- `land` takes two integers and returns their bitwise `and`-/ def land : ℤ → ℤ → ℤ | (m : ℕ), (n : ℕ) => m &&& n | (m : ℕ), -[n +1] => Nat.ldiff m n @@ -85,7 +85,7 @@ def land : ℤ → ℤ → ℤ #align int.land Int.land -- Porting note: I don't know why `Nat.ldiff` got the prime, but I'm matching this change here -/--`ldiff a b` performs bitwise set difference. For each corresponding +/-- `ldiff a b` performs bitwise set difference. For each corresponding pair of bits taken as booleans, say `aᵢ` and `bᵢ`, it applies the boolean operation `aᵢ ∧ bᵢ` to obtain the `iᵗʰ` bit of the result. -/ def ldiff : ℤ → ℤ → ℤ @@ -96,7 +96,7 @@ def ldiff : ℤ → ℤ → ℤ #align int.ldiff Int.ldiff -- Porting note: I don't know why `Nat.xor'` got the prime, but I'm matching this change here -/--`xor` computes the bitwise `xor` of two natural numbers-/ +/-- `xor` computes the bitwise `xor` of two natural numbers-/ protected def xor : ℤ → ℤ → ℤ | (m : ℕ), (n : ℕ) => (m ^^^ n) | (m : ℕ), -[n +1] => -[(m ^^^ n) +1] diff --git a/Mathlib/Data/Int/Defs.lean b/Mathlib/Data/Int/Defs.lean index c84a872510381..3388e68ac7389 100644 --- a/Mathlib/Data/Int/Defs.lean +++ b/Mathlib/Data/Int/Defs.lean @@ -85,6 +85,8 @@ protected lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a := ⟨Int.le_of_sub_nonneg, instance instNontrivial : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩ +@[simp] lemma ofNat_injective : Function.Injective ofNat := @Int.ofNat.inj + @[simp] lemma ofNat_eq_natCast (n : ℕ) : Int.ofNat n = n := rfl @[deprecated ofNat_eq_natCast] -- 2024-03-24 diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean index fb15d21f11073..77a473843e93e 100644 --- a/Mathlib/Data/List/Defs.lean +++ b/Mathlib/Data/List/Defs.lean @@ -549,4 +549,31 @@ def replaceIf : List α → List Bool → List α → List α #align list.map_with_prefix_suffix List.mapWithPrefixSuffix #align list.map_with_complement List.mapWithComplement +/-- `iterate f a n` is `[a, f a, ..., f^[n - 1] a]`. -/ +@[simp] +def iterate (f : α → α) (a : α) : (n : ℕ) → List α + | 0 => [] + | n + 1 => a :: iterate f (f a) n + +/-- Tail-recursive version of `List.iterate`. -/ +@[inline] +def iterateTR (f : α → α) (a : α) (n : ℕ) : List α := + loop a n [] +where + /-- `iterateTR.loop f a n l := iterate f a n ++ reverse l`. -/ + @[simp, specialize] + loop (a : α) (n : ℕ) (l : List α) : List α := + match n with + | 0 => reverse l + | n + 1 => loop (f a) n (a :: l) + +theorem iterateTR_loop_eq (f : α → α) (a : α) (n : ℕ) (l : List α) : + iterateTR.loop f a n l = reverse l ++ iterate f a n := by + induction n generalizing a l <;> simp [*] + +@[csimp] +theorem iterate_eq_iterateTR : @iterate = @iterateTR := by + funext α f a n + exact Eq.symm <| iterateTR_loop_eq f a n [] + end List diff --git a/Mathlib/Data/List/Iterate.lean b/Mathlib/Data/List/Iterate.lean new file mode 100644 index 0000000000000..5589f2078ae92 --- /dev/null +++ b/Mathlib/Data/List/Iterate.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2024 Miyahara Kō. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Miyahara Kō +-/ + +import Mathlib.Data.List.Defs +import Mathlib.Algebra.Order.Ring.Nat + +/-! +# iterate + +Proves various lemmas about `List.iterate`. +-/ + +variable {α : Type*} + +namespace List + +@[simp] +theorem length_iterate (f : α → α) (a : α) (n : ℕ) : length (iterate f a n) = n := by + induction n generalizing a <;> simp [*] + +@[simp] +theorem iterate_eq_nil {f : α → α} {a : α} {n : ℕ} : iterate f a n = [] ↔ n = 0 := by + rw [← length_eq_zero, length_iterate] + +theorem get?_iterate (f : α → α) (a : α) : + ∀ (n i : ℕ), i < n → get? (iterate f a n) i = f^[i] a + | n + 1, 0 , _ => rfl + | n + 1, i + 1, h => by simp [get?_iterate f (f a) n i (by simpa using h)] + +@[simp] +theorem get_iterate (f : α → α) (a : α) (n : ℕ) (i : Fin (iterate f a n).length) : + get (iterate f a n) i = f^[↑i] a := + (get?_eq_some.1 <| get?_iterate f a n i.1 (by simpa using i.2)).2 + +@[simp] +theorem mem_iterate {f : α → α} {a : α} {n : ℕ} {b : α} : + b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a := by + simp [List.mem_iff_get, Fin.exists_iff, eq_comm (b := b)] + +@[simp] +theorem range_map_iterate (n : ℕ) (f : α → α) (a : α) : + (List.range n).map (f^[·] a) = List.iterate f a n := by + apply List.ext_get <;> simp + +end List diff --git a/Mathlib/Data/MLList/BestFirst.lean b/Mathlib/Data/MLList/BestFirst.lean index 8ec003793df80..a07dac9f6b575 100644 --- a/Mathlib/Data/MLList/BestFirst.lean +++ b/Mathlib/Data/MLList/BestFirst.lean @@ -94,7 +94,7 @@ variable {α : Type} {prio : α → Thunk ω} {ε : α → Type} [LinearOrder ω [I : ∀ a : α, WellFoundedGT (range (bound (prio a) : ε a → ω))] {m : Type → Type} [Monad m] {β : Type} -/-- Calculate the current best lower bound for the the priority of a node. -/ +/-- Calculate the current best lower bound for the priority of a node. -/ def BestFirstNode.estimate (n : BestFirstNode prio ε) : ω := bound (prio n.key) n.estimator instance [Ord ω] [Ord α] : Ord (BestFirstNode prio ε) where diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean index 5f366a1f0d118..0ddd97abd6cf2 100644 --- a/Mathlib/Data/Nat/Bits.lean +++ b/Mathlib/Data/Nat/Bits.lean @@ -168,7 +168,7 @@ lemma bit_zero : bit false 0 = 0 := rfl #align nat.bit_zero Nat.bit_zero -/--`shiftLeft' b m n` performs a left shift of `m` `n` times +/-- `shiftLeft' b m n` performs a left shift of `m` `n` times and adds the bit `b` as the least significant bit each time. Returns the corresponding natural number-/ def shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ @@ -233,7 +233,7 @@ def bits : ℕ → List Bool := #align nat.land Nat.land #align nat.lxor Nat.xor -/--`ldiff a b` performs bitwise set difference. For each corresponding +/-- `ldiff a b` performs bitwise set difference. For each corresponding pair of bits taken as booleans, say `aᵢ` and `bᵢ`, it applies the boolean operation `aᵢ ∧ ¬bᵢ` to obtain the `iᵗʰ` bit of the result. -/ def ldiff : ℕ → ℕ → ℕ := diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index ea84a1c6c0fb5..595f9e5a71b37 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -667,7 +667,7 @@ so if one of `a` or `b` is `0` then the result is `1`. Note that `factorizationLCMRight a b` is *not* `factorizationLCMLeft b a`: the difference is that in `factorizationLCMLeft a b` there are the primes whose exponent in `a` is bigger or equal -than the exponent in `b`, while in `factorizationLCMRight a b` there are the primes primes whose +than the exponent in `b`, while in `factorizationLCMRight a b` there are the primes whose exponent in `b` is strictly bigger than in `a`. For example `factorizationLCMLeft 2 2 = 2`, but `factorizationLCMRight 2 2 = 1`. -/ def factorizationLCMRight (a b : ℕ) := diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index ef2bd00d7999f..e6c2b23e3f449 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -156,7 +156,7 @@ theorem totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) : rcases d.eq_zero_or_pos with (rfl | hd0); · simp [eq_zero_of_zero_dvd hnd] rcases hnd with ⟨x, rfl⟩ rw [Nat.mul_div_cancel_left x hd0] - apply Finset.card_congr fun k _ => d * k + apply Finset.card_bij fun k _ => d * k · simp only [mem_filter, mem_range, and_imp, Coprime] refine fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, ?_⟩ rw [gcd_mul_left, ha2, mul_one] diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean index 11698fc20033f..6626eda334d57 100644 --- a/Mathlib/Data/Option/Basic.lean +++ b/Mathlib/Data/Option/Basic.lean @@ -105,6 +105,15 @@ theorem bind_eq_some' {x : Option α} {f : α → Option β} {b : β} : #align option.bind_eq_none' Option.bind_eq_none' +theorem bind_congr {f g : α → Option β} {x : Option α} + (h : ∀ a ∈ x, f a = g a) : x.bind f = x.bind g := by + cases x <;> simp only [some_bind, none_bind, mem_def, h] + +@[congr] +theorem bind_congr' {f g : α → Option β} {x y : Option α} (hx : x = y) + (hf : ∀ a ∈ y, f a = g a) : x.bind f = y.bind g := + hx.symm ▸ bind_congr hf + theorem joinM_eq_join : joinM = @join α := funext fun _ ↦ rfl #align option.join_eq_join Option.joinM_eq_join diff --git a/Mathlib/Data/Rel.lean b/Mathlib/Data/Rel.lean index 575eaabe27bea..b9a9406d5bd37 100644 --- a/Mathlib/Data/Rel.lean +++ b/Mathlib/Data/Rel.lean @@ -31,6 +31,13 @@ Relations are also known as set-valued functions, or partial multifunctions. related to `x` are in `s`. * `Rel.restrict_domain`: Domain-restriction of a relation to a subtype. * `Function.graph`: Graph of a function as a relation. + +## TODOs + +The `Rel.comp` function uses the notation `r • s`, rather than the more common `r ∘ s` for things +named `comp`. This is because the latter is already used for function composition, and causes a +clash. A better notation should be found, perhaps a variant of `r ∘r s` or `r; s`. + -/ variable {α β γ : Type*} @@ -91,7 +98,6 @@ def comp (r : Rel α β) (s : Rel β γ) : Rel α γ := fun x z => ∃ y, r x y #align rel.comp Rel.comp -- Porting note: the original `∘` syntax can't be overloaded here, lean considers it ambiguous. --- TODO: Change this syntax to something nicer? /-- Local syntax for composition of relations. -/ local infixr:90 " • " => Rel.comp @@ -407,10 +413,8 @@ theorem Relation.is_graph_iff (r : Rel α β) : (∃! f, Function.graph f = r) namespace Set --- TODO: if image were defined with bounded quantification in corelib, the next two would --- be definitional theorem image_eq (f : α → β) (s : Set α) : f '' s = (Function.graph f).image s := by - simp [Set.image, Rel.image] + rfl #align set.image_eq Set.image_eq theorem preimage_eq (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s := by diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 8753d3e9d154c..8f6aed4b5d7f6 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -524,7 +524,7 @@ theorem nonempty_of_nonempty_subtype [Nonempty (↥s)] : s.Nonempty := /-! ### Lemmas about the empty set -/ -theorem empty_def : (↥(∅ : Set α)) = { _x : α | False } := +theorem empty_def : (∅ : Set α) = { _x : α | False } := rfl #align set.empty_def Set.empty_def diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean index 5c65fda629235..00e1bae016672 100644 --- a/Mathlib/Data/Setoid/Basic.lean +++ b/Mathlib/Data/Setoid/Basic.lean @@ -196,6 +196,25 @@ theorem eq_top_iff {s : Setoid α} : s = (⊤ : Setoid α) ↔ ∀ x y : α, s.R simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left] #align setoid.eq_top_iff Setoid.eq_top_iff +lemma sInf_equiv {S : Set (Setoid α)} {x y : α} : + letI := sInf S + x ≈ y ↔ ∀ s ∈ S, s.Rel x y := Iff.rfl + +lemma quotient_mk_sInf_eq {S : Set (Setoid α)} {x y : α} : + Quotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s.Rel x y := by + simp + rfl + +/-- The map induced between quotients by a setoid inequality. -/ +def map_of_le {s t : Setoid α} (h : s ≤ t) : Quotient s → Quotient t := + Quotient.map' id h + +/-- The map from the quotient of the infimum of a set of setoids into the quotient +by an element of this set. -/ +def map_sInf {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : + Quotient (sInf S) → Quotient s := + Setoid.map_of_le fun _ _ a ↦ a s h + /-- The inductively defined equivalence closure of a binary relation r is the infimum of the set of all equivalence relations containing r. -/ theorem eqvGen_eq (r : α → α → Prop) : diff --git a/Mathlib/Data/Sym/Card.lean b/Mathlib/Data/Sym/Card.lean index 922a1c3a91a56..64d37c73ae06b 100644 --- a/Mathlib/Data/Sym/Card.lean +++ b/Mathlib/Data/Sym/Card.lean @@ -110,7 +110,9 @@ theorem card_sym_fin_eq_multichoose : ∀ n k : ℕ, card (Sym (Fin n) k) = mult theorem card_sym_eq_multichoose (α : Type*) (k : ℕ) [Fintype α] [Fintype (Sym α k)] : card (Sym α k) = multichoose (card α) k := by rw [← card_sym_fin_eq_multichoose] - exact card_congr (equivCongr (equivFin α)) + -- FIXME: Without the `Fintype` namespace, why does it complain about `Finset.card_congr` being + -- deprecated? + exact Fintype.card_congr (equivCongr (equivFin α)) #align sym.card_sym_eq_multichoose Sym.card_sym_eq_multichoose /-- The *stars and bars* lemma: the cardinality of `Sym α k` is equal to diff --git a/Mathlib/Data/Tree.lean b/Mathlib/Data/Tree.lean index 8487468575bcd..d26544415f418 100644 --- a/Mathlib/Data/Tree.lean +++ b/Mathlib/Data/Tree.lean @@ -22,6 +22,10 @@ We also specialize for `Tree Unit`, which is a binary tree without any additional data. We provide the notation `a △ b` for making a `Tree Unit` with children `a` and `b`. +## TODO + +Implement a `Traversable` instance for `Tree`. + ## References @@ -87,7 +91,7 @@ def getOrElse (n : PosNum) (t : Tree α) (v : α) : α := #align tree.get_or_else Tree.getOrElse /-- Apply a function to each value in the tree. This is the `map` function for the `Tree` functor. -TODO: implement `Traversable Tree`. -/ +-/ def map {β} (f : α → β) : Tree α → Tree β | nil => nil | node a l r => node (f a) (map f l) (map f r) diff --git a/Mathlib/Dynamics/Newton.lean b/Mathlib/Dynamics/Newton.lean index 4afaa0cde22e9..7783cb5d36d2c 100644 --- a/Mathlib/Dynamics/Newton.lean +++ b/Mathlib/Dynamics/Newton.lean @@ -25,7 +25,7 @@ such as Hensel's lemma and Jordan-Chevalley decomposition. * `Polynomial.isFixedPt_newtonMap_of_isUnit_iff`: `x` is a fixed point for Newton iteration iff it is a root of `P` (provided `P'(x)` is a unit). * `Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero`: if `x` is almost a root of `P` in the - sense that that `P(x)` is nilpotent (and `P'(x)` is a unit) then we may write `x` as a sum + sense that `P(x)` is nilpotent (and `P'(x)` is a unit) then we may write `x` as a sum `x = n + r` where `n` is nilpotent and `r` is a root of `P`. This can be used to prove the Jordan-Chevalley decomposition of linear endomorphims. @@ -98,7 +98,7 @@ theorem aeval_pow_two_pow_dvd_aeval_iterate_newtonMap · rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul] exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _ -/-- If `x` is almost a root of `P` in the sense that that `P(x)` is nilpotent (and `P'(x)` is a +/-- If `x` is almost a root of `P` in the sense that `P(x)` is nilpotent (and `P'(x)` is a unit) then we may write `x` as a sum `x = n + r` where `n` is nilpotent and `r` is a root of `P`. Moreover, `n` and `r` are unique. diff --git a/Mathlib/FieldTheory/IsPerfectClosure.lean b/Mathlib/FieldTheory/IsPerfectClosure.lean index 109d4b7a15acd..0f1cd7247fd5e 100644 --- a/Mathlib/FieldTheory/IsPerfectClosure.lean +++ b/Mathlib/FieldTheory/IsPerfectClosure.lean @@ -180,7 +180,7 @@ theorem IsPRadical.trans [IsPRadical i p] [IsPRadical f p] : rw [RingHom.mem_ker, RingHom.comp_apply, ← RingHom.mem_ker] at h simpa only [← Ideal.mem_comap, comap_pNilradical] using ker_le f p h -/-- If `i : K →+* L` is a `p`-radical ring homomorphism , then it makes `L` a perfect closure +/-- If `i : K →+* L` is a `p`-radical ring homomorphism, then it makes `L` a perfect closure of `K`, if `L` is perfect. In this case the kernel of `i` is equal to the `p`-nilradical of `K` (see `IsPerfectClosure.ker_eq`). diff --git a/Mathlib/Geometry/Euclidean/Basic.lean b/Mathlib/Geometry/Euclidean/Basic.lean index 6482810becaff..a2a0c03c67eb1 100644 --- a/Mathlib/Geometry/Euclidean/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Basic.lean @@ -289,7 +289,7 @@ nonrec def orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s] mk' (v +ᵥ p) s.directionᗮ := by rw [← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk', vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc] - refine' Submodule.add_mem _ (orthogonalProjectionFn_vsub_mem_direction_orthogonal p) _ + refine Submodule.add_mem _ (orthogonalProjectionFn_vsub_mem_direction_orthogonal p) ?_ rw [Submodule.mem_orthogonal'] intro w hw rw [← neg_sub, inner_neg_left, orthogonalProjection_inner_eq_zero _ w hw, neg_zero] diff --git a/Mathlib/Geometry/Manifold/Algebra/Structures.lean b/Mathlib/Geometry/Manifold/Algebra/Structures.lean index 3e15aaf3e9d6c..4e7876c5ed420 100644 --- a/Mathlib/Geometry/Manifold/Algebra/Structures.lean +++ b/Mathlib/Geometry/Manifold/Algebra/Structures.lean @@ -52,7 +52,7 @@ instance (priority := 100) fieldSmoothRing {𝕜 : Type*} [NontriviallyNormedFie { normedSpaceLieAddGroup with smooth_mul := by rw [smooth_iff] - refine' ⟨continuous_mul, fun x y => _⟩ + refine ⟨continuous_mul, fun x y => ?_⟩ simp only [mfld_simps] rw [contDiffOn_univ] exact contDiff_mul } diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean index b1e1872aebc80..422146f261078 100644 --- a/Mathlib/Geometry/Manifold/BumpFunction.lean +++ b/Mathlib/Geometry/Manifold/BumpFunction.lean @@ -294,7 +294,7 @@ theorem nhds_basis_tsupport : (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) := by rw [← map_extChartAt_symm_nhdsWithin_range I c] exact nhdsWithin_range_basis.map _ - refine' this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) + exact this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) fun f _ => f.tsupport_mem_nhds #align smooth_bump_function.nhds_basis_tsupport SmoothBumpFunction.nhds_basis_tsupport diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index fe80692f2901a..942bde5468fd6 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -323,7 +323,7 @@ def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where cases' he with he he · left have : e = e' := by - refine' eq_of_eqOnSource_univ (Setoid.symm he'e) _ _ <;> + refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_ <;> rw [Set.mem_singleton_iff.1 he] <;> rfl rwa [← this] · right @@ -383,15 +383,15 @@ def Pregroupoid.groupoid (PG : Pregroupoid H) : StructureGroupoid H where id_mem' := ⟨PG.id_mem, PG.id_mem⟩ locality' e he := by constructor - · refine' PG.locality e.open_source fun x xu ↦ _ + · refine PG.locality e.open_source fun x xu ↦ ?_ rcases he x xu with ⟨s, s_open, xs, hs⟩ - refine' ⟨s, s_open, xs, _⟩ + refine ⟨s, s_open, xs, ?_⟩ convert hs.1 using 1 dsimp [PartialHomeomorph.restr] rw [s_open.interior_eq] - · refine' PG.locality e.open_target fun x xu ↦ _ + · refine PG.locality e.open_target fun x xu ↦ ?_ rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩ - refine' ⟨e.target ∩ e.symm ⁻¹' s, _, ⟨xu, xs⟩, _⟩ + refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩ · exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open · rw [← inter_assoc, inter_self] convert hs.2 using 1 @@ -454,7 +454,7 @@ instance instStructureGroupoidOrderTop : OrderTop (StructureGroupoid H) where instance : CompleteLattice (StructureGroupoid H) := { SetLike.instPartialOrder, completeLatticeOfInf _ (by - refine' fun s => + exact fun s => ⟨fun S Ss F hF => mem_iInter₂.mp hF S Ss, fun T Tl F fT => mem_iInter₂.mpr (fun i his => Tl his fT)⟩) with le := (· ≤ ·) @@ -497,7 +497,7 @@ def idRestrGroupoid : StructureGroupoid H where id_mem' := ⟨univ, isOpen_univ, by simp only [mfld_simps, refl]⟩ locality' := by intro e h - refine' ⟨e.source, e.open_source, by simp only [mfld_simps], _⟩ + refine ⟨e.source, e.open_source, by simp only [mfld_simps], ?_⟩ intro x hx rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩ have hes : x ∈ (e.restr s).source := by @@ -1008,7 +1008,7 @@ instance hasGroupoid_model_space (H : Type*) [TopologicalSpace H] (G : Structure /-- Any charted space structure is compatible with the groupoid of all partial homeomorphisms. -/ instance hasGroupoid_continuousGroupoid : HasGroupoid M (continuousGroupoid H) := by - refine' ⟨fun _ _ ↦ _⟩ + refine ⟨fun _ _ ↦ ?_⟩ rw [continuousGroupoid, mem_groupoid_of_pregroupoid] simp only [and_self_iff] #align has_groupoid_continuous_groupoid hasGroupoid_continuousGroupoid @@ -1219,7 +1219,7 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G rw [hc.symm, mem_singleton_iff] at he rw [hc'.symm, mem_singleton_iff] at he' rw [he, he'] - refine' G.mem_of_eqOnSource _ + refine G.mem_of_eqOnSource ?_ (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x')) apply closedUnderRestriction' · exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _) @@ -1331,7 +1331,7 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') : rw [trans_source] at hx exact hx.1 · exact hg₂ - refine' ⟨s, open_s, this, _⟩ + refine ⟨s, open_s, this, ?_⟩ let F₁ := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c' have A : F₁ ∈ G := G.trans (e.mem_groupoid c g hc hg₁) (e'.mem_groupoid g c' hg₁ hc') let F₂ := (c.symm ≫ₕ f ≫ₕ c').restr s diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean index 3be65bdce490b..19291edd4d46a 100644 --- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean +++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean @@ -86,7 +86,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → have h4f := h4f.preimage_mem_nhds (extChartAt_source_mem_nhds I' (f x₀ (g x₀))) have h3f := contMDiffAt_iff_contMDiffAt_nhds.mp (hf.of_le <| (self_le_add_left 1 m).trans hmn) have h2f : ∀ᶠ x₂ in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂) := by - refine' ((continuousAt_id.prod hg.continuousAt).tendsto.eventually h3f).mono fun x hx => _ + refine ((continuousAt_id.prod hg.continuousAt).tendsto.eventually h3f).mono fun x hx => ?_ exact hx.comp (g x) (contMDiffAt_const.prod_mk contMDiffAt_id) have h2g := hg.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds I (g x₀)) have : @@ -99,7 +99,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → rw [contMDiffAt_iff] at hf hg simp_rw [Function.comp, uncurry, extChartAt_prod, PartialEquiv.prod_coe_symm, ModelWithCorners.range_prod] at hf ⊢ - refine' ContDiffWithinAt.fderivWithin _ hg.2 I.unique_diff hmn (mem_range_self _) _ + refine ContDiffWithinAt.fderivWithin ?_ hg.2 I.unique_diff hmn (mem_range_self _) ?_ · simp_rw [extChartAt_to_inv]; exact hf.2 · rw [← image_subset_iff] rintro _ ⟨x, -, rfl⟩ @@ -122,7 +122,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → writtenInExtChartAt I I' (g x) (f x) ∘ extChartAt I (g x) ∘ (extChartAt I (g x₀)).symm) (range I) (extChartAt I (g x₀) (g x))) x₀ := by - refine' this.congr_of_eventuallyEq _ + refine this.congr_of_eventuallyEq ?_ filter_upwards [h2g, h2f] intro x₂ hx₂ h2x₂ have : @@ -135,11 +135,11 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → rintro x ⟨hx, h2x⟩ simp_rw [writtenInExtChartAt, Function.comp_apply] rw [(extChartAt I (g x₂)).left_inv hx, (extChartAt I' (f x₂ (g x₂))).left_inv h2x] - refine' Filter.EventuallyEq.fderivWithin_eq_nhds _ - refine' eventually_of_mem (inter_mem _ _) this + refine Filter.EventuallyEq.fderivWithin_eq_nhds ?_ + refine eventually_of_mem (inter_mem ?_ ?_) this · exact extChartAt_preimage_mem_nhds' _ hx₂ (extChartAt_source_mem_nhds I (g x₂)) - refine' extChartAt_preimage_mem_nhds' _ hx₂ _ - exact h2x₂.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds _ _) + · refine extChartAt_preimage_mem_nhds' _ hx₂ ?_ + exact h2x₂.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds _ _) /- The conclusion is equal to the following, when unfolding coord_change of `tangentBundleCore` -/ -- Porting note: added @@ -155,7 +155,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → ((mfderiv I I' (f x) (g x)).comp (fderivWithin 𝕜 (extChartAt I (g x) ∘ (extChartAt I (g x₀)).symm) (range I) (extChartAt I (g x₀) (g x))))) x₀ := by - refine' this.congr_of_eventuallyEq _ + refine this.congr_of_eventuallyEq ?_ filter_upwards [h2g, h2f, h4f] intro x₂ hx₂ h2x₂ h3x₂ symm @@ -168,13 +168,13 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N → PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂))) h3x₂).differentiableWithinAt le_top have h3f := (h2x₂.mdifferentiableAt le_rfl).differentiableWithinAt_writtenInExtChartAt - refine' fderivWithin.comp₃ _ hI' h3f hI _ _ _ _ (I.unique_diff _ <| mem_range_self _) + refine fderivWithin.comp₃ _ hI' h3f hI ?_ ?_ ?_ ?_ (I.unique_diff _ <| mem_range_self _) · exact fun x _ => mem_range_self _ · exact fun x _ => mem_range_self _ · simp_rw [writtenInExtChartAt, Function.comp_apply, (extChartAt I (g x₂)).left_inv (mem_extChartAt_source I (g x₂))] · simp_rw [Function.comp_apply, (extChartAt I (g x₀)).left_inv hx₂] - refine' this.congr_of_eventuallyEq _ + refine this.congr_of_eventuallyEq ?_ filter_upwards [h2g, h4f] with x hx h2x rw [inTangentCoordinates_eq] · rfl diff --git a/Mathlib/Geometry/Manifold/Diffeomorph.lean b/Mathlib/Geometry/Manifold/Diffeomorph.lean index 8f96106c1f899..4b6301da0b366 100644 --- a/Mathlib/Geometry/Manifold/Diffeomorph.lean +++ b/Mathlib/Geometry/Manifold/Diffeomorph.lean @@ -577,8 +577,8 @@ def toTransDiffeomorph (e : E ≃ₘ[𝕜] F) : M ≃ₘ⟮I, I.transDiffeomorph · exact ⟨(extChartAt I x).map_source (mem_extChartAt_source I x), trivial, by simp only [mfld_simps]⟩ contMDiff_invFun x := by - refine' contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, _⟩ - refine' e.symm.contDiff.contDiffWithinAt.congr' (fun y hy => _) _ + refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩ + refine e.symm.contDiff.contDiffWithinAt.congr' (fun y hy => ?_) ?_ · simp only [mem_inter_iff, I.extChartAt_transDiffeomorph_target] at hy simp only [Equiv.coe_refl, Equiv.refl_symm, id, (· ∘ ·), I.coe_extChartAt_transDiffeomorph_symm, (extChartAt I x).right_inv hy.1] diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean index 62fdb2b7c1176..005354aa4e6f9 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean @@ -473,8 +473,8 @@ instance SmoothFiberwiseLinear.hasGroupoid : haveI : MemTrivializationAtlas e := ⟨he⟩ haveI : MemTrivializationAtlas e' := ⟨he'⟩ rw [mem_smoothFiberwiseLinear_iff] - refine' ⟨_, _, e.open_baseSet.inter e'.open_baseSet, smoothOn_coordChangeL IB e e', - smoothOn_symm_coordChangeL IB e e', _⟩ + refine ⟨_, _, e.open_baseSet.inter e'.open_baseSet, smoothOn_coordChangeL IB e e', + smoothOn_symm_coordChangeL IB e e', ?_⟩ refine PartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩ · simp only [e.symm_trans_source_eq e', FiberwiseLinear.partialHomeomorph, trans_toPartialEquiv, symm_toPartialEquiv] @@ -633,12 +633,12 @@ instance Bundle.Prod.smoothVectorBundle : SmoothVectorBundle (F₁ × F₂) (E smoothOn_coordChangeL := by rintro _ _ ⟨e₁, e₂, i₁, i₂, rfl⟩ ⟨e₁', e₂', i₁', i₂', rfl⟩ rw [SmoothOn] - refine' ContMDiffOn.congr _ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂') - refine' ContMDiffOn.clm_prodMap _ _ - · refine' (smoothOn_coordChangeL IB e₁ e₁').mono _ + refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂') + refine ContMDiffOn.clm_prodMap ?_ ?_ + · refine (smoothOn_coordChangeL IB e₁ e₁').mono ?_ simp only [Trivialization.baseSet_prod, mfld_simps] mfld_set_tac - · refine' (smoothOn_coordChangeL IB e₂ e₂').mono _ + · refine (smoothOn_coordChangeL IB e₂ e₂').mono ?_ simp only [Trivialization.baseSet_prod, mfld_simps] mfld_set_tac #align bundle.prod.smooth_vector_bundle Bundle.Prod.smoothVectorBundle diff --git a/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean b/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean index 72dcf40ad2640..3cba9f6f3cc08 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean @@ -143,7 +143,7 @@ theorem SmoothFiberwiseLinear.locality_aux₁ (e : PartialHomeomorph (B × F) (B refine ⟨Prod.fst '' e.source, he, ?_⟩ rintro x ⟨p, hp, rfl⟩ refine ⟨φ ⟨p, hp⟩, u ⟨p, hp⟩, hu ⟨p, hp⟩, ?_, hu' _, hφ ⟨p, hp⟩, h2φ ⟨p, hp⟩, ?_⟩ - · intro y hy; refine' ⟨(y, 0), heu ⟨p, hp⟩ ⟨_, _⟩ hy, rfl⟩ + · intro y hy; exact ⟨(y, 0), heu ⟨p, hp⟩ ⟨_, _⟩ hy, rfl⟩ · rw [← hesu, e.restr_source_inter]; exact heφ ⟨p, hp⟩ #align smooth_fiberwise_linear.locality_aux₁ SmoothFiberwiseLinear.locality_aux₁ diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean b/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean index 208c5bf53ad71..f412316f744f9 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean @@ -37,7 +37,7 @@ vector bundle `f *ᵖ E` is a smooth vector bundle. -/ instance SmoothVectorBundle.pullback : SmoothVectorBundle F (f *ᵖ E) IB' where smoothOn_coordChangeL := by rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩ - refine' ((smoothOn_coordChangeL _ e e').comp f.smooth.smoothOn fun b hb => hb).congr _ + refine ((smoothOn_coordChangeL _ e e').comp f.smooth.smoothOn fun b hb => hb).congr ?_ rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet); ext v show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _] diff --git a/Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean b/Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean index 4063280a30bb0..1d5264b700602 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean @@ -117,8 +117,8 @@ instance instAdd : Add Cₛ^n⟮I; F, V⟯ := by have ht := t.contMDiff x₀ rw [contMDiffAt_section] at hs ht ⊢ set e := trivializationAt F V x₀ - refine' (hs.add ht).congr_of_eventuallyEq _ - refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _ + refine (hs.add ht).congr_of_eventuallyEq ?_ + refine eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) ?_ intro x hx apply (e.linear 𝕜 hx).1 #align cont_mdiff_section.has_add ContMDiffSection.instAdd @@ -135,8 +135,8 @@ instance instSub : Sub Cₛ^n⟮I; F, V⟯ := by have ht := t.contMDiff x₀ rw [contMDiffAt_section] at hs ht ⊢ set e := trivializationAt F V x₀ - refine' (hs.sub ht).congr_of_eventuallyEq _ - refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _ + refine (hs.sub ht).congr_of_eventuallyEq ?_ + refine eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) ?_ intro x hx apply (e.linear 𝕜 hx).map_sub #align cont_mdiff_section.has_sub ContMDiffSection.instSub @@ -165,9 +165,8 @@ instance instSMul : SMul 𝕜 Cₛ^n⟮I; F, V⟯ := by have hs := s.contMDiff x₀ rw [contMDiffAt_section] at hs ⊢ set e := trivializationAt F V x₀ - refine' (contMDiffAt_const.smul hs).congr_of_eventuallyEq _ - · exact c - refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _ + refine ((contMDiffAt_const (c := c)).smul hs).congr_of_eventuallyEq ?_ + refine eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) ?_ intro x hx apply (e.linear 𝕜 hx).2 #align cont_mdiff_section.has_smul ContMDiffSection.instSMul @@ -183,8 +182,8 @@ instance instNeg : Neg Cₛ^n⟮I; F, V⟯ := by have hs := s.contMDiff x₀ rw [contMDiffAt_section] at hs ⊢ set e := trivializationAt F V x₀ - refine' hs.neg.congr_of_eventuallyEq _ - refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _ + refine hs.neg.congr_of_eventuallyEq ?_ + refine eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) ?_ intro x hx apply (e.linear 𝕜 hx).map_neg #align cont_mdiff_section.has_neg ContMDiffSection.instNeg diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean index 905e5c4678749..8e263358b6945 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean @@ -92,8 +92,8 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where exact (i.1.extend I).right_inv hy · simp_rw [Function.comp_apply, i.1.extend_left_inv I hx] continuousOn_coordChange i j := by - refine' (contDiffOn_fderiv_coord_change I i j).continuousOn.comp - ((i.1.continuousOn_extend I).mono _) _ + refine (contDiffOn_fderiv_coord_change I i j).continuousOn.comp + ((i.1.continuousOn_extend I).mono ?_) ?_ · rw [i.1.extend_source]; exact inter_subset_left _ _ simp_rw [← i.1.extend_image_source_inter, mapsTo_image] coordChange_comp := by @@ -352,7 +352,7 @@ instance tangentBundleCore.isSmooth : (tangentBundleCore I M).IsSmooth I := by refine ⟨fun i j => ?_⟩ rw [SmoothOn, contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas I i.2), contMDiffOn_iff_contDiffOn] - · refine' ((contDiffOn_fderiv_coord_change I i j).congr fun x hx => _).mono _ + · refine ((contDiffOn_fderiv_coord_change I i j).congr fun x hx => ?_).mono ?_ · rw [PartialEquiv.trans_source'] at hx simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1] · exact (i.1.extend_image_source_inter j.1 I).subset diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index b6d779960ced5..410124117c27c 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -995,9 +995,9 @@ def pullbackConeOfLeftIsLimit : IsLimit (pullbackConeOfLeft f g) := PullbackCone.isLimitAux' _ fun s => by refine' ⟨LocallyRingedSpace.Hom.mk (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.1 g.1 (PullbackCone.mk _ _ (congr_arg LocallyRingedSpace.Hom.val s.condition))) _, - LocallyRingedSpace.Hom.ext _ _ + LocallyRingedSpace.Hom.ext ?_ _ (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst f.1 g.1 _), - LocallyRingedSpace.Hom.ext _ _ + LocallyRingedSpace.Hom.ext ?_ _ (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 _), _⟩ · intro x have := diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index 0c1f95b07227b..68cee56441288 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean @@ -341,8 +341,8 @@ diagram. We will lift these maps into `ιInvApp`. -/ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) : (𝖣.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op j) := by rcases j with (⟨j, k⟩ | j) - · refine' - D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom _) + · refine + D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom ?_) rw [Functor.op_obj] congr 1; ext1 dsimp only [Functor.op_obj, Opens.map_coe, unop_op, IsOpenMap.functor_obj_coe] @@ -527,8 +527,8 @@ Vᵢⱼ ⟶ Uᵢ -/ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) := PullbackCone.isLimitAux' _ fun s => by - refine' ⟨_, _, _, _⟩ - · refine' PresheafedSpace.IsOpenImmersion.lift (D.f i j) s.fst _ + refine ⟨?_, ?_, ?_, ?_⟩ + · refine PresheafedSpace.IsOpenImmersion.lift (D.f i j) s.fst ?_ erw [← D.toTopGlueData.preimage_range j i] have : s.fst.base ≫ D.toTopGlueData.ι i = diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean index 61a7192d1a819..d9257cbc00346 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean @@ -237,15 +237,15 @@ def descCApp (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (U : (Opens (colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) _* limit (pushforwardDiagramToColimit F).leftOp).obj U := by - refine' + refine limit.lift _ { pt := s.pt.presheaf.obj U π := - { app := fun j => _ - naturality := fun j j' f => _ } } ≫ + { app := fun j => ?_ + naturality := fun j j' f => ?_ } } ≫ (limitObjIsoLimitCompEvaluation _ _).inv -- We still need to construct the `app` and `naturality'` fields omitted above. - · refine' (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom _) + · refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ?_) dsimp rw [← Opens.map_comp_obj] simp @@ -384,11 +384,11 @@ via taking componentwise limits. def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v} C) [HasColimit F] (U : Opens (Limits.colimit F).carrier) : (Limits.colimit F).presheaf.obj (op U) ≅ limit (componentwiseDiagram F U) := by - refine' + refine ((sheafIsoOfIso (colimit.isoColimitCocone ⟨_, colimitCoconeIsColimit F⟩).symm).app (op U)).trans - _ - refine' (limitObjIsoLimitCompEvaluation _ _).trans (Limits.lim.mapIso _) + ?_ + refine (limitObjIsoLimitCompEvaluation _ _).trans (Limits.lim.mapIso ?_) fapply NatIso.ofComponents · intro X refine (F.obj (unop X)).presheaf.mapIso (eqToIso ?_) diff --git a/Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/Geometry/RingedSpace/Stalks.lean index ad56c93d17533..3ff684300785f 100644 --- a/Mathlib/Geometry/RingedSpace/Stalks.lean +++ b/Mathlib/Geometry/RingedSpace/Stalks.lean @@ -204,10 +204,10 @@ instance isIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) [IsIso α] (x -- type for an inverse. -- To get a proper inverse, we need to compose with the `eqToHom` arrow -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`. - refine' + refine ⟨eqToHom (show X.stalk x = X.stalk ((α ≫ β).base x) by rw [h_eq]) ≫ (stalkMap β (α.base x) : _), - _, _⟩ + ?_, ?_⟩ · rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc] erw [← stalkMap.comp β α (α.base x)] rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl, diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 7493468b12e03..9c37fb1d7aaa7 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -745,18 +745,16 @@ theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : σ.support.car #align equiv.perm.is_cycle.is_conj Equiv.Perm.IsCycle.isConj theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) : - IsConj σ τ ↔ σ.support.card = τ.support.card := - ⟨by - intro h + IsConj σ τ ↔ σ.support.card = τ.support.card where + mp h := by obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h - refine Finset.card_congr (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab) - fun b hb => ?_ + refine Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab) + fun b hb ↦ ⟨π⁻¹ b, ?_, π.apply_inv_self b⟩ · simp [mem_support.1 ha] - · refine ⟨π⁻¹ b, ⟨?_, π.apply_inv_self b⟩⟩ - contrapose! hb - rw [mem_support, Classical.not_not] at hb - rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self], - hσ.isConj hτ⟩ + contrapose! hb + rw [mem_support, Classical.not_not] at hb + rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self] + mpr := hσ.isConj hτ #align equiv.perm.is_cycle.is_conj_iff Equiv.Perm.IsCycle.isConj_iff end Conjugation diff --git a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean index 238288c482b1a..99c2ea353f966 100644 --- a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean +++ b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean @@ -85,7 +85,7 @@ theorem star_eigenvectorUnitary_mulVec (j : n) : (star (eigenvectorUnitary hA : Matrix n n 𝕜)) *ᵥ ⇑(hA.eigenvectorBasis j) = Pi.single j 1 := by rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, unitary.coe_star_mul_self, one_mulVec] -/--Unitary diagonalization of a Hermitian matrix.-/ +/-- Unitary diagonalization of a Hermitian matrix. -/ theorem star_mul_self_mul_eq_diagonal : (star (eigenvectorUnitary hA : Matrix n n 𝕜)) * A * (eigenvectorUnitary hA : Matrix n n 𝕜) = diagonal (RCLike.ofReal ∘ hA.eigenvalues) := by diff --git a/Mathlib/LinearAlgebra/UnitaryGroup.lean b/Mathlib/LinearAlgebra/UnitaryGroup.lean index e3c86c44881ff..34d52e9c4e93e 100644 --- a/Mathlib/LinearAlgebra/UnitaryGroup.lean +++ b/Mathlib/LinearAlgebra/UnitaryGroup.lean @@ -206,7 +206,7 @@ section specialUnitaryGroup variable (n) (α) -/--`Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant +/-- `Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant is 1. (This definition is only correct if 2 is invertible.)-/ abbrev specialUnitaryGroup := unitaryGroup n α ⊓ MonoidHom.mker detMonoidHom diff --git a/Mathlib/MeasureTheory/Function/AEEqFun.lean b/Mathlib/MeasureTheory/Function/AEEqFun.lean index 2fea4719cfec2..d725ac119b07c 100644 --- a/Mathlib/MeasureTheory/Function/AEEqFun.lean +++ b/Mathlib/MeasureTheory/Function/AEEqFun.lean @@ -69,9 +69,6 @@ function space, almost everywhere equal, `L⁰`, ae_eq_fun -/ -set_option autoImplicit true - - noncomputable section open scoped Classical @@ -242,7 +239,7 @@ end compQuasiMeasurePreserving section compMeasurePreserving -variable [MeasurableSpace β] {ν : MeasureTheory.Measure β} +variable [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} {g : β → γ} /-- Composition of an almost everywhere equal function and a quasi measure preserving function. @@ -252,8 +249,7 @@ def compMeasurePreserving (g : β →ₘ[ν] γ) (f : α → β) (hf : MeasurePr g.compQuasiMeasurePreserving f hf.quasiMeasurePreserving @[simp] -theorem compMeasurePreserving_mk {g : β → γ} (hg : AEStronglyMeasurable g ν) - (hf : MeasurePreserving f μ ν) : +theorem compMeasurePreserving_mk (hg : AEStronglyMeasurable g ν) (hf : MeasurePreserving f μ ν) : (mk g hg).compMeasurePreserving f hf = mk (g ∘ f) (hg.comp_quasiMeasurePreserving hf.quasiMeasurePreserving) := rfl @@ -457,13 +453,13 @@ theorem toGerm_injective : Injective (toGerm : (α →ₘ[μ] β) → Germ μ.ae #align measure_theory.ae_eq_fun.to_germ_injective MeasureTheory.AEEqFun.toGerm_injective @[simp] -theorem compQuasiMeasurePreserving_toGerm [MeasurableSpace β] {ν} +theorem compQuasiMeasurePreserving_toGerm [MeasurableSpace β] {f : α → β} {ν} (g : β →ₘ[ν] γ) (hf : Measure.QuasiMeasurePreserving f μ ν) : (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f hf.tendsto_ae := by rcases g; rfl @[simp] -theorem compMeasurePreserving_toGerm [MeasurableSpace β] {ν} +theorem compMeasurePreserving_toGerm [MeasurableSpace β] {f : α → β} {ν} (g : β →ₘ[ν] γ) (hf : MeasurePreserving f μ ν) : (g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f hf.quasiMeasurePreserving.tendsto_ae := diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean index 316deedb777d0..9853325217ac5 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean @@ -63,9 +63,9 @@ theorem congr (hf : AEStronglyMeasurable' m f μ) (hfg : f =ᵐ[μ] g) : AEStron by obtain ⟨f', hf'_meas, hff'⟩ := hf; exact ⟨f', hf'_meas, hfg.symm.trans hff'⟩ #align measure_theory.ae_strongly_measurable'.congr MeasureTheory.AEStronglyMeasurable'.congr -set_option autoImplicit true in -theorem mono (hf : AEStronglyMeasurable' m f μ) (hm : m ≤ m') : AEStronglyMeasurable' m' f μ := by - obtain ⟨f', hf'_meas, hff'⟩ := hf; exact ⟨f', hf'_meas.mono hm, hff'⟩ +theorem mono {m'} (hf : AEStronglyMeasurable' m f μ) (hm : m ≤ m') : + AEStronglyMeasurable' m' f μ := + let ⟨f', hf'_meas, hff'⟩ := hf; ⟨f', hf'_meas.mono hm, hff'⟩ theorem add [Add β] [ContinuousAdd β] (hf : AEStronglyMeasurable' m f μ) (hg : AEStronglyMeasurable' m g μ) : AEStronglyMeasurable' m (f + g) μ := by diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 72427226bb720..5b6f673186dc3 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -556,9 +556,7 @@ For a set `s` with `(hs : MeasurableSet s)` and `(hμs : μ s < ∞)`, we build section Indicator -set_option autoImplicit true - -variable {c : E} {f : α → E} {hf : AEStronglyMeasurable f μ} +variable {c : E} {f : α → E} {hf : AEStronglyMeasurable f μ} {s : Set α} theorem snormEssSup_indicator_le (s : Set α) (f : α → G) : snormEssSup (s.indicator f) μ ≤ snormEssSup f μ := by @@ -585,8 +583,7 @@ theorem snormEssSup_indicator_const_eq (s : Set α) (c : G) (hμs : μ s ≠ 0) rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem] #align measure_theory.snorm_ess_sup_indicator_const_eq MeasureTheory.snormEssSup_indicator_const_eq -theorem snorm_indicator_le (f : α → E) {s : Set α} : - snorm (s.indicator f) p μ ≤ snorm f p μ := by +theorem snorm_indicator_le (f : α → E) : snorm (s.indicator f) p μ ≤ snorm f p μ := by refine snorm_mono_ae (eventually_of_forall fun x => ?_) suffices ‖s.indicator f x‖₊ ≤ ‖f x‖₊ by exact NNReal.coe_mono this rw [nnnorm_indicator_eq_indicator_nnnorm] @@ -725,7 +722,7 @@ theorem exists_snorm_indicator_le (hp : p ≠ ∞) (c : E) {ε : ℝ≥0∞} (h exact mul_le_mul_left' (ENNReal.rpow_le_rpow hs hp₀') _ #align measure_theory.exists_snorm_indicator_le MeasureTheory.exists_snorm_indicator_le -lemma Memℒp.piecewise [DecidablePred (· ∈ s)] +protected lemma Memℒp.piecewise [DecidablePred (· ∈ s)] {g} (hs : MeasurableSet s) (hf : Memℒp f p (μ.restrict s)) (hg : Memℒp g p (μ.restrict sᶜ)) : Memℒp (s.piecewise f g) p μ := by by_cases hp_zero : p = 0 diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index c20081c0fdce3..ca83d8b766a5b 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -456,7 +456,7 @@ theorem lintegral_eq_iSup_eapprox_lintegral {f : α → ℝ≥0∞} (hf : Measur #align measure_theory.lintegral_eq_supr_eapprox_lintegral MeasureTheory.lintegral_eq_iSup_eapprox_lintegral /-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends -to zero as `μ s` tends to zero. This lemma states states this fact in terms of `ε` and `δ`. -/ +to zero as `μ s` tends to zero. This lemma states this fact in terms of `ε` and `δ`. -/ theorem exists_pos_set_lintegral_lt_of_measure_lt {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ δ > 0, ∀ s, μ s < δ → ∫⁻ x in s, f x ∂μ < ε := by rcases exists_between (pos_iff_ne_zero.mpr hε) with ⟨ε₂, hε₂0, hε₂ε⟩ diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean index d9e64b13cbe8e..68613dde9e1e6 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean @@ -266,7 +266,7 @@ theorem injective_mapNatBool [MeasurableSpace α] [CountablyGenerated α] exact congr_fun hxy n /-- If a measurable space is countably generated and separates points, it is measure equivalent -to some some subset of the Cantor space `ℕ → Bool` (equipped with the product sigma algebra). +to some subset of the Cantor space `ℕ → Bool` (equipped with the product sigma algebra). Note: `s` need not be measurable, so this map need not be a `MeasurableEmbedding` to the Cantor Space. -/ theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α] diff --git a/Mathlib/NumberTheory/LSeries/HurwitzZeta.lean b/Mathlib/NumberTheory/LSeries/HurwitzZeta.lean new file mode 100644 index 0000000000000..9e2ea7413d3bb --- /dev/null +++ b/Mathlib/NumberTheory/LSeries/HurwitzZeta.lean @@ -0,0 +1,187 @@ +/- +Copyright (c) 2024 David Loeffler. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Loeffler +-/ + +import Mathlib.NumberTheory.LSeries.HurwitzZetaEven +import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd +import Mathlib.Analysis.SpecialFunctions.Gamma.Beta + +/-! +# The Hurwitz zeta function + +This file gives the definition and properties of the following two functions: + +* The **Hurwitz zeta function**, which is the meromorphic continuation to all `s ∈ ℂ` of the + function defined for `1 < re s` by the series + + `∑' n, 1 / (n + a) ^ s` + + for a parameter `a ∈ ℝ`, with the sum taken over all `n` such that `n + a > 0`; + +* the related sum, which we call the "**exponential zeta function**" (does it have a standard name?) + + `∑' n : ℕ, exp (2 * π * I * n * a) / n ^ s`. + +## Main definitions and results + +* `hurwitzZeta`: the Hurwitz zeta function (defined to be periodic in `a` with period 1) +* `expZeta`: the exponential zeta function +* `hasSum_nat_hurwitzZeta_of_mem_Icc` and `hasSum_expZeta_of_one_lt_re`: + relation to Dirichlet series for `1 < re s` +* ` hurwitzZeta_residue_one` shows that the residue at `s = 1` equals `1` +* `differentiableAt_hurwitzZeta` and `differentiableAt_expZeta`: analyticity away from `s = 1` +* `hurwitzZeta_one_sub` and `expZeta_one_sub`: functional equations `s ↔ 1 - s`. +-/ + +open Set Real Complex Filter Topology + +/-! +## The Hurwitz zeta function +-/ + +/-- The Hurwitz zeta function, which is the meromorphic continuation of +`∑ (n : ℕ), 1 / (n + a) ^ s` if `0 ≤ a ≤ 1`. See `hasSum_hurwitzZeta_of_one_lt_re` for the relation +to the Dirichlet series in the convergence range. -/ +noncomputable def hurwitzZeta (a : UnitAddCircle) (s : ℂ) := + hurwitzZetaEven a s + hurwitzZetaOdd a s + +lemma hurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) : + hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2 := by + simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg] + ring_nf + +lemma hurwitzZetaOdd_eq (a : UnitAddCircle) (s : ℂ) : + hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2 := by + simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg] + ring_nf + +/-- The Hurwitz zeta function is differentiable away from `s = 1`. -/ +lemma differentiableAt_hurwitzZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 1) : + DifferentiableAt ℂ (hurwitzZeta a) s := + (differentiableAt_hurwitzZetaEven a hs).add (differentiable_hurwitzZetaOdd a s) + +/-- Formula for `hurwitzZeta s` as a Dirichlet series in the convergence range. We +restrict to `a ∈ Icc 0 1` to simplify the statement. -/ +lemma hasSum_hurwitzZeta_of_one_lt_re {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) : + HasSum (fun n : ℕ ↦ 1 / (n + a : ℂ) ^ s) (hurwitzZeta a s) := by + convert (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add + (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs) using 1 + ext1 n + -- plain `ring_nf` works here, but the following is faster: + apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring + +/-- The residue of the Hurwitz zeta function at `s = 1` is `1`. -/ +lemma hurwitzZeta_residue_one (a : UnitAddCircle) : + Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1) := by + simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))] + refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds) + exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _] + +lemma differentiableAt_hurwitzZeta_sub_one_div (a : UnitAddCircle) : + DifferentiableAt ℂ (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) 1 := by + simp only [hurwitzZeta, add_sub_right_comm] + exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1) + +/-- Expression for `hurwitzZeta a 1` as a limit. (Mathematically `hurwitzZeta a 1` is +undefined, but our construction assigns some value to it; this lemma is mostly of interest for +determining what that value is). -/ +lemma tendsto_hurwitzZeta_sub_one_div_nhds_one (a : UnitAddCircle) : + Tendsto (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1) (𝓝 (hurwitzZeta a 1)) := by + simp only [hurwitzZeta, add_sub_right_comm] + refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add ?_ + exact (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto + +/-- The difference of two Hurwitz zeta functions is differentiable everywhere. -/ +lemma differentiable_hurwitzZeta_sub_hurwitzZeta (a b : UnitAddCircle) : + Differentiable ℂ (fun s ↦ hurwitzZeta a s - hurwitzZeta b s) := by + simp only [hurwitzZeta, add_sub_add_comm] + refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (Differentiable.sub ?_ ?_) + all_goals apply differentiable_hurwitzZetaOdd + +/-! +## The exponential zeta function +-/ + +/-- Meromorphic continuation of the series `∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s`. See +`hasSum_expZeta_of_one_lt_re` for the relation to the Dirichlet series. -/ +noncomputable def expZeta (a : UnitAddCircle) (s : ℂ) := + cosZeta a s + I * sinZeta a s + +lemma cosZeta_eq (a : UnitAddCircle) (s : ℂ) : + cosZeta a s = (expZeta a s + expZeta (-a) s) / 2 := by + rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg] + ring_nf + +lemma sinZeta_eq (a : UnitAddCircle) (s : ℂ) : + sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I) := by + rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg] + field_simp + ring_nf + +lemma hasSum_expZeta_of_one_lt_re (a : ℝ) {s : ℂ} (hs : 1 < re s) : + HasSum (fun n : ℕ ↦ cexp (2 * π * I * a * n) / n ^ s) (expZeta a s) := by + convert (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1 + ext1 n + simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast] + rw [add_div, mul_div, mul_comm _ I] + +lemma differentiableAt_expZeta (a : UnitAddCircle) (s : ℂ) (hs : s ≠ 1 ∨ a ≠ 0) : + DifferentiableAt ℂ (expZeta a) s := by + apply DifferentiableAt.add + · exact differentiableAt_cosZeta a hs + · apply (differentiableAt_const _).mul (differentiableAt_sinZeta a s) + +/-- If `a ≠ 0` then the exponential zeta function is analytic everywhere. -/ +lemma differentiable_expZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : + Differentiable ℂ (expZeta a) := + (differentiableAt_expZeta a · (Or.inr ha)) + +/-- Reformulation of `hasSum_expZeta_of_one_lt_re` using `LSeriesHasSum`. -/ +lemma LSeriesHasSum_exp (a : ℝ) {s : ℂ} (hs : 1 < re s) : + LSeriesHasSum (cexp <| 2 * π * I * a * ·) s (expZeta a s) := by + refine (hasSum_expZeta_of_one_lt_re a hs).congr_fun (fun n ↦ ?_) + rcases eq_or_ne n 0 with rfl | hn + · rw [LSeries.term_zero, Nat.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero] + · apply LSeries.term_of_ne_zero hn + +/-! +## The functional equation +-/ + +lemma hurwitzZeta_one_sub (a : UnitAddCircle) {s : ℂ} + (hs : ∀ (n : ℕ), s ≠ -n) (hs' : a ≠ 0 ∨ s ≠ 1) : + hurwitzZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s * + (exp (-π * I * s / 2) * expZeta a s + exp (π * I * s / 2) * expZeta (-a) s) := by + rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs, + expZeta, expZeta, Complex.cos, Complex.sin, sinZeta_neg, cosZeta_neg] + rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring, + show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring] + -- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but + -- make it run faster: + generalize (2 * π : ℂ) ^ (-s) = x + generalize (↑π * s / 2 * I).exp = y + generalize (-(↑π * s / 2) * I).exp = z + ring_nf + +/-- Functional equation for the exponential zeta function. -/ +lemma expZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) : + expZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s * + (exp (π * I * s / 2) * hurwitzZeta a s + exp (-π * I * s / 2) * hurwitzZeta (-a) s) := by + have hs' (n : ℕ) : s ≠ -↑n := by + convert hs (n + 1) using 1 + push_cast + ring + rw [expZeta, cosZeta_one_sub a hs, sinZeta_one_sub a hs', hurwitzZeta, hurwitzZeta, + hurwitzZetaEven_neg, hurwitzZetaOdd_neg, Complex.cos, Complex.sin] + rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring, + show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring] + -- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but + -- make it run faster: + generalize (2 * π : ℂ) ^ (-s) = x + generalize (↑π * s / 2 * I).exp = y + generalize (-(↑π * s / 2) * I).exp = z + ring_nf + rw [I_sq] + ring_nf diff --git a/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean b/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean index 8f919ba2e7c4b..48235d66ade57 100644 --- a/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean +++ b/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean @@ -34,7 +34,7 @@ We also define completed versions of these functions with nicer functional equat modified versions with a subscript `0`, which are entire functions differing from the above by multiples of `1 / s` and `1 / (1 - s)`. -## Main definitions and theorems +## Main definitions and theorems * `hurwitzZetaEven` and `cosZeta`: the zeta functions * `completedHurwitzZetaEven` and `completedCosZeta`: completed variants * `differentiableAt_hurwitzZetaEven` and `differentiableAt_cosZeta`: diff --git a/Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean b/Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean index 1da450aed8bda..0ba8a8d2a4bf1 100644 --- a/Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean +++ b/Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean @@ -28,7 +28,7 @@ Of course, we cannot *define* these functions by the above formulae (since exist analytic continuation is not at all obvious); we in fact construct them as Mellin transforms of various versions of the Jacobi theta function. -## Main definitions and theorems +## Main definitions and theorems * `completedHurwitzZetaOdd`: the completed Hurwitz zeta function * `completedSinZeta`: the completed cosine zeta function @@ -541,7 +541,7 @@ lemma hasSum_nat_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) : · simp only [Nat.cast_zero, Int.sign_zero, Int.cast_zero, mul_zero, zero_mul, neg_zero, sub_self, zero_div, zero_add] -/-- Reformulation of `hasSum_nat_cosZeta` using `LSeriesHasSum`. -/ +/-- Reformulation of `hasSum_nat_sinZeta` using `LSeriesHasSum`. -/ lemma LSeriesHasSum_sin (a : ℝ) {s : ℂ} (hs : 1 < re s) : LSeriesHasSum (Real.sin <| 2 * π * a * ·) s (sinZeta a s) := by refine (hasSum_nat_sinZeta a hs).congr_fun (fun n ↦ ?_) diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index e075bc6451ced..fd3a4c53905eb 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -181,16 +181,11 @@ private theorem sum_Ico_eq_card_lt {p q : ℕ} : _ ≤ _ := Nat.div_mul_div_le_div _ _ _ _ = _ := by rw [← card_sigma] - exact card_congr (fun a _ => ⟨a.1, a.2⟩) (by - simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, + exact card_nbij' (fun a ↦ ⟨a.1, a.2⟩) (fun a ↦ ⟨a.1, a.2⟩) + (by simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, forall_true_iff, mem_product]) - (fun ⟨_, _⟩ ⟨_, _⟩ => by - simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, - and_self_iff, heq_iff_eq, forall_true_iff]) - fun ⟨b₁, b₂⟩ h => ⟨⟨b₁, b₂⟩, by - revert h - simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, - exists_prop_of_true, mem_sigma, and_self_iff, forall_true_iff, mem_product]⟩ + (by simp (config := { contextual := true }) only [mem_filter, mem_sigma, and_self_iff, + forall_true_iff, mem_product]) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) /-- Each of the sums in this lemma is the cardinality of the set of integer points in each of the two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them @@ -202,17 +197,10 @@ theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0 ((Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ).filter fun x : ℕ × ℕ => x.2 * q ≤ x.1 * p).card = ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p).card := - card_congr (fun x _ => Prod.swap x) + card_equiv (Equiv.prodComm _ _) (fun ⟨_, _⟩ => by simp (config := { contextual := true }) only [mem_filter, and_self_iff, Prod.swap_prod_mk, - forall_true_iff, mem_product]) - (fun ⟨_, _⟩ ⟨_, _⟩ => by - simp (config := { contextual := true }) only [Prod.mk.inj_iff, eq_self_iff_true, - and_self_iff, Prod.swap_prod_mk, forall_true_iff]) - fun ⟨x₁, x₂⟩ h => ⟨⟨x₂, x₁⟩, by - revert h - simp (config := { contextual := true }) only [mem_filter, eq_self_iff_true, and_self_iff, - exists_prop_of_true, Prod.swap_prod_mk, forall_true_iff, mem_product]⟩ + forall_true_iff, mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm]) have hdisj : Disjoint ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.2 * p ≤ x.1 * q) ((Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ).filter fun x : ℕ × ℕ => x.1 * q ≤ x.2 * p) := by diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index d513e0dc90507..576f81f4c59dd 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -788,9 +788,8 @@ theorem NeBot.nonempty (f : Filter α) [hf : f.NeBot] : Nonempty α := equal. -/ theorem eq_top_of_neBot [Subsingleton α] (l : Filter α) [NeBot l] : l = ⊤ := by refine top_unique fun s hs => ?_ - obtain rfl : s = univ - · exact Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs) - · exact univ_mem + obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs) + exact univ_mem #align filter.eq_top_of_ne_bot Filter.eq_top_of_neBot theorem forall_mem_nonempty_iff_neBot {f : Filter α} : @@ -1437,6 +1436,12 @@ theorem frequently_principal {a : Set α} {p : α → Prop} : (∃ᶠ x in 𝓟 simp [Filter.Frequently, not_forall] #align filter.frequently_principal Filter.frequently_principal +theorem frequently_inf_principal {f : Filter α} {s : Set α} {p : α → Prop} : + (∃ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ x in f, x ∈ s ∧ p x := by + simp only [Filter.Frequently, eventually_inf_principal, not_and] + +alias ⟨Frequently.of_inf_principal, Frequently.inf_principal⟩ := frequently_inf_principal + theorem frequently_sup {p : α → Prop} {f g : Filter α} : (∃ᶠ x in f ⊔ g, p x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in g, p x := by simp only [Filter.Frequently, eventually_sup, not_and_or] @@ -2175,6 +2180,14 @@ theorem pure_bind (a : α) (m : α → Filter β) : bind (pure a) m = m a := by simp only [Bind.bind, bind, map_pure, join_pure] #align filter.pure_bind Filter.pure_bind +theorem map_bind {α β} (m : β → γ) (f : Filter α) (g : α → Filter β) : + map m (bind f g) = bind f (map m ∘ g) := + rfl + +theorem bind_map {α β} (m : α → β) (f : Filter α) (g : β → Filter γ) : + (bind (map m f) g) = bind f (g ∘ m) := + rfl + /-! ### `Filter` as a `Monad` @@ -2345,6 +2358,11 @@ theorem comap_principal {t : Set β} : comap m (𝓟 t) = 𝓟 (m ⁻¹' t) := fun h => ⟨t, Subset.rfl, h⟩⟩ #align filter.comap_principal Filter.comap_principal +theorem principal_subtype {α : Type*} (s : Set α) (t : Set s) : + 𝓟 t = comap (↑) (𝓟 (((↑) : s → α) '' t)) := by + rw [comap_principal, preimage_image_eq _ Subtype.coe_injective] +#align principal_subtype Filter.principal_subtype + @[simp] theorem comap_pure {b : β} : comap m (pure b) = 𝓟 (m ⁻¹' {b}) := by rw [← principal_singleton, comap_principal] diff --git a/Mathlib/Order/Filter/Curry.lean b/Mathlib/Order/Filter/Curry.lean index 62907f80d8252..02276cc199fe2 100644 --- a/Mathlib/Order/Filter/Curry.lean +++ b/Mathlib/Order/Filter/Curry.lean @@ -21,12 +21,16 @@ yields the quantifier order `∃ ∀ ∃ ∀`. For instance, This is different from a product filter, which instead yields a quantifier order `∃ ∃ ∀ ∀`. For instance, `∀ᶠ n in at_top ×ˢ at_top, p n ↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)`. This makes it clear that if something eventually occurs on the product filter, it eventually occurs on the curried -filter (see `Filter.curry_le_prod` and `Filter.eventually.curry`), but the converse is not true. +filter (see `Filter.curry_le_prod` and `Filter.Eventually.curry`), but the converse is not true. Another way to think about the curried versus the product filter is that tending to some limit on the product filter is a version of uniform convergence (see `tendsto_prod_filter_iff`) whereas tending to some limit on a curried filter is just iterated limits (see `Filter.Tendsto.curry`). +In the "generalized set" intuition, `Filter.prod` and `Filter.curry` correspond to two ways of +describing the product of two sets, namely `s ×ˢ t = fst ⁻¹' s ∩ snd ⁻¹' t` and +`s ×ˢ t = ⋃ x ∈ s, (x, ·) '' t`. + ## Main definitions * `Filter.curry`: A binary operation on filters which represents iterated limits @@ -51,13 +55,8 @@ variable {α β γ : Type*} `(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)`. Useful in adding quantifiers to the middle of `Tendsto`s. See `hasFDerivAt_of_tendstoUniformlyOnFilter`. -/ -def curry (f : Filter α) (g : Filter β) : Filter (α × β) where - sets := { s | ∀ᶠ a : α in f, ∀ᶠ b : β in g, (a, b) ∈ s } - univ_sets := by simp only [Set.mem_setOf_eq, Set.mem_univ, eventually_true] - sets_of_superset := fun hx hxy => - hx.mono fun a ha => ha.mono fun b hb => Set.mem_of_subset_of_mem hxy hb - inter_sets := fun hx hy => - (hx.and hy).mono fun a ha => (ha.1.and ha.2).mono fun b hb => hb +def curry (f : Filter α) (g : Filter β) : Filter (α × β) := + bind f fun a ↦ map (a, ·) g #align filter.curry Filter.curry theorem eventually_curry_iff {f : Filter α} {g : Filter β} {p : α × β → Prop} : diff --git a/Mathlib/Order/Filter/SmallSets.lean b/Mathlib/Order/Filter/SmallSets.lean index a1f6de7f901b5..6ef388c936376 100644 --- a/Mathlib/Order/Filter/SmallSets.lean +++ b/Mathlib/Order/Filter/SmallSets.lean @@ -42,6 +42,14 @@ theorem smallSets_eq_generate {f : Filter α} : f.smallSets = generate (powerset rfl #align filter.small_sets_eq_generate Filter.smallSets_eq_generate +-- TODO: get more properties from the adjunction? +-- TODO: is there a general way to get a lower adjoint for the lift of an upper adjoint? +theorem bind_smallSets_gc : + GaloisConnection (fun L : Filter (Set α) ↦ L.bind principal) smallSets := by + intro L l + simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff] + rfl + protected theorem HasBasis.smallSets {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) : HasBasis l.smallSets p fun i => 𝒫 s i := h.lift' monotone_powerset @@ -114,6 +122,11 @@ theorem smallSets_principal (s : Set α) : (𝓟 s).smallSets = 𝓟 (𝒫 s) := lift'_principal monotone_powerset #align filter.small_sets_principal Filter.smallSets_principal +theorem smallSets_comap_eq_comap_image (l : Filter β) (f : α → β) : + (comap f l).smallSets = comap (image f) l.smallSets := by + refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_ + simp [Function.comp, map_bind, bind_map] + theorem smallSets_comap (l : Filter β) (f : α → β) : (comap f l).smallSets = l.lift' (powerset ∘ preimage f) := comap_lift'_eq2 monotone_powerset diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean index 91496c9fcbfd5..76170df7b1c84 100644 --- a/Mathlib/Order/WellFoundedSet.lean +++ b/Mathlib/Order/WellFoundedSet.lean @@ -304,8 +304,7 @@ theorem PartiallyWellOrderedOn.image_of_monotone_on (hs : s.PartiallyWellOrdered (hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) : (f '' s).PartiallyWellOrderedOn r' := by intro g' hg' choose g hgs heq using hg' - obtain rfl : f ∘ g = g' - · exact funext heq + obtain rfl : f ∘ g = g' := funext heq obtain ⟨m, n, hlt, hmn⟩ := hs g hgs exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩ #align set.partially_well_ordered_on.image_of_monotone_on Set.PartiallyWellOrderedOn.image_of_monotone_on diff --git a/Mathlib/RingTheory/Artinian.lean b/Mathlib/RingTheory/Artinian.lean index 6baa266c4b4c8..fc0042073d43c 100644 --- a/Mathlib/RingTheory/Artinian.lean +++ b/Mathlib/RingTheory/Artinian.lean @@ -490,16 +490,16 @@ variable (S : Submonoid R) (L : Type*) [CommRing L] [Algebra R L] [IsLocalizatio theorem localization_surjective : Function.Surjective (algebraMap R L) := by intro r' obtain ⟨r₁, s, rfl⟩ := IsLocalization.mk'_surjective S r' - obtain ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r - swap - · exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩ - obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R) - use r - rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr - apply_fun algebraMap R L at hr - simp only [map_mul] at hr - rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one, Submonoid.coe_one, - ← (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul] + -- TODO: can `rsuffices` be used to move the `exact` below before the proof of this `obtain`? + obtain ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r := by + obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R) + use r + rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr + apply_fun algebraMap R L at hr + simp only [map_mul] at hr + rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one, + Submonoid.coe_one, ← (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul] + exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩ #align is_artinian_ring.localization_surjective IsArtinianRing.localization_surjective theorem localization_artinian : IsArtinianRing L := diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 94a2f0df9f554..2e5f85ce9d043 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -197,7 +197,9 @@ theorem discr_powerBasis_eq_prod'' [IsSeparable K L] (e : Fin pb.dim ≃ (L → rw [← Nat.cast_sum, ← @Finset.sum_range ℕ _ pb.dim fun i => i, sum_range_id] have hn : n = pb.dim := by rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim] - exact card_congr (Equiv.symm e) + -- FIXME: Without the `Fintype` namespace, why does it complain about `Finset.card_congr` being + -- deprecated? + exact Fintype.card_congr e.symm have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp have hle : 1 ≤ pb.dim := by diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean index b18805222edbd..32dabda3f1de1 100644 --- a/Mathlib/RingTheory/Ideal/Basic.lean +++ b/Mathlib/RingTheory/Ideal/Basic.lean @@ -778,7 +778,7 @@ theorem eq_bot_or_top : I = ⊥ ∨ I = ⊤ := by #align ideal.eq_bot_or_top Ideal.eq_bot_or_top variable (K) in -/-- A bijection between between (left) ideals of a division ring and `{0, 1}`, sending `⊥` to `0` +/-- A bijection between (left) ideals of a division ring and `{0, 1}`, sending `⊥` to `0` and `⊤` to `1`. -/ def equivFinTwo [DecidableEq (Ideal K)] : Ideal K ≃ Fin 2 where toFun := fun I ↦ if I = ⊥ then 0 else 1 diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean index c2f3cf69fe6d0..8ad89c8249436 100644 --- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean +++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean @@ -124,16 +124,13 @@ variable {R : Type u} {S : Type v} {F : Type w} [CommRing R] [Semiring S] theorem map_quotient_self (I : Ideal R) : map (Quotient.mk I) I = ⊥ := eq_bot_iff.2 <| Ideal.map_le_iff_le_comap.2 fun _ hx => - -- Porting note: Lean can't infer `Module (R ⧸ I) (R ⧸ I)` on its own - (@Submodule.mem_bot (R ⧸ I) _ _ _ Semiring.toModule _).2 <| - Ideal.Quotient.eq_zero_iff_mem.2 hx + (Submodule.mem_bot (R ⧸ I)).2 <| Ideal.Quotient.eq_zero_iff_mem.2 hx #align ideal.map_quotient_self Ideal.map_quotient_self @[simp] theorem mk_ker {I : Ideal R} : ker (Quotient.mk I) = I := by ext - rw [ker, mem_comap, @Submodule.mem_bot _ _ _ _ Semiring.toModule _, - Quotient.eq_zero_iff_mem] + rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem] #align ideal.mk_ker Ideal.mk_ker theorem map_mk_eq_bot_of_le {I J : Ideal R} (h : I ≤ J) : I.map (Quotient.mk J) = ⊥ := by @@ -173,7 +170,7 @@ lemma ker_Pi_Quotient_mk {ι : Type*} (I : ι → Ideal R) : @[simp] theorem bot_quotient_isMaximal_iff (I : Ideal R) : (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal := ⟨fun hI => - @mk_ker _ _ I ▸ + mk_ker (I := I) ▸ comap_isMaximal_of_surjective (Quotient.mk I) Quotient.mk_surjective (K := ⊥) (H := hI), fun hI => by letI := Quotient.field I @@ -426,10 +423,9 @@ theorem kerLiftAlg_toRingHom (f : A →ₐ[R₁] B) : rfl #align ideal.ker_lift_alg_to_ring_hom Ideal.kerLiftAlg_toRingHom --- Porting note: short circuit tc synth and use unification (_) /-- The induced algebra morphism from the quotient by the kernel is injective. -/ theorem kerLiftAlg_injective (f : A →ₐ[R₁] B) : Function.Injective (kerLiftAlg f) := - @RingHom.kerLift_injective A B (_) (_) f + RingHom.kerLift_injective (R := A) (S := B) f #align ideal.ker_lift_alg_injective Ideal.kerLiftAlg_injective /-- The **first isomorphism** theorem for algebras, computable version. -/ @@ -885,7 +881,7 @@ theorem coe_liftSupQuotQuotMkₐ : ⇑(liftSupQuotQuotMkₐ R I J) = liftSupQuot /-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where `I ≤ J`, this is the Third Isomorphism Theorem (see `DoubleQuot.quotQuotEquivQuotOfLE`). -/ def quotQuotEquivQuotSupₐ : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ I ⊔ J := - @AlgEquiv.ofRingEquiv R _ _ _ _ _ _ _ (quotQuotEquivQuotSup I J) fun _ => rfl + AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotSup I J) fun _ => rfl #align double_quot.quot_quot_equiv_quot_supₐ DoubleQuot.quotQuotEquivQuotSupₐ @[simp] @@ -918,7 +914,7 @@ theorem coe_quotQuotEquivQuotSupₐ_symm : where `J'` (resp. `I'`) is the projection of `J` in `A / I` (resp. `I` in `A / J`). -/ def quotQuotEquivCommₐ : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] (A ⧸ J) ⧸ I.map (Quotient.mkₐ R J) := - @AlgEquiv.ofRingEquiv R _ _ _ _ _ _ _ (quotQuotEquivComm I J) fun _ => rfl + AlgEquiv.ofRingEquiv (f := quotQuotEquivComm I J) fun _ => rfl #align double_quot.quot_quot_equiv_commₐ DoubleQuot.quotQuotEquivCommₐ @[simp] @@ -957,7 +953,7 @@ variable {I J} /-- The **third isomorphism theorem** for algebras. See `quotQuotEquivQuotSupₐ` for version that does not assume an inclusion of ideals. -/ def quotQuotEquivQuotOfLEₐ (h : I ≤ J) : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ J := - @AlgEquiv.ofRingEquiv R _ _ _ _ _ _ _ (quotQuotEquivQuotOfLE h) fun _ => rfl + AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotOfLE h) fun _ => rfl #align double_quot.quot_quot_equiv_quot_of_leₐ DoubleQuot.quotQuotEquivQuotOfLEₐ @[simp] diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index f17094f0bf50a..27bed71b84423 100644 --- a/Mathlib/RingTheory/IntegralDomain.lean +++ b/Mathlib/RingTheory/IntegralDomain.lean @@ -198,19 +198,7 @@ theorem card_fiber_eq_of_mem_range {H : Type*} [Group H] [DecidableEq H] (f : G (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by rcases hx with ⟨x, rfl⟩ rcases hy with ⟨y, rfl⟩ - refine card_congr (fun g _ => g * x⁻¹ * y) ?_ ?_ fun g hg => ⟨g * y⁻¹ * x, ?_⟩ - · simp (config := { contextual := true }) only [*, mem_filter, one_mul, MonoidHom.map_mul, - mem_univ, mul_right_inv, eq_self_iff_true, MonoidHom.map_mul_inv, and_self_iff, - forall_true_iff] - -- Porting note: added the following `simp` - simp only [true_and, map_inv, mul_right_inv, one_mul, and_self, implies_true, forall_const] - · simp only [mul_left_inj, imp_self, forall₂_true_iff] - · simp only [true_and_iff, mem_filter, mem_univ] at hg - simp only [hg, mem_filter, one_mul, MonoidHom.map_mul, mem_univ, mul_right_inv, - eq_self_iff_true, exists_prop_of_true, MonoidHom.map_mul_inv, and_self_iff, - mul_inv_cancel_right, inv_mul_cancel_right] - -- Porting note: added the next line. It is weird! - simp only [map_inv, mul_right_inv, one_mul, and_self, exists_prop] + exact card_equiv (Equiv.mulRight (x⁻¹ * y)) (by simp [mul_inv_eq_one]) #align card_fiber_eq_of_mem_range card_fiber_eq_of_mem_range /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero. diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index 9dd1eafca5fb2..4c6e6b35cf728 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -952,13 +952,13 @@ theorem card_primitiveRoots {ζ : R} {k : ℕ} (h : IsPrimitiveRoot ζ k) : by_cases h0 : k = 0 · simp [h0] symm - refine Finset.card_congr (fun i _ => ζ ^ i) ?_ ?_ ?_ + refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_ · simp only [true_and_iff, and_imp, mem_filter, mem_range, mem_univ] rintro i - hi rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)] exact h.pow_of_coprime i hi.symm · simp only [true_and_iff, and_imp, mem_filter, mem_range, mem_univ] - rintro i j hi - hj - H + rintro i hi - j hj - H exact h.pow_inj hi hj H · simp only [exists_prop, true_and_iff, mem_filter, mem_range, mem_univ] intro ξ hξ diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean index f48426422a3b3..efb159577c745 100644 --- a/Mathlib/SetTheory/Cardinal/Finite.lean +++ b/Mathlib/SetTheory/Cardinal/Finite.lean @@ -256,7 +256,7 @@ theorem card_image_of_injective {α : Type u} {β : Type v} (f : α → β) (s : card_image_of_injOn (Set.injOn_of_injective h s) #align part_enat.card_image_of_injective PartENat.card_image_of_injective --- Should I keeep the 6 following lemmas ? +-- Should I keep the 6 following lemmas ? -- TODO: Add ofNat, zero, and one versions for simp confluence @[simp] theorem _root_.Cardinal.natCast_le_toPartENat_iff {n : ℕ} {c : Cardinal} : diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index 90c2b7ea75663..0c7ab3a59e949 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean @@ -1106,8 +1106,8 @@ variable [Infinite α] {α β'} theorem mk_perm_eq_self_power : #(Equiv.Perm α) = #α ^ #α := ((mk_equiv_le_embedding α α).trans (mk_embedding_le_arrow α α)).antisymm <| by suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by - obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) - · erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool, + obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by + erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool, lift_natCast, mul_two, add_eq_self (aleph0_le_mk α)] erw [← le_def, mk_arrow, lift_uzero, mk_bool, lift_natCast 2] at this rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq] diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 5661d2d8be209..ea26c65160cf5 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -112,6 +112,7 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter +import Mathlib.Tactic.Linter.AttributeInstanceIn import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint import Mathlib.Tactic.Linter.TextBased diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean index 7c82485e5f42a..7ed47b173dbb2 100644 --- a/Mathlib/Tactic/ComputeDegree.lean +++ b/Mathlib/Tactic/ComputeDegree.lean @@ -198,7 +198,7 @@ It returns * the name of the relation (`Eq` or `LE.le`), or else `.anonymous` if it's none of these. * either * `.inl zero`, `.inl one`, or `.inl many` if the polynomial in a numeral - * or `.inr` of the the head symbol of `f` + * or `.inr` of the head symbol of `f` * or `.inl .anonymous` if inapplicable * if it exists, whether the `rhs` is a metavariable * if the LHS is `coeff f d`, whether `d` is a metavariable diff --git a/Mathlib/Tactic/Linter.lean b/Mathlib/Tactic/Linter.lean index 25a25c423029f..91505839363db 100644 --- a/Mathlib/Tactic/Linter.lean +++ b/Mathlib/Tactic/Linter.lean @@ -7,5 +7,6 @@ This file is ignored by `Shake`: * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary. -/ +import Mathlib.Tactic.Linter.AttributeInstanceIn import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint diff --git a/Mathlib/Tactic/Linter/AttributeInstanceIn.lean b/Mathlib/Tactic/Linter/AttributeInstanceIn.lean new file mode 100644 index 0000000000000..dcea726b4dd3b --- /dev/null +++ b/Mathlib/Tactic/Linter/AttributeInstanceIn.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2024 Michael Rothgang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Rothgang, Damiano Testa +-/ + +import Lean.Elab.Command +import Lean.Linter.Util + +/-! +# Linter for `attribute instance in` declarations + +The syntax `attribute [instance] instName in` can be used to accidentally create a global instance. +This is **not** obvious from reading the code, and in fact happened twice during the port, +hence, we lint against it. + +*Example*: before this was discovered, `Mathlib/Topology/Category/TopCat/Basic.lean` +contained the following code: +``` +attribute [instance] ConcreteCategory.instFunLike in +instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where + coe f := f +``` +Despite the `in`, this makes `ConcreteCategory.instFunLike` a global instance. +-/ + +open Lean Elab Command + +namespace Mathlib.Linter + +/-- Lint on any occurrence `attribute [instance] name in` (possibly with priority or scoped): +these are a footgun, as they define *global* instances (despite the `in`). -/ +register_option linter.attributeInstanceIn : Bool := { + defValue := true + descr := "enable the attributeInstanceIn linter" +} + +namespace attributeInstanceLinter + +/-- Gets the value of the `linter.attributeInstanceIn` option. -/ +def getLinterAttributeInstanceIn (o : Options) : Bool := + Linter.getLinterValue linter.attributeInstanceIn o + +/-- Whether a syntax element is adding an `instance` attribute without a `local` modifier. -/ +def is_attribute_instance_in (stx : Syntax) : Bool := + match stx with + | `(command|attribute [instance] $_decl:ident in $_) => true + | `(command|attribute [instance $_priority] $_decl:ident in $_) => true + | _ => false + +/-- The `attributeInstanceLinter` linter flags any occurrence of `attribute [instance] name in`, +including scoped or with instance priority: despite the `in`, these define *global* instances, +which can be rather misleading. +Instead, remove the `in` or make this a `local instance` instead. +-/ +def attributeInstanceIn : Linter where run := withSetOptionIn fun stx => do + unless getLinterAttributeInstanceIn (← getOptions) do + return + if (← MonadState.get).messages.hasErrors then + return + if is_attribute_instance_in stx then + Linter.logLint linter.attributeInstanceIn stx[0] m! + "`attribute [instance] ... in` declarations are surprising:\n\ + they are **not** limited to the subsequent declaration, but define global instances\n\ + please remove the `in` or make this a `local instance` instead" + +initialize addLinter attributeInstanceIn + +end attributeInstanceLinter + +end Mathlib.Linter diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 64ee30a0e6d9e..ebc46f87135d9 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -63,7 +63,7 @@ private abbrev allowed_commands : HashSet String := except for the ones in `allowed_commands`. If `warningAsError` is `true`, then the linter logs an info (rather than a warning). -This means that CI will eventually fail on `#`-commands, but not stop it from continuing. +This means that CI will eventually fail on `#`-commands, but does not stop it from continuing. However, in order to avoid local clutter, when `warningAsError` is `false`, the linter logs a warning only for the `#`-commands that do not already emit a message. -/ diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean index 73bc43769f0af..f7d9372bcea4b 100644 --- a/Mathlib/Tactic/Positivity/Basic.lean +++ b/Mathlib/Tactic/Positivity/Basic.lean @@ -10,6 +10,7 @@ import Mathlib.Data.NNRat.Defs import Mathlib.Algebra.Order.Ring.Int import Mathlib.Data.Nat.Factorial.Basic import Mathlib.Data.Rat.Order +import Mathlib.Data.PNat.Defs import Mathlib.Tactic.Positivity.Core import Qq @@ -404,6 +405,15 @@ def evalNatSucc : PositivityExt where eval {u α} _zα _pα e := do pure (.positive q(Nat.succ_pos $a)) | _, _, _ => throwError "not Nat.succ" +/-- Extension for `PNat.val`. -/ +@[positivity PNat.val _] +def evalPNatVal : PositivityExt where eval {u α} _zα _pα e := do + match u, α, e with + | 0, ~q(ℕ), ~q(PNat.val $a) => + assertInstancesCommute + pure (.positive q(PNat.pos $a)) + | _, _, _ => throwError "not PNat.val" + /-- Extension for `Nat.factorial`. -/ @[positivity Nat.factorial _] def evalFactorial : PositivityExt where eval {u α} _ _ e := do diff --git a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean index d054b4a52047e..3e9ad46826607 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean @@ -360,7 +360,6 @@ variable [ContinuousMul M] lemma HasProd.of_nat_of_neg_add_one {f : ℤ → M} (hf₁ : HasProd (fun n : ℕ ↦ f n) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : HasProd f (m * m') := by - have hi₁ : Injective ((↑) : ℕ → ℤ) := @Int.ofNat.inj have hi₂ : Injective Int.negSucc := @Int.negSucc.inj have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) := by constructor @@ -368,7 +367,8 @@ lemma HasProd.of_nat_of_neg_add_one {f : ℤ → M} rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩ · rw [codisjoint_iff_le_sup] rintro (i | j) <;> simp - exact (hi₁.hasProd_range_iff.mpr hf₁).mul_isCompl this (hi₂.hasProd_range_iff.mpr hf₂) + exact (Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl + this (hi₂.hasProd_range_iff.mpr hf₂) #align has_sum.nonneg_add_neg HasSum.of_nat_of_neg_add_one -- deprecated 2024-03-04 diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean index f6fdbc6c695f1..77c6e2b41e983 100644 --- a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean +++ b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean @@ -369,8 +369,9 @@ theorem Antitone.map_limsSup_of_continuousAt {F : Filter R} [NeBot F] {f : R → lt_irrefl (F.liminf f) <| lt_of_le_of_lt (liminf_le_of_frequently_le (frequently_of_forall (fun r ↦ f_decr (maybe_bot r))) (bdd_above.isBoundedUnder f_decr)) H - obtain ⟨l, l_lt, h'l⟩ : ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ { x : R | f x < F.liminf f } - · apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H) + obtain ⟨l, l_lt, h'l⟩ : + ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ { x : R | f x < F.liminf f } := by + apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H) simpa [IsBot] using not_bot obtain ⟨m, l_m, m_lt⟩ : (Set.Ioo l F.limsSup).Nonempty := by contrapose! h' diff --git a/Mathlib/Topology/Algebra/UniformGroup.lean b/Mathlib/Topology/Algebra/UniformGroup.lean index 7a78ea68a6f54..5d419d7bdb8b8 100644 --- a/Mathlib/Topology/Algebra/UniformGroup.lean +++ b/Mathlib/Topology/Algebra/UniformGroup.lean @@ -591,8 +591,8 @@ variable {G} @[to_additive] instance Subgroup.isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTopology H] : IsClosed (H : Set G) := by - obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = {1} - · exact nhds_inter_eq_singleton_of_mem_discrete H.one_mem + obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = {1} := + nhds_inter_eq_singleton_of_mem_discrete H.one_mem have : (fun p : G × G => p.2 / p.1) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in apply isClosed_of_spaced_out this intro h h_in h' h'_in diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index 4c7d0d3598380..59d8021bf3dfb 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -647,9 +647,8 @@ theorem dense_compl_singleton_iff_not_open : · intro hd ho exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _) · refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_ - obtain rfl : U = {x} - · exact eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩ - · exact ho hU + obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩ + exact ho hU #align dense_compl_singleton_iff_not_open dense_compl_singleton_iff_not_open /-! diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index f01c266214ee0..235afaf164e74 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -558,8 +558,7 @@ theorem factors_prod_eq_basis_of_ne {x y : (π C (· ∈ s))} (h : y ≠ x) : rw [list_prod_apply (π C (· ∈ s)) y _] apply List.prod_eq_zero simp only [List.mem_map] - obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a - · contrapose! h; ext; apply h + obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply h cases hx : x.val a · rw [hx, ne_eq, Bool.not_eq_false] at ha refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩ diff --git a/Mathlib/Topology/Category/TopCat/Basic.lean b/Mathlib/Topology/Category/TopCat/Basic.lean index 7871e2ec59e5b..e4ba3bd9ae075 100644 --- a/Mathlib/Topology/Category/TopCat/Basic.lean +++ b/Mathlib/Topology/Category/TopCat/Basic.lean @@ -56,8 +56,9 @@ instance topologicalSpaceUnbundled (X : TopCat) : TopologicalSpace X := set_option linter.uppercaseLean3 false in #align Top.topological_space_unbundled TopCat.topologicalSpaceUnbundled +-- TODO(#13170): remove this global instance -- Porting note: cannot find a coercion to function otherwise -attribute [instance] ConcreteCategory.instFunLike in +attribute [instance] ConcreteCategory.instFunLike instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where coe f := f diff --git a/Mathlib/Topology/Compactness/Lindelof.lean b/Mathlib/Topology/Compactness/Lindelof.lean index f719cfa5c9a75..416d7b5c46ed4 100644 --- a/Mathlib/Topology/Compactness/Lindelof.lean +++ b/Mathlib/Topology/Compactness/Lindelof.lean @@ -392,7 +392,7 @@ theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis (b : ι · exact hs.isLindelof_biUnion fun i _ => hb' i · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _) -/--`Filter.coLindelof` is the filter generated by complements to Lindelöf sets. -/ +/-- `Filter.coLindelof` is the filter generated by complements to Lindelöf sets. -/ def Filter.coLindelof (X : Type*) [TopologicalSpace X] : Filter X := --`Filter.coLindelof` is the filter generated by complements to Lindelöf sets. ⨅ (s : Set X) (_ : IsLindelof s), 𝓟 sᶜ diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index fb9ea554fd042..6d980ea58836a 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -377,8 +377,8 @@ theorem IsPreconnected.preimage_of_isOpenMap [TopologicalSpace β] {f : α → (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) := fun u v hu hv hsuv hsu hsv => by replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf - obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty - · refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_ + obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by + refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_ · simpa only [hsf, image_union] using image_subset f hsuv · simpa only [image_preimage_inter] using hsu.image f · simpa only [image_preimage_inter] using hsv.image f @@ -390,8 +390,8 @@ theorem IsPreconnected.preimage_of_isClosedMap [TopologicalSpace β] {s : Set β (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) := isPreconnected_closed_iff.2 fun u v hu hv hsuv hsu hsv => by replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf - obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty - · refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_ + obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by + refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_ · simpa only [hsf, image_union] using image_subset f hsuv · simpa only [image_preimage_inter] using hsu.image f · simpa only [image_preimage_inter] using hsv.image f @@ -855,8 +855,8 @@ the components `π i`. See also `ContinuousMap.exists_lift_sigma` for a version theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpace (π i)] {f : α → Σ i, π i} (hf : Continuous f) : ∃ (i : ι) (g : α → π i), Continuous g ∧ f = Sigma.mk i ∘ g := by - obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) - · rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩ + obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by + rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩ exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩ rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩ refine ⟨i, g, ?_, rfl⟩ diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 9ac48714eed93..a17d2ac2fc83d 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -204,6 +204,14 @@ theorem DenseRange.quotient [Setoid X] [TopologicalSpace X] {f : Y → X} (hf : Quotient.surjective_Quotient_mk''.denseRange.comp hf continuous_coinduced_rng #align dense_range.quotient DenseRange.quotient +theorem continuous_map_of_le {α : Type*} [TopologicalSpace α] + {s t : Setoid α} (h : s ≤ t) : Continuous (Setoid.map_of_le h) := + continuous_coinduced_rng + +theorem continuous_map_sInf {α : Type*} [TopologicalSpace α] + {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : Continuous (Setoid.map_sInf h) := + continuous_coinduced_rng + instance {p : X → Prop} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (Subtype p) := ⟨bot_unique fun s _ => ⟨(↑) '' s, isOpen_discrete _, preimage_image_eq _ Subtype.val_injective⟩⟩ diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 946c3db978265..fb59876ab1b16 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -51,8 +51,8 @@ theorem eventually_nhdsWithin_iff {a : α} {s : Set α} {p : α → Prop} : #align eventually_nhds_within_iff eventually_nhdsWithin_iff theorem frequently_nhdsWithin_iff {z : α} {s : Set α} {p : α → Prop} : - (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s := by - simp only [Filter.Frequently, eventually_nhdsWithin_iff, not_and'] + (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s := + frequently_inf_principal.trans <| by simp only [and_comm] #align frequently_nhds_within_iff frequently_nhdsWithin_iff theorem mem_closure_ne_iff_frequently_within {z : α} {s : Set α} : @@ -387,12 +387,6 @@ theorem tendsto_nhds_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} h.mono_right nhdsWithin_le_nhds #align tendsto_nhds_of_tendsto_nhds_within tendsto_nhds_of_tendsto_nhdsWithin --- todo: move to `Mathlib.Filter.Order.Basic` or drop -theorem principal_subtype {α : Type*} (s : Set α) (t : Set s) : - 𝓟 t = comap (↑) (𝓟 (((↑) : s → α) '' t)) := by - rw [comap_principal, preimage_image_eq _ Subtype.coe_injective] -#align principal_subtype principal_subtype - theorem nhdsWithin_neBot_of_mem {s : Set α} {x : α} (hx : x ∈ s) : NeBot (𝓝[s] x) := mem_closure_iff_nhdsWithin_neBot.1 <| subset_closure hx #align nhds_within_ne_bot_of_mem nhdsWithin_neBot_of_mem diff --git a/Mathlib/Topology/Defs/Basic.lean b/Mathlib/Topology/Defs/Basic.lean index e8516c1318543..431e8fbc2b67a 100644 --- a/Mathlib/Topology/Defs/Basic.lean +++ b/Mathlib/Topology/Defs/Basic.lean @@ -32,7 +32,7 @@ other than `Mathlib.Data.Set.Lattice`. * `interior s`: the *interior* of a set `s` is the maximal open set that is included in `s`. -* `closure s`: the *closure* of a set `s` is the minimal closed that that includes `s`. +* `closure s`: the *closure* of a set `s` is the minimal closed set that includes `s`. * `frontier s`: the *frontier* of a set is the set difference `closure s \ interior s`. A point `x` belongs to `frontier s`, if any neighborhood of `x` diff --git a/Mathlib/Topology/ExtremallyDisconnected.lean b/Mathlib/Topology/ExtremallyDisconnected.lean index 8fa0c7d6c54fc..c483ddd8d70bd 100644 --- a/Mathlib/Topology/ExtremallyDisconnected.lean +++ b/Mathlib/Topology/ExtremallyDisconnected.lean @@ -277,10 +277,14 @@ protected theorem CompactT2.ExtremallyDisconnected.projective [ExtremallyDisconn ext x exact x.val.mem.symm -protected theorem CompactT2.projective_iff_extremallyDisconnnected [CompactSpace A] [T2Space A] : +protected theorem CompactT2.projective_iff_extremallyDisconnected [CompactSpace A] [T2Space A] : Projective A ↔ ExtremallyDisconnected A := ⟨Projective.extremallyDisconnected, fun _ => ExtremallyDisconnected.projective⟩ +@[deprecated (since := "2024-05-26")] +alias CompactT2.projective_iff_extremallyDisconnnected := + CompactT2.projective_iff_extremallyDisconnected + end -- Note: It might be possible to use Gleason for this instead diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 82a4ac81f7b78..f895abdd541ed 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -646,9 +646,8 @@ theorem finset_sum_iSup_nat {α} {ι} [SemilatticeSup ι] {s : Finset α} {f : theorem mul_iSup {ι : Sort*} {f : ι → ℝ≥0∞} {a : ℝ≥0∞} : a * iSup f = ⨆ i, a * f i := by by_cases hf : ∀ i, f i = 0 - · obtain rfl : f = fun _ => 0 - · exact funext hf - · simp only [iSup_zero_eq_zero, mul_zero] + · obtain rfl : f = fun _ => 0 := funext hf + simp only [iSup_zero_eq_zero, mul_zero] · refine (monotone_id.const_mul' _).map_iSup_of_continuousAt ?_ (mul_zero a) refine ENNReal.Tendsto.const_mul tendsto_id (Or.inl ?_) exact mt iSup_eq_zero.1 hf diff --git a/Mathlib/Topology/Instances/RatLemmas.lean b/Mathlib/Topology/Instances/RatLemmas.lean index 8e37fb439a073..5b7506a863b79 100644 --- a/Mathlib/Topology/Instances/RatLemmas.lean +++ b/Mathlib/Topology/Instances/RatLemmas.lean @@ -57,8 +57,8 @@ theorem not_countably_generated_cocompact : ¬IsCountablyGenerated (cocompact intro H rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩ rw [tendsto_inf] at hx; rcases hx with ⟨hxc, hx0⟩ - obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) - · exact (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists + obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) := + (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists exact hn (Or.inr ⟨n, rfl⟩) #align rat.not_countably_generated_cocompact Rat.not_countably_generated_cocompact diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean index 595d8f76e81c0..a98359393d409 100644 --- a/Mathlib/Topology/Irreducible.lean +++ b/Mathlib/Topology/Irreducible.lean @@ -308,8 +308,8 @@ theorem IsPreirreducible.subset_irreducible {S U : Set X} (ht : IsPreirreducible replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩ refine ⟨⟨z, h₁ hz⟩, ?_⟩ rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩ - obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) - · refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_ + obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) := by + refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_ · simp [*] · intro U H simp only [Finset.mem_insert, Finset.mem_singleton] at H diff --git a/Mathlib/Topology/MetricSpace/Algebra.lean b/Mathlib/Topology/MetricSpace/Algebra.lean index 45325a41e2a30..49df2826ba8f5 100644 --- a/Mathlib/Topology/MetricSpace/Algebra.lean +++ b/Mathlib/Topology/MetricSpace/Algebra.lean @@ -152,8 +152,8 @@ instance (priority := 100) BoundedSMul.continuousSMul : ContinuousSMul α β whe continuous_smul := by rw [Metric.continuous_iff] rintro ⟨a, b⟩ ε ε0 - obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε - · have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by continuity + obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε := by + have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by continuity refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt simp refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩ diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index fe2737180aa63..65d977e9911f4 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -191,12 +191,11 @@ instance tendstoIccClassNhdsPi {ι : Type*} {α : ι → Type*} [∀ i, Preorder TendstoIxxClass Icc (𝓝 f) (𝓝 f) := by constructor conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi] - simp only [smallSets_iInf, smallSets_comap, tendsto_iInf, tendsto_lift', (· ∘ ·), - mem_powerset_iff] - intro i s hs + simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff] + intro i have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f - refine' (tendsto_lift'.1 ((this.comp tendsto_fst).Icc (this.comp tendsto_snd)) s hs).mono _ - exact fun p hp g hg => hp ⟨hg.1 _, hg.2 _⟩ + refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_ + filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩ #align tendsto_Icc_class_nhds_pi tendstoIccClassNhdsPi -- Porting note (#10756): new lemma diff --git a/Mathlib/Topology/Order/IntermediateValue.lean b/Mathlib/Topology/Order/IntermediateValue.lean index caab767f5f178..02b402f45d8b2 100644 --- a/Mathlib/Topology/Order/IntermediateValue.lean +++ b/Mathlib/Topology/Order/IntermediateValue.lean @@ -69,10 +69,9 @@ variable {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [Topol on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` we have `f x = g x`. -/ theorem intermediate_value_univ₂ [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) : ∃ x, f x = g x := by - obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty - · exact - isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg) - (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩ + obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty := + isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg) + (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩ exact ⟨x, le_antisymm hfg hgf⟩ #align intermediate_value_univ₂ intermediate_value_univ₂ diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 85163c4a00036..b4f55507462cb 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -83,6 +83,7 @@ occasionally the literature swaps definitions for e.g. T₃ and regular. it is a `TotallySeparatedSpace`. * `loc_compact_t2_tot_disc_iff_tot_sep`: A locally compact T₂ space is totally disconnected iff it is totally separated. +* `t2Quotient`: the largest T2 quotient of a given topological space. If the space is also compact: @@ -1463,49 +1464,6 @@ theorem Set.InjOn.exists_isOpen_superset {X Y : Type*} [TopologicalSpace X] [Top let ⟨u, huo, hsu, hut⟩ := mem_nhdsSet_iff_exists.1 hst ⟨u, huo, hsu, ht.mono hut⟩ -/-- A T₂.₅ space, also known as a Urysohn space, is a topological space - where for every pair `x ≠ y`, there are two open sets, with the intersection of closures - empty, one containing `x` and the other `y` . -/ -class T25Space (X : Type u) [TopologicalSpace X] : Prop where - /-- Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are - disjoint. -/ - t2_5 : ∀ ⦃x y : X⦄, x ≠ y → Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) -#align t2_5_space T25Space - -@[simp] -theorem disjoint_lift'_closure_nhds [T25Space X] {x y : X} : - Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y := - ⟨fun h hxy => by simp [hxy, nhds_neBot.ne] at h, fun h => T25Space.t2_5 h⟩ -#align disjoint_lift'_closure_nhds disjoint_lift'_closure_nhds - --- see Note [lower instance priority] -instance (priority := 100) T25Space.t2Space [T25Space X] : T2Space X := - t2Space_iff_disjoint_nhds.2 fun _ _ hne => - (disjoint_lift'_closure_nhds.2 hne).mono (le_lift'_closure _) (le_lift'_closure _) -#align t2_5_space.t2_space T25Space.t2Space - -theorem exists_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) : - ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t) := - ((𝓝 x).basis_sets.lift'_closure.disjoint_iff (𝓝 y).basis_sets.lift'_closure).1 <| - disjoint_lift'_closure_nhds.2 h -#align exists_nhds_disjoint_closure exists_nhds_disjoint_closure - -theorem exists_open_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) : - ∃ u : Set X, - x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v) := by - simpa only [exists_prop, and_assoc] using - ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1 - (disjoint_lift'_closure_nhds.2 h) -#align exists_open_nhds_disjoint_closure exists_open_nhds_disjoint_closure - -theorem T25Space.of_injective_continuous [TopologicalSpace Y] [T25Space Y] {f : X → Y} - (hinj : Injective f) (hcont : Continuous f) : T25Space X where - t2_5 x y hne := (tendsto_lift'_closure_nhds hcont x).disjoint (t2_5 <| hinj.ne hne) - (tendsto_lift'_closure_nhds hcont y) - -instance [T25Space X] {p : X → Prop} : T25Space {x // p x} := - .of_injective_continuous Subtype.val_injective continuous_subtype_val - section limUnder variable [T2Space X] {f : Filter X} @@ -1667,6 +1625,87 @@ instance Sigma.t2Space {ι} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [ exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h #align sigma.t2_space Sigma.t2Space +section +variable (X) + +/-- The smallest equivalence relation on a topological space giving a T2 quotient. -/ +def t2Setoid : Setoid X := sInf {s | T2Space (Quotient s)} + +/-- The largest T2 quotient of a topological space. This construction is left-adjoint to the +inclusion of T2 spaces into all topological spaces. -/ +def t2Quotient := Quotient (t2Setoid X) + +namespace t2Quotient +variable {X} + +instance : TopologicalSpace (t2Quotient X) := + inferInstanceAs <| TopologicalSpace (Quotient _) + +/-- The map from a topological space to its largest T2 quotient. -/ +def mk : X → t2Quotient X := Quotient.mk (t2Setoid X) + +lemma mk_eq {x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s.Rel x y := + Setoid.quotient_mk_sInf_eq + +variable (X) + +lemma surjective_mk : Surjective (mk : X → t2Quotient X) := surjective_quotient_mk _ + +lemma continuous_mk : Continuous (mk : X → t2Quotient X) := + continuous_quotient_mk' + +variable {X} + +@[elab_as_elim] +protected lemma inductionOn {motive : t2Quotient X → Prop} (q : t2Quotient X) + (h : ∀ x, motive (t2Quotient.mk x)) : motive q := Quotient.inductionOn q h + +@[elab_as_elim] +protected lemma inductionOn₂ [TopologicalSpace Y] {motive : t2Quotient X → t2Quotient Y → Prop} + (q : t2Quotient X) (q' : t2Quotient Y) (h : ∀ x y, motive (mk x) (mk y)) : motive q q' := + Quotient.inductionOn₂ q q' h + +/-- The largest T2 quotient of a topological space is indeed T2. -/ +instance : T2Space (t2Quotient X) := by + rw [t2Space_iff] + rintro ⟨x⟩ ⟨y⟩ (h : ¬ t2Quotient.mk x = t2Quotient.mk y) + obtain ⟨s, hs, hsxy⟩ : ∃ s, T2Space (Quotient s) ∧ Quotient.mk s x ≠ Quotient.mk s y := by + simpa [t2Quotient.mk_eq] using h + exact separated_by_continuous (continuous_map_sInf (by exact hs)) hsxy + +lemma compatible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] + {f : X → Y} (hf : Continuous f) : letI _ := t2Setoid X + ∀ (a b : X), a ≈ b → f a = f b := by + change t2Setoid X ≤ Setoid.ker f + exact sInf_le <| .of_injective_continuous + (Setoid.ker_lift_injective _) (hf.quotient_lift fun _ _ ↦ id) + +/-- The universal property of the largest T2 quotient of a topological space `X`: any continuous +map from `X` to a T2 space `Y` uniquely factors through `t2Quotient X`. This declaration builds the +factored map. Its continuity is `t2Quotient.continuous_lift`, the fact that it indeed factors the +original map is `t2Quotient.lift_mk` and uniquenes is `t2Quotient.unique_lift`. -/ +def lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] + {f : X → Y} (hf : Continuous f) : t2Quotient X → Y := + Quotient.lift f (t2Quotient.compatible hf) + +lemma continuous_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] + {f : X → Y} (hf : Continuous f) : Continuous (t2Quotient.lift hf) := + continuous_coinduced_dom.mpr hf + +@[simp] +lemma lift_mk {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] + {f : X → Y} (hf : Continuous f) (x : X) : lift hf (mk x) = f x := + Quotient.lift_mk (s := t2Setoid X) f (t2Quotient.compatible hf) x + +lemma unique_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] + {f : X → Y} (hf : Continuous f) {g : t2Quotient X → Y} (hfg : g ∘ mk = f) : + g = lift hf := by + apply surjective_mk X |>.right_cancellable |>.mp <| funext _ + simp [← hfg] + +end t2Quotient +end + variable {Z : Type*} [TopologicalSpace Y] [TopologicalSpace Z] theorem isClosed_eq [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) : @@ -2097,6 +2136,53 @@ theorem locally_compact_of_compact [T2Space X] [CompactSpace X] : end LocallyCompactRegularSpace +section T25 + +/-- A T₂.₅ space, also known as a Urysohn space, is a topological space + where for every pair `x ≠ y`, there are two open sets, with the intersection of closures + empty, one containing `x` and the other `y` . -/ +class T25Space (X : Type u) [TopologicalSpace X] : Prop where + /-- Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are + disjoint. -/ + t2_5 : ∀ ⦃x y : X⦄, x ≠ y → Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) +#align t2_5_space T25Space + +@[simp] +theorem disjoint_lift'_closure_nhds [T25Space X] {x y : X} : + Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y := + ⟨fun h hxy => by simp [hxy, nhds_neBot.ne] at h, fun h => T25Space.t2_5 h⟩ +#align disjoint_lift'_closure_nhds disjoint_lift'_closure_nhds + +-- see Note [lower instance priority] +instance (priority := 100) T25Space.t2Space [T25Space X] : T2Space X := + t2Space_iff_disjoint_nhds.2 fun _ _ hne => + (disjoint_lift'_closure_nhds.2 hne).mono (le_lift'_closure _) (le_lift'_closure _) +#align t2_5_space.t2_space T25Space.t2Space + +theorem exists_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) : + ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t) := + ((𝓝 x).basis_sets.lift'_closure.disjoint_iff (𝓝 y).basis_sets.lift'_closure).1 <| + disjoint_lift'_closure_nhds.2 h +#align exists_nhds_disjoint_closure exists_nhds_disjoint_closure + +theorem exists_open_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) : + ∃ u : Set X, + x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v) := by + simpa only [exists_prop, and_assoc] using + ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1 + (disjoint_lift'_closure_nhds.2 h) +#align exists_open_nhds_disjoint_closure exists_open_nhds_disjoint_closure + +theorem T25Space.of_injective_continuous [TopologicalSpace Y] [T25Space Y] {f : X → Y} + (hinj : Injective f) (hcont : Continuous f) : T25Space X where + t2_5 x y hne := (tendsto_lift'_closure_nhds hcont x).disjoint (t2_5 <| hinj.ne hne) + (tendsto_lift'_closure_nhds hcont y) + +instance [T25Space X] {p : X → Prop} : T25Space {x // p x} := + .of_injective_continuous Subtype.val_injective continuous_subtype_val + +section T25 + section T3 /-- A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and @@ -2387,12 +2473,12 @@ theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : -- closed sets. If we can show that our intersection is a subset of any of these we can then -- "descend" this to show that it is a subset of either a or b. rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩ - obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v - /- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that - `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods of - `X` disjoint to it, but a finite intersection of clopen sets is clopen so we let this be our - `s`. -/ - · have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty + obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v := by + /- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that + `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods + of `X` disjoint to it, but a finite intersection of clopen sets is clopen, + so we let this be our `s`. -/ + have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1 rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1 cases' H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv) diff --git a/Mathlib/Topology/Sequences.lean b/Mathlib/Topology/Sequences.lean index 586457584e0c0..a48d4472d306b 100644 --- a/Mathlib/Topology/Sequences.lean +++ b/Mathlib/Topology/Sequences.lean @@ -143,8 +143,8 @@ theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto refine ⟨fun s x hcx => ?_⟩ by_cases hx : x ∈ s; · exact subset_seqClosure hx - · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s - · simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop, + · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by + simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop, ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true, not_true_eq_false] using h (· ∉ s) x rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩ @@ -290,10 +290,10 @@ protected theorem IsSeqCompact.totallyBounded (h : IsSeqCompact s) : TotallyBoun obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V := by simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h - refine' ⟨u, u_in, fun x _ φ hφ huφ => _⟩ - obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V - · exact huφ.cauchySeq.mem_entourage V_in - · exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl) + refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩ + obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V := + huφ.cauchySeq.mem_entourage V_in + exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl) #align is_seq_compact.totally_bounded IsSeqCompact.totallyBounded variable [IsCountablyGenerated (𝓤 X)] @@ -324,8 +324,8 @@ protected theorem IsSeqCompact.isComplete (hs : IsSeqCompact s) : IsComplete s : ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩ rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩ refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩ - obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) - · exact ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists + obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) := + ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩ exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩ #align is_seq_compact.is_complete IsSeqCompact.isComplete diff --git a/Mathlib/Topology/Sheaves/Skyscraper.lean b/Mathlib/Topology/Sheaves/Skyscraper.lean index 93ae761a4ef13..fc2522a329a02 100644 --- a/Mathlib/Topology/Sheaves/Skyscraper.lean +++ b/Mathlib/Topology/Sheaves/Skyscraper.lean @@ -390,6 +390,8 @@ instance [HasColimits C] : (skyscraperPresheafFunctor p₀ : C ⥤ Presheaf C X) (skyscraperPresheafStalkAdjunction _).isRightAdjoint instance [HasColimits C] : (Presheaf.stalkFunctor C p₀).IsLeftAdjoint := + -- Use a classical instance instead of the one from `variable`s + have : ∀ U : Opens X, Decidable (p₀ ∈ U) := fun _ ↦ Classical.dec _ (skyscraperPresheafStalkAdjunction _).isLeftAdjoint /-- Taking stalks of a sheaf is the left adjoint functor to `skyscraperSheafFunctor` diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index ef9d9ef9afe54..c4c4edc176bb0 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/Mathlib/Topology/TietzeExtension.lean @@ -316,10 +316,10 @@ theorem exists_extension_forall_exists_le_ge_of_closedEmbedding [Nonempty X] (f ∃ g : Y →ᵇ ℝ, (∀ y, ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ g ∘ e = f := by inhabit X -- Put `a = ⨅ x, f x` and `b = ⨆ x, f x` - obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a - · exact ⟨_, isGLB_ciInf (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1⟩ - obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b - · exact ⟨_, isLUB_ciSup (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).2⟩ + obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := + ⟨_, isGLB_ciInf (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1⟩ + obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b := + ⟨_, isLUB_ciSup (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).2⟩ -- Then `f x ∈ [a, b]` for all `x` have hmem : ∀ x, f x ∈ Icc a b := fun x => ⟨ha.1 ⟨x, rfl⟩, hb.1 ⟨x, rfl⟩⟩ -- Rule out the trivial case `a = b` diff --git a/scripts/lint_hash_commands.sh b/scripts/lint_hash_commands.sh deleted file mode 100755 index 235452a1da169..0000000000000 --- a/scripts/lint_hash_commands.sh +++ /dev/null @@ -1,57 +0,0 @@ -#!/usr/bin/env bash - -## Usage: -## From the command-line, run `./Mathlib/lint_hash_commands.sh` or -## `./Mathlib/lint_hash_commands.sh anything` if you want a progress report. -## It runs Lean on a file with `import Mathlib`, so it is a good idea to have -## working `.olean`s. -## -## The output is a list of locations in `Mathlib/*.lean` files beginning with -## `<#cmd>`, where `<#cmd>` is a command beginning with `#`. -## -## *The script does *not* create new files nor does it modify/erase existing ones.* - -## create a list of all the `#`-commands -getHashCommands () { - printf $'import Mathlib\n#help command\n' | - lake env lean --stdin | - sed -n 's=^syntax "\(#[^"]*\)".*=^\1=p' | - grep -v "#align$" | - grep -v "#align_import$" | - grep -v "#noalign$" | - grep -v "#adaptation_note$" | - sort -u | tr '\n' , | - sed 's=$=^#eval=' -} - -## scans all the files in `Mathlib/*.lean` looking for lines that -## * begin with `#cmd`, where `#cmd` is an output of `getHashCommands`; -## * are not inside a comment block. -awk -v csvcmds="$( getHashCommands )" \ - -v con=$( git ls-files 'Mathlib/*.lean' | wc -l ) \ - -v verbose="${1}" \ - 'function perr(errMsg) { print errMsg | "cat >&2"; close("cat >&2") } - BEGIN{ - incomment=0 - split(csvcmds, cmds, ",") - msg="" - if(verbose != "") { print "Sniffing `#`-commands" } - } - ## lines that begin with `/-` are labeled as `incomment` - /^\/-/ { incomment=1 } - ## lines that contain `-/` are labeled as not `incomment` - /-\// { incomment=0 } - ## lines that begin with `#` and are not `incomment` get processed - (/^#/ && incomment == "0") { - for(cmd in cmds) { if ($0 ~ cmds[cmd]) { - msg=msg sprintf("%s:%s:%s\n", FILENAME, FNR, $0) } - } } - (FNR == 1) { - con-- - if(verbose != "" && con % 100 == 0) perr(sprintf("%5s files to go", con)) - } END{ - if (msg != "") { - printf("The following `#`-command should not be present:\n\n%s", msg) - exit 1 - } -}' $( git ls-files 'Mathlib/*.lean' ) diff --git a/scripts/noshake.json b/scripts/noshake.json index 14811f746ec4c..9b89f27db5dfb 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -227,7 +227,8 @@ ["Mathlib.Algebra.GroupPower.Order", "Mathlib.Algebra.Order.Group.PosPart", "Mathlib.Data.Int.CharZero", - "Mathlib.Data.Nat.Factorial.Basic"], + "Mathlib.Data.Nat.Factorial.Basic", + "Mathlib.Data.PNat.Defs"], "Mathlib.Tactic.NormNum.Ineq": ["Mathlib.Algebra.Order.Field.Defs", "Mathlib.Algebra.Order.Monoid.WithTop"], "Mathlib.Tactic.NormNum.BigOperators": ["Mathlib.Data.List.FinRange"], diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 6329c8f3804b5..28aa5fed28a51 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -124,5 +124,5 @@ Mathlib/Topology/ContinuousFunction/Bounded.lean : line 1 : ERR_NUM_LIN : 1800 f Mathlib/Topology/Instances/ENNReal.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1713 lines, try to split it up Mathlib/Topology/MetricSpace/PseudoMetric.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2098 lines, try to split it up Mathlib/Topology/PartialHomeomorph.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1513 lines, try to split it up -Mathlib/Topology/Separation.lean : line 1 : ERR_NUM_LIN : 2600 file contains 2512 lines, try to split it up +Mathlib/Topology/Separation.lean : line 1 : ERR_NUM_LIN : 2800 file contains 2621 lines, try to split it up Mathlib/Topology/UniformSpace/Basic.lean : line 1 : ERR_NUM_LIN : 2100 file contains 1996 lines, try to split it up diff --git a/test/attributeInstanceIn.lean b/test/attributeInstanceIn.lean new file mode 100644 index 0000000000000..3fe3f84182576 --- /dev/null +++ b/test/attributeInstanceIn.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2024 Michael Rothgang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Rothgang, Damiano Testa +-/ + +import Mathlib.Tactic.Linter.AttributeInstanceIn + +/-! Tests for the `attributeInstanceIn` linter. -/ + +-- Test disabling the linter. +set_option linter.attributeInstanceIn false + +set_option autoImplicit false in +attribute [instance] Int.add in +instance : Inhabited Int where + default := 0 + +set_option linter.attributeInstanceIn true + +set_option linter.attributeInstanceIn false in +attribute [instance] Int.add in +instance : Inhabited Int where + default := 0 + +-- Global instances with `in`, are linted, as they are a footgun. + +set_option linter.attributeInstanceIn false in +/-- +warning: `attribute [instance] ... in` declarations are surprising: +they are **not** limited to the subsequent declaration, but define global instances +please remove the `in` or make this a `local instance` instead +note: this linter can be disabled with `set_option linter.attributeInstanceIn false` +-/ +#guard_msgs in +set_option autoImplicit false in +set_option linter.attributeInstanceIn true in +attribute [instance 1100] Int.add in +set_option autoImplicit false in +instance : Inhabited Int where + default := 0 + +set_option linter.attributeInstanceIn false in +/-- +warning: `attribute [instance] ... in` declarations are surprising: +they are **not** limited to the subsequent declaration, but define global instances +please remove the `in` or make this a `local instance` instead +note: this linter can be disabled with `set_option linter.attributeInstanceIn false` +-/ +#guard_msgs in +set_option linter.attributeInstanceIn true in +attribute [instance] Int.add in +instance : Inhabited Int where + default := 0 + +#guard_msgs in +-- non-`instance` attributes are allowed with `in` +#guard_msgs in +attribute [simp] Int.add in +instance : Inhabited Int where + default := 0 + +-- Here's another example, with nested attributes. +def foo := True + +#guard_msgs in +-- TODO: where's the docBlame linter defined? what do I need to import? +--attribute [nolint docBlame] foo in +attribute [simp] foo in +def bar := False + +namespace X + +#guard_msgs in +-- `local instance` is allowed with `in` +attribute [local instance] Int.add in +instance : Inhabited Int where + default := 0 + +#guard_msgs in +-- `local instance priority` is allowed with `in` +attribute [local instance 42] Int.add in +instance : Inhabited Int where + default := 0 + +#guard_msgs in +-- `scoped instance` is allowed with `in` +attribute [scoped instance] Int.add in +instance : Inhabited Int where + default := 0 + +#guard_msgs in +-- `scoped instance priority` is allowed with `in` +attribute [scoped instance 42] Int.add in +instance : Inhabited Int where + default := 0 + +end X + +-- Omitting the `in` is also fine. + +attribute [local instance 42] foo + +-- Global instance without the `in` are also left alone. +attribute [instance 20000] foo + +namespace X + +attribute [scoped instance 0] foo diff --git a/test/positivity.lean b/test/positivity.lean index decca1cf3385c..5bedb0448d4b8 100644 --- a/test/positivity.lean +++ b/test/positivity.lean @@ -282,6 +282,7 @@ example : 0 ≤ max (-3 : ℤ) 5 := by positivity -- [OrderedSMul α β] {a : α} (ha : 0 < a) {b : β} (hb : 0 < b) : 0 ≤ a • b := by positivity example (n : ℕ) : 0 < n.succ := by positivity +example (n : ℕ+) : 0 < (↑n : ℕ) := by positivity example (n : ℕ) : 0 < n ! := by positivity example (n k : ℕ) : 0 < (n+1).ascFactorial k := by positivity