From 55eecd30e63279f625377e2513bd6ab24d554b12 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 3 Oct 2024 18:35:21 +0200 Subject: [PATCH 1/2] remove some variables --- Mathlib/Algebra/Group/Basic.lean | 4 ++-- Mathlib/Algebra/Group/Commute/Defs.lean | 2 +- Mathlib/Algebra/Group/Hom/Defs.lean | 2 -- Mathlib/Algebra/Group/Semiconj/Defs.lean | 2 +- Mathlib/Algebra/GroupWithZero/Defs.lean | 10 +++++----- Mathlib/Algebra/Ring/Defs.lean | 2 +- Mathlib/Control/Traversable/Lemmas.lean | 2 +- Mathlib/Data/Int/Defs.lean | 1 - Mathlib/Data/List/Count.lean | 2 +- Mathlib/Data/Set/Basic.lean | 4 ++-- Mathlib/Data/Sum/Basic.lean | 2 +- Mathlib/Logic/Lemmas.lean | 2 +- Mathlib/Order/BoundedOrder.lean | 4 ++-- Mathlib/Order/Disjoint.lean | 8 ++++---- Mathlib/Order/Lattice.lean | 2 +- Mathlib/Order/Monotone/Basic.lean | 2 +- 16 files changed, 24 insertions(+), 27 deletions(-) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 1fd34ff37fdbc..244c63da588ad 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/Mathlib/Algebra/Group/Basic.lean @@ -172,7 +172,7 @@ end CommSemigroup attribute [local simp] mul_assoc sub_eq_add_neg section Monoid -variable [Monoid M] {a b c : M} {m n : ℕ} +variable [Monoid M] {a b : M} {m n : ℕ} @[to_additive boole_nsmul] lemma pow_boole (P : Prop) [Decidable P] (a : M) : @@ -316,7 +316,7 @@ end InvolutiveInv section DivInvMonoid -variable [DivInvMonoid G] {a b c : G} +variable [DivInvMonoid G] @[to_additive, field_simps] -- The attributes are out of order on purpose theorem inv_eq_one_div (x : G) : x⁻¹ = 1 / x := by rw [div_eq_mul_inv, one_mul] diff --git a/Mathlib/Algebra/Group/Commute/Defs.lean b/Mathlib/Algebra/Group/Commute/Defs.lean index b7bcb09ff56a4..324484366c26a 100644 --- a/Mathlib/Algebra/Group/Commute/Defs.lean +++ b/Mathlib/Algebra/Group/Commute/Defs.lean @@ -181,7 +181,7 @@ end Monoid section DivisionMonoid -variable [DivisionMonoid G] {a b c d : G} +variable [DivisionMonoid G] {a b : G} @[to_additive] protected theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev] diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean index febcba6ed781c..809178c1ff292 100644 --- a/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/Mathlib/Algebra/Group/Hom/Defs.lean @@ -958,8 +958,6 @@ instance [MulOneClass M] [MulOneClass N] : Inhabited (M →* N) := ⟨1⟩ namespace MonoidHom -variable [Group G] [CommGroup H] - @[to_additive (attr := simp)] theorem one_comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) : (1 : N →* P).comp f = 1 := rfl diff --git a/Mathlib/Algebra/Group/Semiconj/Defs.lean b/Mathlib/Algebra/Group/Semiconj/Defs.lean index 88ad2b00a8933..cfeabeb0d12db 100644 --- a/Mathlib/Algebra/Group/Semiconj/Defs.lean +++ b/Mathlib/Algebra/Group/Semiconj/Defs.lean @@ -115,7 +115,7 @@ end Monoid section Group -variable [Group G] {a x y : G} +variable [Group G] /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ @[to_additive "`a` semiconjugates `x` to `a + x + -a`."] diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean index b3d73d7ba0a35..44b5f27539b70 100644 --- a/Mathlib/Algebra/GroupWithZero/Defs.lean +++ b/Mathlib/Algebra/GroupWithZero/Defs.lean @@ -159,17 +159,17 @@ class MulDivCancelClass (M₀ : Type*) [MonoidWithZero M₀] [Div M₀] : Prop w protected mul_div_cancel (a b : M₀) : b ≠ 0 → a * b / b = a section MulDivCancelClass -variable [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {a b : M₀} +variable [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] -@[simp] lemma mul_div_cancel_right₀ (a : M₀) (hb : b ≠ 0) : a * b / b = a := +@[simp] lemma mul_div_cancel_right₀ (a : M₀) {b : M₀} (hb : b ≠ 0) : a * b / b = a := MulDivCancelClass.mul_div_cancel _ _ hb end MulDivCancelClass section MulDivCancelClass -variable [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {a b : M₀} +variable [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] -@[simp] lemma mul_div_cancel_left₀ (b : M₀) (ha : a ≠ 0) : a * b / a = b := by +@[simp] lemma mul_div_cancel_left₀ {a : M₀} (b : M₀) (ha : a ≠ 0) : a * b / a = b := by rw [mul_comm, mul_div_cancel_right₀ _ ha] end MulDivCancelClass @@ -216,7 +216,7 @@ end section GroupWithZero -variable [GroupWithZero G₀] {a b c g h x : G₀} +variable [GroupWithZero G₀] {a b : G₀} @[simp] theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a := diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean index 171d45485e20d..fda1ccb46d3f6 100644 --- a/Mathlib/Algebra/Ring/Defs.lean +++ b/Mathlib/Algebra/Ring/Defs.lean @@ -250,7 +250,7 @@ instance (priority := 100) CommSemiring.toCommMonoidWithZero [CommSemiring α] : section CommSemiring -variable [CommSemiring α] {a b c : α} +variable [CommSemiring α] theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b] diff --git a/Mathlib/Control/Traversable/Lemmas.lean b/Mathlib/Control/Traversable/Lemmas.lean index 25ada54df0f22..a819b3a2c9d79 100644 --- a/Mathlib/Control/Traversable/Lemmas.lean +++ b/Mathlib/Control/Traversable/Lemmas.lean @@ -56,7 +56,7 @@ def PureTransformation : theorem pureTransformation_apply {α} (x : id α) : PureTransformation F x = pure x := rfl -variable {F G} (x : t β) +variable {F G} -- Porting note: need to specify `m/F/G := Id` because `id` no longer has a `Monad` instance theorem map_eq_traverse_id : map (f := t) f = traverse (m := Id) (pure ∘ f) := diff --git a/Mathlib/Data/Int/Defs.lean b/Mathlib/Data/Int/Defs.lean index b5619f8bcea08..2c100995d06a6 100644 --- a/Mathlib/Data/Int/Defs.lean +++ b/Mathlib/Data/Int/Defs.lean @@ -30,7 +30,6 @@ namespace Int variable {a b c d m n : ℤ} section Order -variable {a b c : ℤ} protected lemma le_rfl : a ≤ a := a.le_refl protected lemma lt_or_lt_of_ne : a ≠ b → a < b ∨ b < a := Int.lt_or_gt_of_ne diff --git a/Mathlib/Data/List/Count.lean b/Mathlib/Data/List/Count.lean index 45f4be1166e42..625d247b300b0 100644 --- a/Mathlib/Data/List/Count.lean +++ b/Mathlib/Data/List/Count.lean @@ -19,7 +19,7 @@ assert_not_exists Ring open Nat -variable {α : Type*} {l : List α} +variable {α : Type*} namespace List diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 5a4257688c30d..691836860b538 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1958,7 +1958,7 @@ open Set namespace Function -variable {ι : Sort*} {α : Type*} {β : Type*} {f : α → β} +variable {α : Type*} {β : Type*} theorem Injective.nonempty_apply_iff {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅) {s : Set α} : (f s).Nonempty ↔ s.Nonempty := by @@ -2141,7 +2141,7 @@ end Monotone /-! ### Disjoint sets -/ -variable {α β : Type*} {s t u : Set α} {f : α → β} +variable {α : Type*} {s t u : Set α} namespace Disjoint diff --git a/Mathlib/Data/Sum/Basic.lean b/Mathlib/Data/Sum/Basic.lean index 9da00e98e9adb..d65e9ce7874fe 100644 --- a/Mathlib/Data/Sum/Basic.lean +++ b/Mathlib/Data/Sum/Basic.lean @@ -35,7 +35,7 @@ theorem sum_rec_congr (P : α ⊕ β → Sort*) (f : ∀ i, P (inl i)) (g : ∀ section get -variable {x y : α ⊕ β} +variable {x : α ⊕ β} theorem eq_left_iff_getLeft_eq {a : α} : x = inl a ↔ ∃ h, x.getLeft h = a := by cases x <;> simp diff --git a/Mathlib/Logic/Lemmas.lean b/Mathlib/Logic/Lemmas.lean index 1056a7ffc156f..3e92a9dc21060 100644 --- a/Mathlib/Logic/Lemmas.lean +++ b/Mathlib/Logic/Lemmas.lean @@ -24,7 +24,7 @@ theorem iff_right_comm {a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b) protected alias ⟨HEq.eq, Eq.heq⟩ := heq_iff_eq -variable {α : Sort*} {p q r : Prop} [Decidable p] [Decidable q] {a b c : α} +variable {α : Sort*} {p q : Prop} [Decidable p] [Decidable q] {a b c : α} theorem dite_dite_distrib_left {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} : (dite p a fun hp ↦ dite q (b hp) (c hp)) = diff --git a/Mathlib/Order/BoundedOrder.lean b/Mathlib/Order/BoundedOrder.lean index 7850b239ce06a..985a68cdf8068 100644 --- a/Mathlib/Order/BoundedOrder.lean +++ b/Mathlib/Order/BoundedOrder.lean @@ -353,7 +353,7 @@ theorem OrderBot.ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : Par section SemilatticeSupTop -variable [SemilatticeSup α] [OrderTop α] {a : α} +variable [SemilatticeSup α] [OrderTop α] -- Porting note: Not simp because simp can prove it theorem top_sup_eq (a : α) : ⊤ ⊔ a = ⊤ := @@ -400,7 +400,7 @@ end SemilatticeInfTop section SemilatticeInfBot -variable [SemilatticeInf α] [OrderBot α] {a : α} +variable [SemilatticeInf α] [OrderBot α] -- Porting note: Not simp because simp can prove it lemma bot_inf_eq (a : α) : ⊥ ⊓ a = ⊥ := inf_of_le_left bot_le diff --git a/Mathlib/Order/Disjoint.lean b/Mathlib/Order/Disjoint.lean index 29678782f984f..98aa260c7eaa2 100644 --- a/Mathlib/Order/Disjoint.lean +++ b/Mathlib/Order/Disjoint.lean @@ -108,7 +108,7 @@ end PartialBoundedOrder section SemilatticeInfBot -variable [SemilatticeInf α] [OrderBot α] {a b c d : α} +variable [SemilatticeInf α] [OrderBot α] {a b c : α} theorem disjoint_iff_inf_le : Disjoint a b ↔ a ⊓ b ≤ ⊥ := ⟨fun hd ↦ hd inf_le_left inf_le_right, fun h _ ha hb ↦ (le_inf ha hb).trans h⟩ @@ -267,7 +267,7 @@ end PartialBoundedOrder section SemilatticeSupTop -variable [SemilatticeSup α] [OrderTop α] {a b c d : α} +variable [SemilatticeSup α] [OrderTop α] {a b c : α} theorem codisjoint_iff_le_sup : Codisjoint a b ↔ ⊤ ≤ a ⊔ b := @disjoint_iff_inf_le αᵒᵈ _ _ _ _ @@ -401,7 +401,7 @@ namespace IsCompl section BoundedPartialOrder -variable [PartialOrder α] [BoundedOrder α] {x y z : α} +variable [PartialOrder α] [BoundedOrder α] {x y : α} @[symm] protected theorem symm (h : IsCompl x y) : IsCompl y x := @@ -419,7 +419,7 @@ end BoundedPartialOrder section BoundedLattice -variable [Lattice α] [BoundedOrder α] {x y z : α} +variable [Lattice α] [BoundedOrder α] {x y : α} theorem of_le (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y := ⟨disjoint_iff_inf_le.mpr h₁, codisjoint_iff_le_sup.mpr h₂⟩ diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 76070c79b4151..8383d090d9c12 100644 --- a/Mathlib/Order/Lattice.lean +++ b/Mathlib/Order/Lattice.lean @@ -528,7 +528,7 @@ def Lattice.mk' {α : Type*} [Sup α] [Inf α] (sup_comm : ∀ a b : α, a ⊔ b section Lattice -variable [Lattice α] {a b c d : α} +variable [Lattice α] {a b c : α} theorem inf_le_sup : a ⊓ b ≤ a ⊔ b := inf_le_left.trans le_sup_left diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index 3292cce1aeeec..d2edb733b59cc 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -1025,7 +1025,7 @@ theorem Subtype.strictMono_coe [Preorder α] (t : Set α) : section Preorder -variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} {a b : α} +variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} theorem monotone_fst : Monotone (@Prod.fst α β) := fun _ _ ↦ And.left From 99275e79b76f20b3dbb9e5653d48d337b220deff Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 3 Oct 2024 19:39:40 +0200 Subject: [PATCH 2/2] fewer variables --- Mathlib/Algebra/Algebra/Spectrum.lean | 2 +- Mathlib/Algebra/Polynomial/Smeval.lean | 2 +- .../Geometry/Manifold/LocalInvariantProperties.lean | 2 +- Mathlib/RingTheory/Nilpotent/Lemmas.lean | 10 ---------- 4 files changed, 3 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Spectrum.lean b/Mathlib/Algebra/Algebra/Spectrum.lean index 2b7e28f8e2c29..65c69f706fb00 100644 --- a/Mathlib/Algebra/Algebra/Spectrum.lean +++ b/Mathlib/Algebra/Algebra/Spectrum.lean @@ -400,7 +400,7 @@ end CommSemiring section CommRing -variable {F R A B : Type*} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] +variable {F R A : Type*} [CommRing R] [Ring A] [Algebra R A] variable [FunLike F A R] [AlgHomClass F R A R] local notation "σ" => spectrum R diff --git a/Mathlib/Algebra/Polynomial/Smeval.lean b/Mathlib/Algebra/Polynomial/Smeval.lean index 2eb2eecb587a6..d24a7089bfc93 100644 --- a/Mathlib/Algebra/Polynomial/Smeval.lean +++ b/Mathlib/Algebra/Polynomial/Smeval.lean @@ -180,7 +180,7 @@ the defining structures independently. For non-associative power-associative al octonions), we replace the `[Semiring S]` with `[NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S]`. -/ -variable (R : Type*) [Semiring R] {p : R[X]} (r : R) (p q : R[X]) {S : Type*} +variable (R : Type*) [Semiring R] (r : R) (p q : R[X]) {S : Type*} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x := by diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean index 9feae63ffc666..5ea4b4a42e6b8 100644 --- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean +++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean @@ -68,7 +68,7 @@ structure LocalInvariantProp (P : (H → H') → Set H → H → Prop) : Prop wh left_invariance' : ∀ {s x f} {e' : PartialHomeomorph H' H'}, e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (e' ∘ f) s x -variable {G G'} {P : (H → H') → Set H → H → Prop} {s t u : Set H} {x : H} +variable {G G'} {P : (H → H') → Set H → H → Prop} variable (hG : G.LocalInvariantProp G' P) include hG diff --git a/Mathlib/RingTheory/Nilpotent/Lemmas.lean b/Mathlib/RingTheory/Nilpotent/Lemmas.lean index d5d61f66838de..a26835374afce 100644 --- a/Mathlib/RingTheory/Nilpotent/Lemmas.lean +++ b/Mathlib/RingTheory/Nilpotent/Lemmas.lean @@ -31,16 +31,6 @@ theorem isRadical_iff_span_singleton [CommSemiring R] : simp_rw [IsRadical, ← Ideal.mem_span_singleton] exact forall_swap.trans (forall_congr' fun r => exists_imp.symm) -namespace Commute - -section Semiring - -variable [Semiring R] (h_comm : Commute x y) - -end Semiring - -end Commute - section CommSemiring variable [CommSemiring R] {x y : R}