From 98740267311a24ae6a2fe792964006babfd6788e Mon Sep 17 00:00:00 2001 From: JovanGerb Date: Sun, 24 Mar 2024 09:17:19 +0000 Subject: [PATCH] style: remove redundant instance arguments (#11581) I removed some redundant instance arguments throughout Mathlib. To do this, I used VS Code's regex search. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/repeating.20instances.20from.20variable.20command I closed the previous PR for this and reopened it. --- Mathlib/Algebra/BigOperators/Basic.lean | 4 ++-- Mathlib/Algebra/CharP/Basic.lean | 2 +- Mathlib/Algebra/Group/Hom/Basic.lean | 2 +- Mathlib/Algebra/Group/NatPowAssoc.lean | 2 +- Mathlib/Algebra/Group/Units.lean | 2 +- .../Algebra/Module/Submodule/Localization.lean | 2 +- Mathlib/Algebra/Order/Group/Abs.lean | 2 +- Mathlib/Algebra/Order/Group/Lattice.lean | 2 +- Mathlib/Algebra/Order/Module/OrderedSMul.lean | 3 +-- Mathlib/Algebra/Order/Monoid/WithTop.lean | 2 +- Mathlib/Algebra/Star/Subalgebra.lean | 2 +- .../Analysis/InnerProductSpace/Projection.lean | 8 ++++---- Mathlib/Analysis/NormedSpace/Basic.lean | 4 +--- .../Abelian/ProjectiveResolution.lean | 2 +- .../CategoryTheory/Preadditive/Biproducts.lean | 2 +- .../Sites/Coherent/CoherentSheaves.lean | 2 +- .../Sites/Coherent/Equivalence.lean | 4 ++-- Mathlib/Data/DFinsupp/Multiset.lean | 2 +- Mathlib/Data/Finsupp/WellFounded.lean | 8 ++++---- Mathlib/Data/Fintype/Sigma.lean | 2 +- Mathlib/Data/Int/Order/Basic.lean | 2 +- Mathlib/Data/List/EditDistance/Estimator.lean | 3 +-- Mathlib/Data/Matrix/Basic.lean | 5 ++--- Mathlib/Data/Multiset/Basic.lean | 4 ++-- Mathlib/FieldTheory/Normal.lean | 2 +- Mathlib/GroupTheory/Exponent.lean | 9 ++++----- Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean | 2 +- Mathlib/GroupTheory/GroupAction/ConjAct.lean | 2 +- Mathlib/GroupTheory/Perm/ClosureSwap.lean | 2 +- Mathlib/GroupTheory/PushoutI.lean | 3 +-- Mathlib/LinearAlgebra/Dimension/Finite.lean | 6 +++--- .../LinearAlgebra/Dimension/Localization.lean | 2 +- Mathlib/LinearAlgebra/Dual.lean | 2 +- Mathlib/LinearAlgebra/SesquilinearForm.lean | 3 +-- .../Constructions/BorelSpace/Basic.lean | 2 +- .../Constructions/Projective.lean | 3 +-- Mathlib/MeasureTheory/Group/Measure.lean | 4 ++-- Mathlib/MeasureTheory/Measure/Count.lean | 2 +- Mathlib/MeasureTheory/Measure/Typeclasses.lean | 5 ++--- .../LegendreSymbol/MulCharacter.lean | 2 +- Mathlib/Order/Birkhoff.lean | 2 +- Mathlib/Order/Bounds/Basic.lean | 4 ++-- Mathlib/Order/Directed.lean | 2 +- Mathlib/Order/Hom/Bounded.lean | 2 -- Mathlib/Order/Monotone/Basic.lean | 2 -- .../ProbabilityMassFunction/Basic.lean | 2 +- .../RepresentationTheory/Action/Limits.lean | 6 ++---- .../RingTheory/Ideal/QuotientOperations.lean | 6 +++--- Mathlib/RingTheory/IntegralRestrict.lean | 5 ++--- Mathlib/RingTheory/RingInvo.lean | 6 +++--- Mathlib/RingTheory/SimpleModule.lean | 2 +- Mathlib/RingTheory/Subsemiring/Order.lean | 10 +++++----- Mathlib/RingTheory/TensorProduct/Basic.lean | 7 +++---- Mathlib/Topology/Algebra/Order/Compact.lean | 18 +++++++++--------- Mathlib/Topology/Compactness/SigmaCompact.lean | 2 +- .../Connected/TotallyDisconnected.lean | 4 ++-- Mathlib/Topology/Order.lean | 6 +++--- Mathlib/Topology/Order/ScottTopology.lean | 2 +- Mathlib/Topology/Separation.lean | 2 +- test/ComputeDegree.lean | 8 ++++---- test/Continuity.lean | 3 +-- test/fun_prop_dev.lean | 4 ++-- 62 files changed, 105 insertions(+), 124 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 6b8c28519f064..7b3c1cc4f9e60 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -2269,7 +2269,7 @@ lemma prod_of_injective (e : ι → κ) (he : Injective e) (f : ι → α) (g : prod_of_injOn e (he.injOn _) (by simp) (by simpa using h') (fun i _ ↦ h i) @[to_additive] -lemma prod_fiberwise [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : ι → α) : +lemma prod_fiberwise [DecidableEq κ] (g : ι → κ) (f : ι → α) : ∏ j, ∏ i : {i // g i = j}, f i = ∏ i, f i := by rw [← Finset.prod_fiberwise _ g f] congr with j @@ -2278,7 +2278,7 @@ lemma prod_fiberwise [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : ι → #align fintype.sum_fiberwise Fintype.sum_fiberwise @[to_additive] -lemma prod_fiberwise' [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : κ → α) : +lemma prod_fiberwise' [DecidableEq κ] (g : ι → κ) (f : κ → α) : ∏ j, ∏ _i : {i // g i = j}, f j = ∏ i, f (g i) := by rw [← Finset.prod_fiberwise' _ g f] congr with j diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean index c04dd956b1729..f788286c0eb6c 100644 --- a/Mathlib/Algebra/CharP/Basic.lean +++ b/Mathlib/Algebra/CharP/Basic.lean @@ -388,7 +388,7 @@ theorem ringChar_ne_zero_of_finite [Finite R] : ringChar R ≠ 0 := char_ne_zero_of_finite R (ringChar R) #align char_p.ring_char_ne_zero_of_finite CharP.ringChar_ne_zero_of_finite -theorem ringChar_zero_iff_CharZero [NonAssocRing R] : ringChar R = 0 ↔ CharZero R := by +theorem ringChar_zero_iff_CharZero : ringChar R = 0 ↔ CharZero R := by rw [ringChar.eq_iff, charP_zero_iff_charZero] end diff --git a/Mathlib/Algebra/Group/Hom/Basic.lean b/Mathlib/Algebra/Group/Hom/Basic.lean index 0e71ef56efac7..d5f712c672c35 100644 --- a/Mathlib/Algebra/Group/Hom/Basic.lean +++ b/Mathlib/Algebra/Group/Hom/Basic.lean @@ -190,7 +190,7 @@ lemma mul_comp [MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) : #align add_monoid_hom.add_comp AddMonoidHom.add_comp @[to_additive] -lemma comp_mul [CommMonoid N] [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) : +lemma comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by ext; simp only [mul_apply, Function.comp_apply, map_mul, coe_comp] #align monoid_hom.comp_mul MonoidHom.comp_mul diff --git a/Mathlib/Algebra/Group/NatPowAssoc.lean b/Mathlib/Algebra/Group/NatPowAssoc.lean index e9ed72df007bc..c740c99749ec2 100644 --- a/Mathlib/Algebra/Group/NatPowAssoc.lean +++ b/Mathlib/Algebra/Group/NatPowAssoc.lean @@ -95,7 +95,7 @@ section Monoid variable [Monoid M] -instance Monoid.PowAssoc [Monoid M] : NatPowAssoc M where +instance Monoid.PowAssoc : NatPowAssoc M where npow_add _ _ _ := pow_add _ _ _ npow_zero _ := pow_zero _ npow_one _ := pow_one _ diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean index 8b4563b8912f5..4fbbb7bf5f3e5 100644 --- a/Mathlib/Algebra/Group/Units.lean +++ b/Mathlib/Algebra/Group/Units.lean @@ -705,7 +705,7 @@ lemma IsUnit.exists_right_inv (h : IsUnit a) : ∃ b, a * b = 1 := by #align is_add_unit.exists_neg IsAddUnit.exists_neg @[to_additive IsAddUnit.exists_neg'] -lemma IsUnit.exists_left_inv [Monoid M] {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by +lemma IsUnit.exists_left_inv {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩ exact ⟨b, hba⟩ #align is_unit.exists_left_inv IsUnit.exists_left_inv diff --git a/Mathlib/Algebra/Module/Submodule/Localization.lean b/Mathlib/Algebra/Module/Submodule/Localization.lean index 31cdc1c184f11..120cf4b2b9b0e 100644 --- a/Mathlib/Algebra/Module/Submodule/Localization.lean +++ b/Mathlib/Algebra/Module/Submodule/Localization.lean @@ -30,7 +30,7 @@ open nonZeroDivisors universe u u' v v' variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'} -variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] +variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] variable (hp : p ≤ R⁰) diff --git a/Mathlib/Algebra/Order/Group/Abs.lean b/Mathlib/Algebra/Order/Group/Abs.lean index e521a4578c1bd..0ab53cb77a1f5 100644 --- a/Mathlib/Algebra/Order/Group/Abs.lean +++ b/Mathlib/Algebra/Order/Group/Abs.lean @@ -183,7 +183,7 @@ lemma inf_sq_eq_mul_div_mabs_div (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ -- See, e.g. Zaanen, Lectures on Riesz Spaces -- 3rd lecture @[to_additive] -lemma mabs_div_sup_mul_mabs_div_inf [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : +lemma mabs_div_sup_mul_mabs_div_inf (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ := by letI : DistribLattice α := CommGroup.toDistribLattice α calc diff --git a/Mathlib/Algebra/Order/Group/Lattice.lean b/Mathlib/Algebra/Order/Group/Lattice.lean index 0154e658cd5f0..e3b0a14e38b3c 100644 --- a/Mathlib/Algebra/Order/Group/Lattice.lean +++ b/Mathlib/Algebra/Order/Group/Lattice.lean @@ -93,7 +93,7 @@ lemma inf_div (a b c : α) : (a ⊓ b) / c = a / c ⊓ b / c := (OrderIso.divRig -- Chapter V, 1.E -- See also `one_le_pow_iff` for the existing version in linear orders @[to_additive] -lemma pow_two_semiclosed [CovariantClass α α (· * ·) (· ≤ ·)] +lemma pow_two_semiclosed [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a := by suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by rwa [← inf_eq_right, ← mul_right_eq_self] diff --git a/Mathlib/Algebra/Order/Module/OrderedSMul.lean b/Mathlib/Algebra/Order/Module/OrderedSMul.lean index 4f68e912343d4..a8564c4a5438f 100644 --- a/Mathlib/Algebra/Order/Module/OrderedSMul.lean +++ b/Mathlib/Algebra/Order/Module/OrderedSMul.lean @@ -65,8 +65,7 @@ instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where instance OrderedSMul.toPosSMulReflectLT : PosSMulReflectLT R M := PosSMulReflectLT.of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha -instance OrderDual.instOrderedSMul [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] - [OrderedSMul R M] : OrderedSMul R Mᵒᵈ where +instance OrderDual.instOrderedSMul : OrderedSMul R Mᵒᵈ where smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M) lt_of_smul_lt_smul_of_pos := OrderedSMul.lt_of_smul_lt_smul_of_pos (M := M) diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean index 203d185c5eab9..73a87dea118d4 100644 --- a/Mathlib/Algebra/Order/Monoid/WithTop.lean +++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean @@ -487,7 +487,7 @@ lemma one_eq_coe : 1 = (a : WithBot α) ↔ a = 1 := eq_comm.trans coe_eq_one @[to_additive (attr := simp)] lemma one_ne_bot : (1 : WithBot α) ≠ ⊥ := coe_ne_bot @[to_additive (attr := simp)] -theorem unbot_one [One α] : (1 : WithBot α).unbot coe_ne_bot = 1 := +theorem unbot_one : (1 : WithBot α).unbot coe_ne_bot = 1 := rfl #align with_bot.unbot_one WithBot.unbot_one #align with_bot.unbot_zero WithBot.unbot_zero diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean index 251ad32be1ec7..168d8dc84d8fe 100644 --- a/Mathlib/Algebra/Star/Subalgebra.lean +++ b/Mathlib/Algebra/Star/Subalgebra.lean @@ -745,7 +745,7 @@ theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (h DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial #align star_alg_hom.ext_of_adjoin_eq_top StarAlgHom.ext_of_adjoin_eq_top -theorem map_adjoin [StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A) : +theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) : map f (adjoin R s) = adjoin R (f '' s) := GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarSubalgebra.gc StarSubalgebra.gc fun _ => rfl diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 5bc756831413d..06dae0fb38d30 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -514,25 +514,25 @@ theorem eq_orthogonalProjection_of_mem_of_inner_eq_zero {u v : E} (hvm : v ∈ K /-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the orthogonal projection. -/ -theorem eq_orthogonalProjection_of_mem_orthogonal [HasOrthogonalProjection K] {u v : E} (hv : v ∈ K) +theorem eq_orthogonalProjection_of_mem_orthogonal {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) : (orthogonalProjection K u : E) = v := eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hv <| (Submodule.mem_orthogonal' _ _).1 hvo #align eq_orthogonal_projection_of_mem_orthogonal eq_orthogonalProjection_of_mem_orthogonal /-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the orthogonal projection. -/ -theorem eq_orthogonalProjection_of_mem_orthogonal' [HasOrthogonalProjection K] {u v z : E} +theorem eq_orthogonalProjection_of_mem_orthogonal' {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) : (orthogonalProjection K u : E) = v := eq_orthogonalProjection_of_mem_orthogonal hv (by simpa [hu] ) #align eq_orthogonal_projection_of_mem_orthogonal' eq_orthogonalProjection_of_mem_orthogonal' @[simp] -theorem orthogonalProjection_orthogonal_val [HasOrthogonalProjection K] (u : E) : +theorem orthogonalProjection_orthogonal_val (u : E) : (orthogonalProjection Kᗮ u : E) = u - orthogonalProjection K u := eq_orthogonalProjection_of_mem_orthogonal' (sub_orthogonalProjection_mem_orthogonal _) (K.le_orthogonal_orthogonal (orthogonalProjection K u).2) <| by simp -theorem orthogonalProjection_orthogonal [HasOrthogonalProjection K] (u : E) : +theorem orthogonalProjection_orthogonal (u : E) : orthogonalProjection Kᗮ u = ⟨u - orthogonalProjection K u, sub_orthogonalProjection_mem_orthogonal _⟩ := Subtype.eq <| orthogonalProjection_orthogonal_val _ diff --git a/Mathlib/Analysis/NormedSpace/Basic.lean b/Mathlib/Analysis/NormedSpace/Basic.lean index a92c6ffe47884..ead9d14784a08 100644 --- a/Mathlib/Analysis/NormedSpace/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Basic.lean @@ -49,6 +49,7 @@ attribute [inherit_doc NormedSpace] NormedSpace.norm_smul_le end Prio variable [NormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] +variable [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] -- see Note [lower instance priority] instance (priority := 100) NormedSpace.boundedSMul [NormedSpace 𝕜 E] : BoundedSMul 𝕜 E := @@ -68,9 +69,6 @@ theorem norm_zsmul [NormedSpace 𝕜 E] (n : ℤ) (x : E) : ‖n • x‖ = ‖( rw [← norm_smul, ← Int.smul_one_eq_coe, smul_assoc, one_smul] #align norm_zsmul norm_zsmul -variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] -variable [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] - theorem eventually_nhds_norm_smul_sub_lt (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) : ∀ᶠ y in 𝓝 x, ‖c • (y - x)‖ < ε := have : Tendsto (fun y ↦ ‖c • (y - x)‖) (𝓝 x) (𝓝 0) := diff --git a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean index 8b4a472ee6bf8..9b2f3253e265d 100644 --- a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean +++ b/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean @@ -59,7 +59,7 @@ section Abelian variable [Abelian C] -lemma exact₀ [Abelian C] {Z : C} (P : ProjectiveResolution Z) : +lemma exact₀ {Z : C} (P : ProjectiveResolution Z) : (ShortComplex.mk _ _ P.complex_d_comp_π_f_zero).Exact := ShortComplex.exact_of_g_is_cokernel _ P.isColimitCokernelCofork diff --git a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean index b85a551016029..1f8933d1d93f7 100644 --- a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean +++ b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean @@ -271,7 +271,7 @@ theorem biproduct.matrix_desc [Fintype K] {f : J → C} {g : K → C} simp [lift_desc] #align category_theory.limits.biproduct.matrix_desc CategoryTheory.Limits.biproduct.matrix_desc -variable [Finite K] [HasFiniteBiproducts C] +variable [Finite K] @[reassoc] theorem biproduct.matrix_map {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k) diff --git a/Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean b/Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean index 80d985a69c413..de2b805552be8 100644 --- a/Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean +++ b/Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean @@ -24,7 +24,7 @@ namespace CategoryTheory variable {C : Type*} [Category C] [Precoherent C] universe w in -lemma isSheaf_coherent [Precoherent C] (P : Cᵒᵖ ⥤ Type w) : +lemma isSheaf_coherent (P : Cᵒᵖ ⥤ Type w) : Presieve.IsSheaf (coherentTopology C) P ↔ (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → (X a ⟶ B)), EffectiveEpiFamily X π → (Presieve.ofArrows X π).IsSheafFor P) := by diff --git a/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean index d9c5a34aecbf4..6a61bfb193c12 100644 --- a/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean +++ b/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean @@ -44,7 +44,7 @@ theorem precoherent : Precoherent D where infer_instance · simpa using congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map) (h' b) -instance [EssentiallySmall C] [Precoherent C] : +instance [EssentiallySmall C] : Precoherent (SmallModel C) := (equivSmallModel C).precoherent /-- @@ -124,7 +124,7 @@ theorem preregular : Preregular D where e.functor.map i' ≫ e.counit.app _, ?_⟩ simpa using congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map) w -instance [EssentiallySmall C] [Preregular C] : +instance [EssentiallySmall C] : Preregular (SmallModel C) := (equivSmallModel C).preregular /-- diff --git a/Mathlib/Data/DFinsupp/Multiset.lean b/Mathlib/Data/DFinsupp/Multiset.lean index ed0f4287e391d..db5562fe25b71 100644 --- a/Mathlib/Data/DFinsupp/Multiset.lean +++ b/Mathlib/Data/DFinsupp/Multiset.lean @@ -124,7 +124,7 @@ namespace DFinsupp variable [DecidableEq α] {f g : Π₀ _a : α, ℕ} @[simp] -theorem toMultiset_toDFinsupp [DecidableEq α] (f : Π₀ _ : α, ℕ) : +theorem toMultiset_toDFinsupp (f : Π₀ _ : α, ℕ) : Multiset.toDFinsupp (DFinsupp.toMultiset f) = f := Multiset.equivDFinsupp.apply_symm_apply f #align dfinsupp.to_multiset_to_dfinsupp DFinsupp.toMultiset_toDFinsupp diff --git a/Mathlib/Data/Finsupp/WellFounded.lean b/Mathlib/Data/Finsupp/WellFounded.lean index e1c1ff2bc95f3..02bb2767ee97c 100644 --- a/Mathlib/Data/Finsupp/WellFounded.lean +++ b/Mathlib/Data/Finsupp/WellFounded.lean @@ -59,17 +59,17 @@ instance Lex.wellFoundedLT {α N} [LT α] [IsTrichotomous α (· < ·)] [hα : W variable (r) -theorem Lex.wellFounded_of_finite [IsStrictTotalOrder α r] [Finite α] [Zero N] +theorem Lex.wellFounded_of_finite [IsStrictTotalOrder α r] [Finite α] (hs : WellFounded s) : WellFounded (Finsupp.Lex r s) := InvImage.wf (@equivFunOnFinite α N _ _) (Pi.Lex.wellFounded r fun _ => hs) #align finsupp.lex.well_founded_of_finite Finsupp.Lex.wellFounded_of_finite -theorem Lex.wellFoundedLT_of_finite [LinearOrder α] [Finite α] [Zero N] [LT N] +theorem Lex.wellFoundedLT_of_finite [LinearOrder α] [Finite α] [LT N] [hwf : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N)) := ⟨Finsupp.Lex.wellFounded_of_finite (· < ·) hwf.1⟩ #align finsupp.lex.well_founded_lt_of_finite Finsupp.Lex.wellFoundedLT_of_finite -protected theorem wellFoundedLT [Zero N] [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N, ¬n < 0) : +protected theorem wellFoundedLT [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N, ¬n < 0) : WellFoundedLT (α →₀ N) := ⟨InvImage.wf toDFinsupp (DFinsupp.wellFoundedLT fun _ a => hbot a).wf⟩ #align finsupp.well_founded_lt Finsupp.wellFoundedLT @@ -79,7 +79,7 @@ instance wellFoundedLT' {N} [CanonicallyOrderedAddCommMonoid N] [WellFoundedLT N Finsupp.wellFoundedLT fun a => (zero_le a).not_lt #align finsupp.well_founded_lt' Finsupp.wellFoundedLT' -instance wellFoundedLT_of_finite [Finite α] [Zero N] [Preorder N] [WellFoundedLT N] : +instance wellFoundedLT_of_finite [Finite α] [Preorder N] [WellFoundedLT N] : WellFoundedLT (α →₀ N) := ⟨InvImage.wf equivFunOnFinite Function.wellFoundedLT.wf⟩ #align finsupp.well_founded_lt_of_finite Finsupp.wellFoundedLT_of_finite diff --git a/Mathlib/Data/Fintype/Sigma.lean b/Mathlib/Data/Fintype/Sigma.lean index d7a0649bf7a79..86e7cc21d635d 100644 --- a/Mathlib/Data/Fintype/Sigma.lean +++ b/Mathlib/Data/Fintype/Sigma.lean @@ -35,7 +35,7 @@ lemma Set.biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) : lemma Set.biInter_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) : ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesop -variable [Fintype ι] [Π i, Fintype (κ i)] +variable [Fintype ι] instance Sigma.instFintype : Fintype (Σ i, κ i) := ⟨univ.sigma fun _ ↦ univ, by simp⟩ instance PSigma.instFintype : Fintype (Σ' i, κ i) := .ofEquiv _ (Equiv.psigmaEquivSigma _).symm diff --git a/Mathlib/Data/Int/Order/Basic.lean b/Mathlib/Data/Int/Order/Basic.lean index bde423c7dc5f6..8cee62e721c4d 100644 --- a/Mathlib/Data/Int/Order/Basic.lean +++ b/Mathlib/Data/Int/Order/Basic.lean @@ -566,7 +566,7 @@ variable [NonAssocRing R] (n r : R) lemma bit1_mul : bit1 n * r = (2 : ℤ) • (n * r) + r := by rw [bit1, add_mul, bit0_mul, one_mul] #align bit1_mul bit1_mul -lemma mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by +lemma mul_bit1 {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r := by rw [bit1, mul_add, mul_bit0, mul_one] #align mul_bit1 mul_bit1 diff --git a/Mathlib/Data/List/EditDistance/Estimator.lean b/Mathlib/Data/List/EditDistance/Estimator.lean index 6335890f01e14..09e0f77eec85a 100644 --- a/Mathlib/Data/List/EditDistance/Estimator.lean +++ b/Mathlib/Data/List/EditDistance/Estimator.lean @@ -133,8 +133,7 @@ instance [∀ a : δ × ℕ, WellFoundedGT { x // x ≤ a }] : Estimator.fstInst (Thunk.mk fun _ => _) (Thunk.mk fun _ => _) (estimator' C xs ys) /-- The initial estimator for Levenshtein distances. -/ -instance [CanonicallyLinearOrderedAddCommMonoid δ] - (C : Levenshtein.Cost α β δ) (xs : List α) (ys : List β) : +instance (C : Levenshtein.Cost α β δ) (xs : List α) (ys : List β) : Bot (LevenshteinEstimator C xs ys) where bot := { inner := diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean index abec245c8fbbb..2291781447193 100644 --- a/Mathlib/Data/Matrix/Basic.lean +++ b/Mathlib/Data/Matrix/Basic.lean @@ -1272,12 +1272,11 @@ theorem scalar_inj [Nonempty n] {r s : α} : scalar n r = scalar n s ↔ r = s : (diagonal_injective.comp Function.const_injective).eq_iff #align matrix.scalar_inj Matrix.scalar_inj -theorem scalar_commute_iff [Fintype n] [DecidableEq n] {r : α} {M : Matrix n n α} : +theorem scalar_commute_iff {r : α} {M : Matrix n n α} : Commute (scalar n r) M ↔ r • M = MulOpposite.op r • M := by simp_rw [Commute, SemiconjBy, scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal] -theorem scalar_commute [Fintype n] [DecidableEq n] (r : α) (hr : ∀ r', Commute r r') - (M : Matrix n n α) : +theorem scalar_commute (r : α) (hr : ∀ r', Commute r r') (M : Matrix n n α) : Commute (scalar n r) M := scalar_commute_iff.2 <| ext fun _ _ => hr _ #align matrix.scalar.commute Matrix.scalar_commuteₓ diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 56795507ff4b1..6c9f00f2c2890 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -2681,11 +2681,11 @@ theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) : rw [inter_comm, replicate_inter, min_comm] #align multiset.inter_replicate Multiset.inter_replicate -theorem erase_attach_map_val [DecidableEq α] (s : Multiset α) (x : {x // x ∈ s}) : +theorem erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) : (s.attach.erase x).map (↑) = s.erase x := by rw [Multiset.map_erase _ val_injective, attach_map_val] -theorem erase_attach_map [DecidableEq α] (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) : +theorem erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) : (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f := by simp only [← Function.comp_apply (f := f)] rw [← map_map, erase_attach_map_val] diff --git a/Mathlib/FieldTheory/Normal.lean b/Mathlib/FieldTheory/Normal.lean index 8b067ef4f702c..8bb06042d389e 100644 --- a/Mathlib/FieldTheory/Normal.lean +++ b/Mathlib/FieldTheory/Normal.lean @@ -148,7 +148,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : exact ⟨hp, minpoly.ne_zero hx⟩ #align normal.of_is_splitting_field Normal.of_isSplittingField -instance Polynomial.SplittingField.instNormal [Field F] (p : F[X]) : Normal F p.SplittingField := +instance Polynomial.SplittingField.instNormal (p : F[X]) : Normal F p.SplittingField := Normal.of_isSplittingField p #align polynomial.splitting_field.normal Polynomial.SplittingField.instNormal diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index 43052c3140321..89da81c213792 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -429,10 +429,10 @@ end Submonoid section LeftCancelMonoid -variable [LeftCancelMonoid G] +variable [LeftCancelMonoid G] [Finite G] @[to_additive] -theorem ExponentExists.of_finite [Finite G] : ExponentExists G := by +theorem ExponentExists.of_finite : ExponentExists G := by let _inst := Fintype.ofFinite G simp only [Monoid.ExponentExists] refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩ @@ -441,14 +441,13 @@ theorem ExponentExists.of_finite [Finite G] : ExponentExists G := by exact order_dvd_exponent g @[to_additive] -theorem exponent_ne_zero_of_finite [Finite G] : exponent G ≠ 0 := +theorem exponent_ne_zero_of_finite : exponent G ≠ 0 := ExponentExists.of_finite.exponent_ne_zero #align monoid.exponent_ne_zero_of_finite Monoid.exponent_ne_zero_of_finite #align add_monoid.exponent_ne_zero_of_finite AddMonoid.exponent_ne_zero_of_finite @[to_additive AddMonoid.one_lt_exponent] -lemma one_lt_exponent [LeftCancelMonoid G] [Finite G] [Nontrivial G] : - 1 < Monoid.exponent G := by +lemma one_lt_exponent [Nontrivial G] : 1 < Monoid.exponent G := by rw [Nat.one_lt_iff_ne_zero_and_ne_one] exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩ diff --git a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean index 33c4220a56dfb..71a30afc7b866 100644 --- a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean +++ b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean @@ -243,7 +243,7 @@ lemma ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) IsFreeGroup G := (FreeGroupBasis.ofUniqueLift X of h).isFreeGroup -lemma ofMulEquiv [IsFreeGroup G] (e : G ≃* H) : IsFreeGroup H := +lemma ofMulEquiv (e : G ≃* H) : IsFreeGroup H := ((basis G).map e).isFreeGroup end IsFreeGroup diff --git a/Mathlib/GroupTheory/GroupAction/ConjAct.lean b/Mathlib/GroupTheory/GroupAction/ConjAct.lean index 5708d1470a479..017305b68ef70 100644 --- a/Mathlib/GroupTheory/GroupAction/ConjAct.lean +++ b/Mathlib/GroupTheory/GroupAction/ConjAct.lean @@ -311,7 +311,7 @@ theorem orbitRel_conjAct : (orbitRel (ConjAct G) G).Rel = IsConj := funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct] #align conj_act.orbit_rel_conj_act ConjAct.orbitRel_conjAct -theorem orbit_eq_carrier_conjClasses [Group G] (g : G) : +theorem orbit_eq_carrier_conjClasses (g : G) : orbit (ConjAct G) g = (ConjClasses.mk g).carrier := by ext h rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct] diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean index bddbf6ec98793..daf9ba2d9c37d 100644 --- a/Mathlib/GroupTheory/Perm/ClosureSwap.lean +++ b/Mathlib/GroupTheory/Perm/ClosureSwap.lean @@ -126,7 +126,7 @@ theorem closure_of_isSwap_of_isPretransitive [Finite α] {S : Set (Perm α)} (hS simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite] /-- A transitive permutation group generated by transpositions must be the whole symmetric group -/ -theorem surjective_of_isSwap_of_isPretransitive [Group G] [MulAction G α] [Finite α] (S : Set G) +theorem surjective_of_isSwap_of_isPretransitive [Finite α] (S : Set G) (hS1 : ∀ σ ∈ S, Perm.IsSwap (MulAction.toPermHom G α σ)) (hS2 : Subgroup.closure S = ⊤) [h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α) := by rw [← MonoidHom.range_top_iff_surjective] diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean index c756e3be8cb71..48e938f32da86 100644 --- a/Mathlib/GroupTheory/PushoutI.lean +++ b/Mathlib/GroupTheory/PushoutI.lean @@ -435,8 +435,7 @@ theorem summand_smul_def' {i : ι} (g : G i) (w : NormalWord d) : { equivPair i w with head := g * (equivPair i w).head } := rfl -noncomputable instance mulAction [DecidableEq ι] [∀ i, DecidableEq (G i)] : - MulAction (PushoutI φ) (NormalWord d) := +noncomputable instance mulAction : MulAction (PushoutI φ) (NormalWord d) := MulAction.ofEndHom <| lift (fun i => MulAction.toEndHom) diff --git a/Mathlib/LinearAlgebra/Dimension/Finite.lean b/Mathlib/LinearAlgebra/Dimension/Finite.lean index 9ac0f2dbede50..4c701e5c4cd05 100644 --- a/Mathlib/LinearAlgebra/Dimension/Finite.lean +++ b/Mathlib/LinearAlgebra/Dimension/Finite.lean @@ -67,7 +67,7 @@ lemma rank_eq_zero_iff : variable [Nontrivial R] variable [NoZeroSMulDivisors R M] -theorem rank_zero_iff_forall_zero [NoZeroSMulDivisors R M] : +theorem rank_zero_iff_forall_zero : Module.rank R M = 0 ↔ ∀ x : M, x = 0 := by simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or, exists_and_right, and_iff_right (exists_ne (0 : R))] @@ -93,7 +93,7 @@ lemma rank_eq_zero_iff_isTorsion {R M} [CommRing R] [IsDomain R] [AddCommGroup M rw [Module.IsTorsion, rank_eq_zero_iff] simp [mem_nonZeroDivisors_iff_ne_zero] -theorem rank_pos [NoZeroSMulDivisors R M] [Nontrivial M] : 0 < Module.rank R M := +theorem rank_pos [Nontrivial M] : 0 < Module.rank R M := rank_pos_iff_nontrivial.mpr ‹_› #align rank_pos rank_pos @@ -382,7 +382,7 @@ theorem FiniteDimensional.finrank_pos [NoZeroSMulDivisors R M] [h : Nontrivial M /-- See `FiniteDimensional.finrank_zero_iff` for the stronger version with `NoZeroSMulDivisors R M`. -/ -theorem FiniteDimensional.finrank_eq_zero_iff [Module.Finite R M] : +theorem FiniteDimensional.finrank_eq_zero_iff : finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 := by rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank] norm_cast diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean index 11247b3c678a7..4485bc7cda3de 100644 --- a/Mathlib/LinearAlgebra/Dimension/Localization.lean +++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean @@ -23,7 +23,7 @@ section CommRing universe u u' v v' variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'} -variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] +variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] variable (hp : p ≤ R⁰) diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index a13baa5c2435b..891907a42b6f2 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -694,7 +694,7 @@ instance _root_.Prod.instModuleIsReflexive [IsReflexive R N] : exact Bijective.Prod_map (bijective_dual_eval R M) (bijective_dual_eval R N) variable {R M N} in -lemma equiv [IsReflexive R M] (e : M ≃ₗ[R] N) : IsReflexive R N where +lemma equiv (e : M ≃ₗ[R] N) : IsReflexive R N where bijective_dual_eval' := by let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) := by diff --git a/Mathlib/LinearAlgebra/SesquilinearForm.lean b/Mathlib/LinearAlgebra/SesquilinearForm.lean index ee6e376b0d0b8..c69ea280841fc 100644 --- a/Mathlib/LinearAlgebra/SesquilinearForm.lean +++ b/Mathlib/LinearAlgebra/SesquilinearForm.lean @@ -654,9 +654,8 @@ theorem SeparatingLeft.ne_zero [Nontrivial M₁] {B : M₁ →ₛₗ[I₁] M₂ section Linear variable [AddCommMonoid Mₗ₁] [AddCommMonoid Mₗ₂] [AddCommMonoid Mₗ₁'] [AddCommMonoid Mₗ₂'] - [AddCommMonoid M] -variable [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] [Module R M] +variable [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] variable {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M} (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') theorem SeparatingLeft.congr (h : B.SeparatingLeft) : diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index d585d368c6fec..c63c9fe6745b2 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -1145,7 +1145,7 @@ lemma MeasurableEmbedding.borelSpace {α β : Type*} [MeasurableSpace α] [Topol have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq rw [← this, ← borel_comap, h''e.induced] -instance _root_.ULift.instBorelSpace [BorelSpace α] : BorelSpace (ULift α) := +instance _root_.ULift.instBorelSpace : BorelSpace (ULift α) := MeasurableEquiv.ulift.measurableEmbedding.borelSpace Homeomorph.ulift.inducing instance DiscreteMeasurableSpace.toBorelSpace {α : Type*} [TopologicalSpace α] [DiscreteTopology α] diff --git a/Mathlib/MeasureTheory/Constructions/Projective.lean b/Mathlib/MeasureTheory/Constructions/Projective.lean index 49021d5a71383..8798bf8561dd4 100644 --- a/Mathlib/MeasureTheory/Constructions/Projective.lean +++ b/Mathlib/MeasureTheory/Constructions/Projective.lean @@ -38,8 +38,7 @@ variable {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] /-- A family of measures indexed by finite sets of `ι` is projective if, for finite sets `J ⊆ I`, the projection from `∀ i : I, α i` to `∀ i : J, α i` maps `P I` to `P J`. -/ -def IsProjectiveMeasureFamily [∀ i, MeasurableSpace (α i)] - (P : ∀ J : Finset ι, Measure (∀ j : J, α j)) : Prop := +def IsProjectiveMeasureFamily (P : ∀ J : Finset ι, Measure (∀ j : J, α j)) : Prop := ∀ (I J : Finset ι) (hJI : J ⊆ I), P J = (P I).map (fun (x : ∀ i : I, α i) (j : J) ↦ x ⟨j, hJI j.2⟩) diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 800dad979cd6a..9e12f74f5e9bf 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -578,12 +578,12 @@ instance innerRegular_map_smul {α} [Monoid α] [MulAction α G] [ContinuousCons /-- The image of an inner regular measure under left multiplication is again inner regular. -/ @[to_additive "The image of an inner regular measure under left addition is again inner regular."] -instance innerRegular_map_mul_left [BorelSpace G] [TopologicalGroup G] [InnerRegular μ] (g : G) : +instance innerRegular_map_mul_left [TopologicalGroup G] [InnerRegular μ] (g : G) : InnerRegular (Measure.map (g * ·) μ) := InnerRegular.map_of_continuous (continuous_mul_left g) /-- The image of an inner regular measure under right multiplication is again inner regular. -/ @[to_additive "The image of an inner regular measure under right addition is again inner regular."] -instance innerRegular_map_mul_right [BorelSpace G] [TopologicalGroup G] [InnerRegular μ] (g : G) : +instance innerRegular_map_mul_right [TopologicalGroup G] [InnerRegular μ] (g : G) : InnerRegular (Measure.map (· * g) μ) := InnerRegular.map_of_continuous (continuous_mul_right g) variable [TopologicalGroup G] diff --git a/Mathlib/MeasureTheory/Measure/Count.lean b/Mathlib/MeasureTheory/Measure/Count.lean index 27a4012045cc3..aa8deb3a722ac 100644 --- a/Mathlib/MeasureTheory/Measure/Count.lean +++ b/Mathlib/MeasureTheory/Measure/Count.lean @@ -183,7 +183,7 @@ theorem count_injective_image [MeasurableSingletonClass α] [MeasurableSingleton rw [count_apply_infinite hs] #align measure_theory.measure.count_injective_image MeasureTheory.Measure.count_injective_image -instance count.isFiniteMeasure [Finite α] [MeasurableSpace α] : +instance count.isFiniteMeasure [Finite α] : IsFiniteMeasure (Measure.count : Measure α) := ⟨by cases nonempty_fintype α diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean index 4f1a654f92b3e..ea1ac4544ab90 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -313,11 +313,10 @@ protected lemma _root_.MeasurableEmbedding.isProbabilityMeasure_comap (hf : Meas (hf' : ∀ᵐ a ∂μ, a ∈ range f) : IsProbabilityMeasure (μ.comap f) := isProbabilityMeasure_comap hf.injective hf' hf.measurableSet_image' -instance isProbabilityMeasure_map_up [IsProbabilityMeasure μ] : +instance isProbabilityMeasure_map_up : IsProbabilityMeasure (μ.map ULift.up) := isProbabilityMeasure_map measurable_up.aemeasurable -instance isProbabilityMeasure_comap_down [IsProbabilityMeasure μ] : - IsProbabilityMeasure (μ.comap ULift.down) := +instance isProbabilityMeasure_comap_down : IsProbabilityMeasure (μ.comap ULift.down) := MeasurableEquiv.ulift.measurableEmbedding.isProbabilityMeasure_comap <| ae_of_all _ <| by simp [Function.Surjective.range_eq <| EquivLike.surjective _] diff --git a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean index 8fb799ce25f1f..a4596892c3a5c 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean @@ -551,7 +551,7 @@ theorem IsNontrivial.sum_eq_zero [IsDomain R'] {χ : MulChar R R'} /-- The sum over all values of the trivial multiplicative character on a finite ring is the cardinality of its unit group. -/ -theorem sum_one_eq_card_units [Fintype R] [DecidableEq R] : +theorem sum_one_eq_card_units [DecidableEq R] : (∑ a, (1 : MulChar R R') a) = Fintype.card Rˣ := by calc (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 := diff --git a/Mathlib/Order/Birkhoff.lean b/Mathlib/Order/Birkhoff.lean index 686e170f0ff35..8cf896d0ca17e 100644 --- a/Mathlib/Order/Birkhoff.lean +++ b/Mathlib/Order/Birkhoff.lean @@ -247,7 +247,7 @@ variable [DecidableEq α] rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding] simpa using OrderIso.map_inf _ _ _ -@[simp] lemma birkhoffSet_apply [OrderBot α] (a : α) : +@[simp] lemma birkhoffSet_apply (a : α) : birkhoffSet a = OrderIso.lowerSetSupIrred a := by simp [birkhoffSet]; convert rfl diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index 7ee23d8aa1097..7a59d196fce7d 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -1590,7 +1590,7 @@ lemma bddBelow_range_prod {F : ι → α × β} : BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) := bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ) -theorem isLUB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : +theorem isLUB_prod {s : Set (α × β)} (p : α × β) : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by refine' ⟨fun H => @@ -1607,7 +1607,7 @@ theorem isLUB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩ #align is_lub_prod isLUB_prod -theorem isGLB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : +theorem isGLB_prod {s : Set (α × β)} (p : α × β) : IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 := @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _ #align is_glb_prod isGLB_prod diff --git a/Mathlib/Order/Directed.lean b/Mathlib/Order/Directed.lean index 7c603a96169d0..2fb710dc7c26a 100644 --- a/Mathlib/Order/Directed.lean +++ b/Mathlib/Order/Directed.lean @@ -312,7 +312,7 @@ theorem exists_lt_of_directed_le [IsDirected β (· ≤ ·)] [Nontrivial β] : ⟨b, a, h⟩ #align exists_lt_of_directed_le exists_lt_of_directed_le -variable [PartialOrder β] {f : α → β} {s : Set α} +variable {f : α → β} {s : Set α} -- TODO: Generalise the following two lemmas to connected orders diff --git a/Mathlib/Order/Hom/Bounded.lean b/Mathlib/Order/Hom/Bounded.lean index 0fa6f7ee2107e..64a788214c4b4 100644 --- a/Mathlib/Order/Hom/Bounded.lean +++ b/Mathlib/Order/Hom/Bounded.lean @@ -181,8 +181,6 @@ def BotHomClass.toBotHom [Bot α] [Bot β] [BotHomClass F α β] (f : F) : BotHo instance [Bot α] [Bot β] [BotHomClass F α β] : CoeTC F (BotHom α β) := ⟨BotHomClass.toBotHom⟩ -variable [FunLike F α β] - /-- Turn an element of a type `F` satisfying `BoundedOrderHomClass F α β` into an actual `BoundedOrderHom`. This is declared as the default coercion from `F` to `BoundedOrderHom α β`. -/ @[coe] diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index b4d3ce3dc42f2..9d66a67c300bb 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -970,8 +970,6 @@ lemma not_monotone_not_antitone_iff_exists_lt_lt : -/ -variable [LinearOrder β] {f : α → β} {s : Set α} {x y : α} - theorem StrictMonoOn.cmp_map_eq (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp x y := ((hf.compares hx hy).2 (cmp_compares x y)).cmp_eq diff --git a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean index fb5839aceff92..8c4f177f993b4 100644 --- a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean +++ b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean @@ -283,7 +283,7 @@ theorem toMeasure_apply_inter_support (hs : MeasurableSet s) (hp : MeasurableSet #align pmf.to_measure_apply_inter_support PMF.toMeasure_apply_inter_support @[simp] -theorem restrict_toMeasure_support [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) : +theorem restrict_toMeasure_support [MeasurableSingletonClass α] (p : PMF α) : Measure.restrict (toMeasure p) (support p) = toMeasure p := by ext s hs apply (MeasureTheory.Measure.restrict_apply hs).trans diff --git a/Mathlib/RepresentationTheory/Action/Limits.lean b/Mathlib/RepresentationTheory/Action/Limits.lean index a63e6f676ad01..1b8f6a3d48aab 100644 --- a/Mathlib/RepresentationTheory/Action/Limits.lean +++ b/Mathlib/RepresentationTheory/Action/Limits.lean @@ -326,13 +326,11 @@ set_option linter.uppercaseLean3 false in variable {H : MonCat.{u}} (f : G ⟶ H) -instance res_additive [Preadditive V] : (res V f).Additive where +instance res_additive : (res V f).Additive where set_option linter.uppercaseLean3 false in #align Action.res_additive Action.res_additive -variable {R : Type*} [Semiring R] - -instance res_linear [Preadditive V] [Linear R V] : (res V f).Linear R where +instance res_linear : (res V f).Linear R where set_option linter.uppercaseLean3 false in #align Action.res_linear Action.res_linear diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean index 577437c6130b1..4906d6723aa6b 100644 --- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean +++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean @@ -38,12 +38,12 @@ variable {R : Type u} {S : Type v} [CommRing R] [Semiring S] (f : R →+* S) This is an isomorphism if `f` has a right inverse (`quotientKerEquivOfRightInverse`) / is surjective (`quotientKerEquivOfSurjective`). -/ -def kerLift (f : R →+* S) : R ⧸ ker f →+* S := +def kerLift : R ⧸ ker f →+* S := Ideal.Quotient.lift _ f fun _ => f.mem_ker.mp #align ring_hom.ker_lift RingHom.kerLift @[simp] -theorem kerLift_mk (f : R →+* S) (r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r := +theorem kerLift_mk (r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r := Ideal.Quotient.lift_mk _ _ _ #align ring_hom.ker_lift_mk RingHom.kerLift_mk @@ -58,7 +58,7 @@ theorem lift_injective_of_ker_le_ideal (I : Ideal R) {f : R →+* S} (H : ∀ a #align ring_hom.lift_injective_of_ker_le_ideal RingHom.lift_injective_of_ker_le_ideal /-- The induced map from the quotient by the kernel is injective. -/ -theorem kerLift_injective [Semiring S] (f : R →+* S) : Function.Injective (kerLift f) := +theorem kerLift_injective : Function.Injective (kerLift f) := lift_injective_of_ker_le_ideal (ker f) (fun a => by simp only [mem_ker, imp_self]) le_rfl #align ring_hom.ker_lift_injective RingHom.kerLift_injective diff --git a/Mathlib/RingTheory/IntegralRestrict.lean b/Mathlib/RingTheory/IntegralRestrict.lean index 5511a000bd8c5..a91d3aa21bfc7 100644 --- a/Mathlib/RingTheory/IntegralRestrict.lean +++ b/Mathlib/RingTheory/IntegralRestrict.lean @@ -284,7 +284,7 @@ variable [IsIntegrallyClosed A] /-- The restriction of the norm on `L/K` restricted onto `B/A` in an AKLB setup. See `Algebra.intNorm` instead. -/ noncomputable -def Algebra.intNormAux [IsIntegrallyClosed A] [IsSeparable K L] : +def Algebra.intNormAux [IsSeparable K L] : B →* A where toFun := fun s ↦ IsIntegralClosure.mk' (R := A) A (Algebra.norm K (algebraMap B L s)) (isIntegral_norm K <| IsIntegral.map (IsScalarTower.toAlgHom A B L) @@ -396,8 +396,7 @@ variable [IsDomain Aₘ] [IsIntegrallyClosed Aₘ] [IsDomain Bₘ] [IsIntegrally variable [NoZeroSMulDivisors Aₘ Bₘ] [Module.Finite Aₘ Bₘ] variable [IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)] -lemma Algebra.intNorm_eq_of_isLocalization - [IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)] (x : B) : +lemma Algebra.intNorm_eq_of_isLocalization (x : B) : algebraMap A Aₘ (Algebra.intNorm A B x) = Algebra.intNorm Aₘ Bₘ (algebraMap B Bₘ x) := by by_cases hM : 0 ∈ M · have := IsLocalization.uniqueOfZeroMem (S := Aₘ) hM diff --git a/Mathlib/RingTheory/RingInvo.lean b/Mathlib/RingTheory/RingInvo.lean index 5b530ffcba6ef..ce6ca1bcaa24a 100644 --- a/Mathlib/RingTheory/RingInvo.lean +++ b/Mathlib/RingTheory/RingInvo.lean @@ -64,10 +64,10 @@ variable {R} [Semiring R] [EquivLike F R Rᵐᵒᵖ] /-- Any type satisfying `RingInvoClass` can be cast into `RingInvo` via `RingInvoClass.toRingInvo`. -/ -instance [Semiring R] [RingInvoClass F R] : CoeTC F (RingInvo R) := +instance [RingInvoClass F R] : CoeTC F (RingInvo R) := ⟨RingInvoClass.toRingInvo⟩ -instance [Semiring R] : EquivLike (RingInvo R) R Rᵐᵒᵖ where +instance : EquivLike (RingInvo R) R Rᵐᵒᵖ where coe f := f.toFun inv f := f.invFun coe_injective' e f h₁ h₂ := by @@ -78,7 +78,7 @@ instance [Semiring R] : EquivLike (RingInvo R) R Rᵐᵒᵖ where left_inv f := f.left_inv right_inv f := f.right_inv -instance [Semiring R] : RingInvoClass (RingInvo R) R where +instance : RingInvoClass (RingInvo R) R where map_add f := f.map_add' map_mul f := f.map_mul' involution f := f.involution' diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 34860b597510d..87f736812fb7e 100644 --- a/Mathlib/RingTheory/SimpleModule.lean +++ b/Mathlib/RingTheory/SimpleModule.lean @@ -219,7 +219,7 @@ instance quotient : IsSemisimpleModule R (M ⧸ m) := .congr (m.quotientEquivOfIsCompl P compl) -- does not work as an instance, not sure why -protected theorem range [IsSemisimpleModule R M] (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) := +protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) := .congr (quotKerEquivRange _).symm section diff --git a/Mathlib/RingTheory/Subsemiring/Order.lean b/Mathlib/RingTheory/Subsemiring/Order.lean index 2f7a2c0194e50..21f6bf79fa239 100644 --- a/Mathlib/RingTheory/Subsemiring/Order.lean +++ b/Mathlib/RingTheory/Subsemiring/Order.lean @@ -23,35 +23,35 @@ instance toOrderedSemiring [OrderedSemiring R] [SubsemiringClass S R] : #align subsemiring_class.to_ordered_semiring SubsemiringClass.toOrderedSemiring /-- A subsemiring of a `StrictOrderedSemiring` is a `StrictOrderedSemiring`. -/ -instance toStrictOrderedSemiring [StrictOrderedSemiring R] [SetLike S R] +instance toStrictOrderedSemiring [StrictOrderedSemiring R] [SubsemiringClass S R] : StrictOrderedSemiring s := Subtype.coe_injective.strictOrderedSemiring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl #align subsemiring_class.to_strict_ordered_semiring SubsemiringClass.toStrictOrderedSemiring /-- A subsemiring of an `OrderedCommSemiring` is an `OrderedCommSemiring`. -/ -instance toOrderedCommSemiring [OrderedCommSemiring R] [SetLike S R] [SubsemiringClass S R] : +instance toOrderedCommSemiring [OrderedCommSemiring R] [SubsemiringClass S R] : OrderedCommSemiring s := Subtype.coe_injective.orderedCommSemiring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl #align subsemiring_class.to_ordered_comm_semiring SubsemiringClass.toOrderedCommSemiring /-- A subsemiring of a `StrictOrderedCommSemiring` is a `StrictOrderedCommSemiring`. -/ -instance toStrictOrderedCommSemiring [StrictOrderedCommSemiring R] [SetLike S R] +instance toStrictOrderedCommSemiring [StrictOrderedCommSemiring R] [SubsemiringClass S R] : StrictOrderedCommSemiring s := Subtype.coe_injective.strictOrderedCommSemiring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl #align subsemiring_class.to_strict_ordered_comm_semiring SubsemiringClass.toStrictOrderedCommSemiring /-- A subsemiring of a `LinearOrderedSemiring` is a `LinearOrderedSemiring`. -/ -instance toLinearOrderedSemiring [LinearOrderedSemiring R] [SetLike S R] +instance toLinearOrderedSemiring [LinearOrderedSemiring R] [SubsemiringClass S R] : LinearOrderedSemiring s := Subtype.coe_injective.linearOrderedSemiring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) fun _ _ => rfl #align subsemiring_class.to_linear_ordered_semiring SubsemiringClass.toLinearOrderedSemiring /-- A subsemiring of a `LinearOrderedCommSemiring` is a `LinearOrderedCommSemiring`. -/ -instance toLinearOrderedCommSemiring [LinearOrderedCommSemiring R] [SetLike S R] +instance toLinearOrderedCommSemiring [LinearOrderedCommSemiring R] [SubsemiringClass S R] : LinearOrderedCommSemiring s := Subtype.coe_injective.linearOrderedCommSemiring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) fun _ _ => rfl diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean index d1b415dd60f5b..545dbdb78ec47 100644 --- a/Mathlib/RingTheory/TensorProduct/Basic.lean +++ b/Mathlib/RingTheory/TensorProduct/Basic.lean @@ -659,7 +659,7 @@ theorem algEquivOfLinearEquivTripleTensorProduct_apply (f h_mul h_one x) : #align algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product_apply Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply section lift -variable [IsScalarTower R S A] [IsScalarTower R S C] +variable [IsScalarTower R S C] /-- The forward direction of the universal property of tensor products of algebras; any algebra morphism from the tensor product can be factored as the product of two algebra morphisms that @@ -709,9 +709,8 @@ This is `Algebra.TensorProduct.lift` as an equivalence. See also `GradedTensorProduct.liftEquiv` for an alternative commutativity requirement for graded algebra. -/ @[simps] -def liftEquiv [IsScalarTower R S A] [IsScalarTower R S C] : - {fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ x y, Commute (fg.1 x) (fg.2 y)} - ≃ ((A ⊗[R] B) →ₐ[S] C) where +def liftEquiv : {fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ x y, Commute (fg.1 x) (fg.2 y)} + ≃ ((A ⊗[R] B) →ₐ[S] C) where toFun fg := lift fg.val.1 fg.val.2 fg.prop invFun f' := ⟨(f'.comp includeLeft, (f'.restrictScalars R).comp includeRight), fun x y => ((Commute.one_right _).tmul (Commute.one_left _)).map f'⟩ diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean index 2936119b76ad7..f043e149a87c9 100644 --- a/Mathlib/Topology/Algebra/Order/Compact.lean +++ b/Mathlib/Topology/Algebra/Order/Compact.lean @@ -202,7 +202,7 @@ theorem IsCompact.exists_isLUB [ClosedIciTopology α] {s : Set α} (hs : IsCompa IsCompact.exists_isGLB (α := αᵒᵈ) hs ne_s #align is_compact.exists_is_lub IsCompact.exists_isLUB -theorem cocompact_le_atBot_atTop [LinearOrder α] [CompactIccSpace α] : +theorem cocompact_le_atBot_atTop [CompactIccSpace α] : cocompact α ≤ atBot ⊔ atTop := by refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩ @@ -211,7 +211,7 @@ theorem cocompact_le_atBot_atTop [LinearOrder α] [CompactIccSpace α] : refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩ exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_le h)) fun h ↦ hu x (le_of_not_le h) -theorem cocompact_le_atBot [LinearOrder α] [OrderTop α] [CompactIccSpace α] : +theorem cocompact_le_atBot [OrderTop α] [CompactIccSpace α] : cocompact α ≤ atBot := by refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩ @@ -219,11 +219,11 @@ theorem cocompact_le_atBot [LinearOrder α] [OrderTop α] [CompactIccSpace α] : refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩ exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_le h)) (fun h ↦ (h le_top).elim) -theorem cocompact_le_atTop [LinearOrder α] [OrderBot α] [CompactIccSpace α] : +theorem cocompact_le_atTop [OrderBot α] [CompactIccSpace α] : cocompact α ≤ atTop := cocompact_le_atBot (α := αᵒᵈ) -theorem atBot_le_cocompact [LinearOrder α] [NoMinOrder α] [ClosedIicTopology α] : +theorem atBot_le_cocompact [NoMinOrder α] [ClosedIicTopology α] : atBot ≤ cocompact α := by refine fun s hs ↦ ?_ obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs @@ -236,26 +236,26 @@ theorem atBot_le_cocompact [LinearOrder α] [NoMinOrder α] [ClosedIicTopology exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_not_mem.mp hc)⟩ -theorem atTop_le_cocompact [LinearOrder α] [NoMaxOrder α] [ClosedIciTopology α] : +theorem atTop_le_cocompact [NoMaxOrder α] [ClosedIciTopology α] : atTop ≤ cocompact α := atBot_le_cocompact (α := αᵒᵈ) -theorem atBot_atTop_le_cocompact [LinearOrder α] [NoMinOrder α] [NoMaxOrder α] +theorem atBot_atTop_le_cocompact [NoMinOrder α] [NoMaxOrder α] [OrderClosedTopology α] : atBot ⊔ atTop ≤ cocompact α := sup_le atBot_le_cocompact atTop_le_cocompact @[simp 900] -theorem cocompact_eq_atBot_atTop [LinearOrder α] [NoMaxOrder α] [NoMinOrder α] +theorem cocompact_eq_atBot_atTop [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] : cocompact α = atBot ⊔ atTop := cocompact_le_atBot_atTop.antisymm atBot_atTop_le_cocompact @[simp] -theorem cocompact_eq_atBot [LinearOrder α] [NoMinOrder α] [OrderTop α] +theorem cocompact_eq_atBot [NoMinOrder α] [OrderTop α] [ClosedIicTopology α] [CompactIccSpace α] : cocompact α = atBot := cocompact_le_atBot.antisymm atBot_le_cocompact @[simp] -theorem cocompact_eq_atTop [LinearOrder α] [NoMaxOrder α] [OrderBot α] +theorem cocompact_eq_atTop [NoMaxOrder α] [OrderBot α] [ClosedIciTopology α] [CompactIccSpace α] : cocompact α = atTop := cocompact_le_atTop.antisymm atTop_le_cocompact diff --git a/Mathlib/Topology/Compactness/SigmaCompact.lean b/Mathlib/Topology/Compactness/SigmaCompact.lean index 6862ebe5cefab..69d55a86cd03d 100644 --- a/Mathlib/Topology/Compactness/SigmaCompact.lean +++ b/Mathlib/Topology/Compactness/SigmaCompact.lean @@ -435,7 +435,7 @@ noncomputable def choice (X : Type*) [TopologicalSpace X] [WeaklyLocallyCompactS exact iUnion_mono' fun n => ⟨n + 1, subset_union_right _ _⟩ #align compact_exhaustion.choice CompactExhaustion.choice -noncomputable instance [LocallyCompactSpace X] [SigmaCompactSpace X] : +noncomputable instance [LocallyCompactSpace X] : Inhabited (CompactExhaustion X) := ⟨CompactExhaustion.choice X⟩ diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index cc65d80b9dddb..b03e32a106a5c 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -332,7 +332,7 @@ theorem PreconnectedSpace.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTop /-- Refinement of `IsPreconnected.constant` only assuming the map factors through a discrete subset of the target. -/ -theorem IsPreconnected.constant_of_mapsTo [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) +theorem IsPreconnected.constant_of_mapsTo {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y := by let F : S → T := hTm.restrict f S T @@ -342,7 +342,7 @@ theorem IsPreconnected.constant_of_mapsTo [TopologicalSpace β] {S : Set α} (hS /-- A version of `IsPreconnected.constant_of_mapsTo` that assumes that the codomain is nonempty and proves that `f` is equal to `const α y` on `S` for some `y ∈ T`. -/ -theorem IsPreconnected.eqOn_const_of_mapsTo [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) +theorem IsPreconnected.eqOn_const_of_mapsTo {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, EqOn f (const α y) S := by rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩) diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean index 0023ffe57ea87..55406b70c40f8 100644 --- a/Mathlib/Topology/Order.lean +++ b/Mathlib/Topology/Order.lean @@ -299,7 +299,7 @@ theorem continuous_of_discreteTopology [TopologicalSpace β] {f : α → β} : C /-- A function to a discrete topological space is continuous if and only if the preimage of every singleton is open. -/ -theorem continuous_discrete_rng [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] +theorem continuous_discrete_rng [TopologicalSpace β] [DiscreteTopology β] {f : α → β} : Continuous f ↔ ∀ b : β, IsOpen (f ⁻¹' {b}) := ⟨fun h b => (isOpen_discrete _).preimage h, fun h => ⟨fun s _ => by rw [← biUnion_of_singleton s, preimage_iUnion₂] @@ -863,13 +863,13 @@ theorem map_nhds_induced_of_mem {a : α} (h : range f ∈ 𝓝 (f a)) : map f (@nhds α (induced f t) a) = 𝓝 (f a) := by rw [nhds_induced, Filter.map_comap_of_mem h] #align map_nhds_induced_of_mem map_nhds_induced_of_mem -theorem closure_induced [t : TopologicalSpace β] {f : α → β} {a : α} {s : Set α} : +theorem closure_induced {f : α → β} {a : α} {s : Set α} : a ∈ @closure α (t.induced f) s ↔ f a ∈ closure (f '' s) := by letI := t.induced f simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm] #align closure_induced closure_induced -theorem isClosed_induced_iff' [t : TopologicalSpace β] {f : α → β} {s : Set α} : +theorem isClosed_induced_iff' {f : α → β} {s : Set α} : IsClosed[t.induced f] s ↔ ∀ a, f a ∈ closure (f '' s) → a ∈ s := by letI := t.induced f simp only [← closure_subset_iff_isClosed, subset_def, closure_induced] diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean index c7b229a054d51..3af4e260a9e4a 100644 --- a/Mathlib/Topology/Order/ScottTopology.lean +++ b/Mathlib/Topology/Order/ScottTopology.lean @@ -340,7 +340,7 @@ variable [Preorder α] [TopologicalSpace α] /-- If `α` is equipped with the Scott topology, then it is homeomorphic to `WithScott α`. -/ -def IsScott.withScottHomeomorph [TopologicalSpace α] [IsScott α] : WithScott α ≃ₜ α := +def IsScott.withScottHomeomorph [IsScott α] : WithScott α ≃ₜ α := WithScott.ofScott.toHomeomorphOfInducing ⟨by erw [IsScott.topology_eq α, induced_id]; rfl⟩ lemma IsScott.scottHausdorff_le [IsScott α] : scottHausdorff α ≤ ‹TopologicalSpace α› := by diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index c9b05051cac09..8687cf40f3217 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -1992,7 +1992,7 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, /-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint neighborhoods. -/ -lemma SeparatedNhds.of_isCompact_isClosed [RegularSpace X] {s t : Set X} +lemma SeparatedNhds.of_isCompact_isClosed {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t := by simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, ht.closure_eq, disjoint_left] using hst diff --git a/test/ComputeDegree.lean b/test/ComputeDegree.lean index 3f4d209c9650f..14449a1c73908 100644 --- a/test/ComputeDegree.lean +++ b/test/ComputeDegree.lean @@ -220,15 +220,15 @@ example : natDegree (C a * C b + X + monomial 3 4 * X) ≤ 4 := by compute_degre example {F} [Ring F] {a : F} : natDegree (X ^ 3 + C a * X ^ 10 : F[X]) ≤ 10 := by compute_degree -example [Semiring R] : natDegree (7 * X : R[X]) ≤ 1 := by compute_degree +example : natDegree (7 * X : R[X]) ≤ 1 := by compute_degree -example [Semiring R] {a : R} : natDegree (a • X ^ 5 : R[X]) ≤ 5 := by +example {a : R} : natDegree (a • X ^ 5 : R[X]) ≤ 5 := by compute_degree -example [Semiring R] {a : R} (a0 : a ≠ 0) : natDegree (a • X ^ 5 + X : R[X]) = 5 := by +example {a : R} (a0 : a ≠ 0) : natDegree (a • X ^ 5 + X : R[X]) = 5 := by compute_degree! -example [Semiring R] {a : R} (a0 : a ≠ 0) : degree (a • X ^ 5 + X ^ 2 : R[X]) = 5 := by +example {a : R} (a0 : a ≠ 0) : degree (a • X ^ 5 + X ^ 2 : R[X]) = 5 := by compute_degree! end tests_from_mathlib3 diff --git a/test/Continuity.lean b/test/Continuity.lean index b70112a6d3fc2..7df66051c1b4e 100644 --- a/test/Continuity.lean +++ b/test/Continuity.lean @@ -27,8 +27,7 @@ example {g : X → X} (y : Y) : Continuous ((fun _ ↦ y) ∘ g) := by continuit example {f : X → Y} (x : X) : Continuous (fun (_ : X) ↦ f x) := by continuity -example [TopologicalSpace X] [TopologicalSpace Y] - (f₁ f₂ : X → Y) (hf₁ : Continuous f₁) (hf₂ : Continuous f₂) +example (f₁ f₂ : X → Y) (hf₁ : Continuous f₁) (hf₂ : Continuous f₂) (g : Y → ℝ) (hg : Continuous g) : Continuous (fun x => (max (g (f₁ x)) (g (f₂ x))) + 1) := by continuity diff --git a/test/fun_prop_dev.lean b/test/fun_prop_dev.lean index 7168d4ca2ef5b..89612f04e7db9 100644 --- a/test/fun_prop_dev.lean +++ b/test/fun_prop_dev.lean @@ -125,12 +125,12 @@ instance : FunLike (α -o β) α β where instance : HasUncurry (α ->> β) α β := ⟨fun f x => f x⟩ -instance [Obj β] [HasUncurry β γ δ] : HasUncurry (α ->> β) (α × γ) δ := +instance [HasUncurry β γ δ] : HasUncurry (α ->> β) (α × γ) δ := ⟨fun f p ↦ (↿(f p.1)) p.2⟩ instance : HasUncurry (α -o β) α β := ⟨fun f x => f x⟩ -instance [Obj β] [HasUncurry β γ δ] : HasUncurry (α -o β) (α × γ) δ := +instance [HasUncurry β γ δ] : HasUncurry (α -o β) (α × γ) δ := ⟨fun f p ↦ (↿(f p.1)) p.2⟩