From 9f502c28baa1e9a8197bd0027eb6bfedc9e7fd3c Mon Sep 17 00:00:00 2001 From: damiano Date: Mon, 30 Sep 2024 00:42:10 +0000 Subject: [PATCH] chore: remove some unused variables (#17261) Inspired by #17178 and found by a linter. --- Mathlib/Algebra/Field/Basic.lean | 2 +- Mathlib/Algebra/Group/Defs.lean | 4 ++-- Mathlib/Algebra/Group/Equiv/Basic.lean | 1 - Mathlib/Algebra/Group/Semiconj/Units.lean | 2 +- Mathlib/Algebra/GroupWithZero/Basic.lean | 4 ++-- Mathlib/Algebra/GroupWithZero/Commute.lean | 4 ++-- Mathlib/Algebra/GroupWithZero/InjSurj.lean | 2 +- Mathlib/Algebra/GroupWithZero/Semiconj.lean | 2 +- Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean | 1 - Mathlib/Algebra/Module/BigOperators.lean | 2 +- Mathlib/Algebra/Polynomial/Induction.lean | 5 ++--- Mathlib/Algebra/Ring/Basic.lean | 9 +-------- Mathlib/Algebra/Ring/Commute.lean | 4 ++-- Mathlib/Algebra/Ring/Hom/Defs.lean | 4 +--- Mathlib/Algebra/Ring/Semiconj.lean | 6 +++--- Mathlib/Algebra/Ring/Units.lean | 2 +- Mathlib/Control/Basic.lean | 2 -- Mathlib/Control/Lawful.lean | 2 +- Mathlib/Data/Subtype.lean | 2 +- Mathlib/Lean/PrettyPrinter/Delaborator.lean | 7 ------- Mathlib/Logic/Basic.lean | 7 +++---- Mathlib/Logic/Equiv/Basic.lean | 2 -- Mathlib/Logic/Function/Conjugate.lean | 2 +- Mathlib/Logic/Relator.lean | 4 ++-- Mathlib/Logic/Unique.lean | 1 - Mathlib/Order/Basic.lean | 2 +- Mathlib/Order/Defs.lean | 1 - Mathlib/Order/Interval/Finset/Basic.lean | 8 ++++---- Mathlib/Order/Max.lean | 2 +- Mathlib/Order/SuccPred/Basic.lean | 2 +- Mathlib/Probability/Kernel/Disintegration/Integral.lean | 4 ++-- Mathlib/Topology/AlexandrovDiscrete.lean | 2 -- Mathlib/Topology/MetricSpace/Infsep.lean | 6 +++--- Mathlib/Topology/MetricSpace/ShrinkingLemma.lean | 2 +- 34 files changed, 42 insertions(+), 70 deletions(-) diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean index 570a5278b9b56..fe9961bb0230a 100644 --- a/Mathlib/Algebra/Field/Basic.lean +++ b/Mathlib/Algebra/Field/Basic.lean @@ -167,7 +167,7 @@ end DivisionRing section Semifield -variable [Semifield K] {a b c d : K} +variable [Semifield K] {a b d : K} theorem div_add_div (a : K) (c : K) (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d) := diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 810e4ced7a7a0..cd436c8a8fdfc 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -552,7 +552,7 @@ instance AddMonoid.toNatSMul {M : Type*} [AddMonoid M] : SMul ℕ M := attribute [to_additive existing toNatSMul] Monoid.toNatPow section Monoid -variable {M : Type*} [Monoid M] {a b c : M} {m n : ℕ} +variable {M : Type*} [Monoid M] {a b c : M} @[to_additive (attr := simp) nsmul_eq_smul] theorem npow_eq_pow (n : ℕ) (x : M) : Monoid.npow n x = x ^ n := @@ -879,7 +879,7 @@ theorem exists_zpow_surjective (G : Type*) [Pow G ℤ] [IsCyclic G] : section DivInvMonoid -variable [DivInvMonoid G] {a b : G} +variable [DivInvMonoid G] @[to_additive (attr := simp) zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) : DivInvMonoid.zpow n x = x ^ n := diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean index 242b93f9ace47..ad1eee7b26f9c 100644 --- a/Mathlib/Algebra/Group/Equiv/Basic.lean +++ b/Mathlib/Algebra/Group/Equiv/Basic.lean @@ -130,7 +130,6 @@ instance (priority := 100) instMonoidHomClass _ = e (EquivLike.inv e (1 : N)) := by rw [← map_mul, one_mul] _ = 1 := EquivLike.right_inv e 1 } -variable [EquivLike F α β] variable {F} @[to_additive (attr := simp)] diff --git a/Mathlib/Algebra/Group/Semiconj/Units.lean b/Mathlib/Algebra/Group/Semiconj/Units.lean index b842e2c11bc3b..5a31a5e5130e9 100644 --- a/Mathlib/Algebra/Group/Semiconj/Units.lean +++ b/Mathlib/Algebra/Group/Semiconj/Units.lean @@ -32,7 +32,7 @@ assert_not_exists DenselyOrdered open scoped Int -variable {M G : Type*} +variable {M : Type*} namespace SemiconjBy diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean index 8b4b08535c105..26f0af2649201 100644 --- a/Mathlib/Algebra/GroupWithZero/Basic.lean +++ b/Mathlib/Algebra/GroupWithZero/Basic.lean @@ -291,7 +291,7 @@ end GroupWithZero section GroupWithZero -variable [GroupWithZero G₀] {a b c : G₀} +variable [GroupWithZero G₀] {a : G₀} @[simp] theorem zero_div (a : G₀) : 0 / a = 0 := by rw [div_eq_mul_inv, zero_mul] @@ -421,7 +421,7 @@ end GroupWithZero section CommGroupWithZero -variable [CommGroupWithZero G₀] {a b c d : G₀} +variable [CommGroupWithZero G₀] theorem div_mul_eq_mul_div₀ (a b c : G₀) : a / c * b = a * b / c := by simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹] diff --git a/Mathlib/Algebra/GroupWithZero/Commute.lean b/Mathlib/Algebra/GroupWithZero/Commute.lean index 59423cb09016f..24a2a0afe674b 100644 --- a/Mathlib/Algebra/GroupWithZero/Commute.lean +++ b/Mathlib/Algebra/GroupWithZero/Commute.lean @@ -14,7 +14,7 @@ import Mathlib.Tactic.Nontriviality assert_not_exists DenselyOrdered -variable {α M₀ G₀ M₀' G₀' F F' : Type*} +variable {M₀ G₀ : Type*} variable [MonoidWithZero M₀] namespace Ring @@ -83,7 +83,7 @@ theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c := end Commute section GroupWithZero -variable {G₀ : Type*} [GroupWithZero G₀] {a : G₀} {m n : ℕ} +variable {G₀ : Type*} [GroupWithZero G₀] theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m := (Commute.refl a).inv_left₀.pow_pow m n diff --git a/Mathlib/Algebra/GroupWithZero/InjSurj.lean b/Mathlib/Algebra/GroupWithZero/InjSurj.lean index d7a7ff367118a..26278384167c1 100644 --- a/Mathlib/Algebra/GroupWithZero/InjSurj.lean +++ b/Mathlib/Algebra/GroupWithZero/InjSurj.lean @@ -19,7 +19,7 @@ variable {M₀ G₀ M₀' G₀' : Type*} section MulZeroClass -variable [MulZeroClass M₀] {a b : M₀} +variable [MulZeroClass M₀] /-- Pull back a `MulZeroClass` instance along an injective function. See note [reducible non-instances]. -/ diff --git a/Mathlib/Algebra/GroupWithZero/Semiconj.lean b/Mathlib/Algebra/GroupWithZero/Semiconj.lean index f3798456188e4..0dfc56212073d 100644 --- a/Mathlib/Algebra/GroupWithZero/Semiconj.lean +++ b/Mathlib/Algebra/GroupWithZero/Semiconj.lean @@ -13,7 +13,7 @@ import Mathlib.Algebra.Group.Semiconj.Units assert_not_exists DenselyOrdered -variable {α M₀ G₀ M₀' G₀' F F' : Type*} +variable {G₀ : Type*} namespace SemiconjBy diff --git a/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean b/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean index c413ab0a165b8..bbf5c0a8dc88f 100644 --- a/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean +++ b/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean @@ -94,7 +94,6 @@ def invMonoidWithZeroHom {G₀ : Type*} [CommGroupWithZero G₀] : G₀ →*₀ namespace Units variable [GroupWithZero G₀] -variable {a b : G₀} @[simp] theorem smul_mk0 {α : Type*} [SMul G₀ α] {g : G₀} (hg : g ≠ 0) (a : α) : mk0 g hg • a = g • a := diff --git a/Mathlib/Algebra/Module/BigOperators.lean b/Mathlib/Algebra/Module/BigOperators.lean index 8b68d57357fd4..d15e7274ec57a 100644 --- a/Mathlib/Algebra/Module/BigOperators.lean +++ b/Mathlib/Algebra/Module/BigOperators.lean @@ -15,7 +15,7 @@ variable {ι κ α β R M : Type*} section AddCommMonoid -variable [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x y : M) +variable [Semiring R] [AddCommMonoid M] [Module R M] theorem List.sum_smul {l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum := map_list_sum ((smulAddHom R M).flip x) l diff --git a/Mathlib/Algebra/Polynomial/Induction.lean b/Mathlib/Algebra/Polynomial/Induction.lean index 4ba0e2bf397db..a4fc244b867ab 100644 --- a/Mathlib/Algebra/Polynomial/Induction.lean +++ b/Mathlib/Algebra/Polynomial/Induction.lean @@ -26,12 +26,11 @@ open Polynomial universe u v w x y z -variable {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z} {a b : R} - {m n : ℕ} +variable {R : Type u} section Semiring -variable [Semiring R] {p q r : R[X]} +variable [Semiring R] @[elab_as_elim] protected theorem induction_on {M : R[X] → Prop} (p : R[X]) (h_C : ∀ a, M (C a)) diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean index 4ae5170c85619..fd10db100aadd 100644 --- a/Mathlib/Algebra/Ring/Basic.lean +++ b/Mathlib/Algebra/Ring/Basic.lean @@ -40,13 +40,6 @@ def mulRight [Distrib R] (r : R) : AddHom R R where end AddHom -section AddHomClass - -variable {α β F : Type*} [NonAssocSemiring α] [NonAssocSemiring β] - [FunLike F α β] [AddHomClass F α β] - -end AddHomClass - namespace AddMonoidHom /-- Left multiplication by an element of a (semi)ring is an `AddMonoidHom` -/ @@ -105,7 +98,7 @@ end HasDistribNeg section NonUnitalCommRing -variable {α : Type*} [NonUnitalCommRing α] {a b c : α} +variable {α : Type*} [NonUnitalCommRing α] attribute [local simp] add_assoc add_comm add_left_comm mul_comm diff --git a/Mathlib/Algebra/Ring/Commute.lean b/Mathlib/Algebra/Ring/Commute.lean index 6793e2df1e30d..54cf0da485262 100644 --- a/Mathlib/Algebra/Ring/Commute.lean +++ b/Mathlib/Algebra/Ring/Commute.lean @@ -75,7 +75,7 @@ end section -variable [MulOneClass R] [HasDistribNeg R] {a : R} +variable [MulOneClass R] [HasDistribNeg R] -- Porting note (#10618): no longer needs to be `@[simp]` since `simp` can prove it. -- @[simp] @@ -147,7 +147,7 @@ alias neg_one_pow_two := neg_one_sq end HasDistribNeg section Ring -variable [Ring R] {a b : R} {n : ℕ} +variable [Ring R] {a : R} {n : ℕ} @[simp] lemma neg_one_pow_mul_eq_zero_iff : (-1) ^ n * a = 0 ↔ a = 0 := by rcases neg_one_pow_eq_or R n with h | h <;> simp [h] diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index 6ffa90e13d5da..86672a2bb1c98 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -153,7 +153,6 @@ end coe section variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] -variable (f : α →ₙ+* β) {x y : α} @[ext] theorem ext ⦃f g : α →ₙ+* β⦄ : (∀ x, f x = g x) → f = g := @@ -225,7 +224,6 @@ theorem coe_comp (g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = g @[simp] theorem comp_apply (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : g.comp f x = g (f x) := rfl -variable (g : β →ₙ+* γ) (f : α →ₙ+* β) @[simp] theorem coe_comp_addMonoidHom (g : β →ₙ+* γ) (f : α →ₙ+* β) : @@ -441,7 +439,7 @@ end coe section -variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β) {x y : α} +variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β) protected theorem congr_fun {f g : α →+* β} (h : f = g) (x : α) : f x = g x := DFunLike.congr_fun h x diff --git a/Mathlib/Algebra/Ring/Semiconj.lean b/Mathlib/Algebra/Ring/Semiconj.lean index 7ca35cfbf5af9..8b20e68a71a06 100644 --- a/Mathlib/Algebra/Ring/Semiconj.lean +++ b/Mathlib/Algebra/Ring/Semiconj.lean @@ -19,9 +19,9 @@ For the definitions of semirings and rings see `Mathlib.Algebra.Ring.Defs`. -/ -universe u v w x +universe u -variable {α : Type u} {β : Type v} {γ : Type w} {R : Type x} +variable {R : Type u} open Function @@ -59,7 +59,7 @@ end section -variable [MulOneClass R] [HasDistribNeg R] {a x y : R} +variable [MulOneClass R] [HasDistribNeg R] -- Porting note: `simpNF` told me to remove `simp` attribute theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) := diff --git a/Mathlib/Algebra/Ring/Units.lean b/Mathlib/Algebra/Ring/Units.lean index fbcb29f67829f..3e177e160d871 100644 --- a/Mathlib/Algebra/Ring/Units.lean +++ b/Mathlib/Algebra/Ring/Units.lean @@ -49,7 +49,7 @@ end HasDistribNeg section Ring -variable [Ring α] {a b : α} +variable [Ring α] -- Needs to have higher simp priority than divp_add_divp. 1000 is the default priority. @[field_simps 1010] diff --git a/Mathlib/Control/Basic.lean b/Mathlib/Control/Basic.lean index 0df3671f162c4..9f03e34b31c1e 100644 --- a/Mathlib/Control/Basic.lean +++ b/Mathlib/Control/Basic.lean @@ -214,8 +214,6 @@ class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulAppl open Functor -variable {m} - theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ} (a : m α) (b : m β) {f : α → β → γ} : f <$> a <*> b = flip f <$> b <*> a := diff --git a/Mathlib/Control/Lawful.lean b/Mathlib/Control/Lawful.lean index 769ec2655f4ec..ce4807b4cde66 100644 --- a/Mathlib/Control/Lawful.lean +++ b/Mathlib/Control/Lawful.lean @@ -48,7 +48,7 @@ end StateT namespace ExceptT -variable {α β ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α) +variable {α ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α) -- Porting note: This is proven by proj reduction in Lean 3. @[simp] diff --git a/Mathlib/Data/Subtype.lean b/Mathlib/Data/Subtype.lean index 48aaa0d08f165..0583ba40e98cc 100644 --- a/Mathlib/Data/Subtype.lean +++ b/Mathlib/Data/Subtype.lean @@ -207,7 +207,7 @@ end Subtype namespace Subtype /-! Some facts about sets, which require that `α` is a type. -/ -variable {α β γ : Type*} {p : α → Prop} +variable {α : Type*} @[simp] theorem coe_prop {S : Set α} (a : { a // a ∈ S }) : ↑a ∈ S := diff --git a/Mathlib/Lean/PrettyPrinter/Delaborator.lean b/Mathlib/Lean/PrettyPrinter/Delaborator.lean index bcc547afa2239..557bdf947198a 100644 --- a/Mathlib/Lean/PrettyPrinter/Delaborator.lean +++ b/Mathlib/Lean/PrettyPrinter/Delaborator.lean @@ -14,13 +14,6 @@ namespace Lean.PrettyPrinter.Delaborator open Lean.Meta Lean.SubExpr SubExpr -namespace SubExpr - -variable {α : Type} [Inhabited α] -variable {m : Type → Type} [Monad m] - -end SubExpr - /-- Assuming the current expression in a lambda or pi, descend into the body using an unused name generated from the binder's name. Provides `d` with both `Syntax` for the bound name as an identifier diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index b33cfc478250f..8fd66baa31e7d 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -435,8 +435,7 @@ end Equality section Quantifiers section Dependent -variable {α : Sort*} {β : α → Sort*} {γ : ∀ a, β a → Sort*} {δ : ∀ a b, γ a b → Sort*} - {ε : ∀ a b c, δ a b c → Sort*} +variable {α : Sort*} {β : α → Sort*} {γ : ∀ a, β a → Sort*} theorem pi_congr {β' : α → Sort _} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a := (funext h : β = β') ▸ rfl @@ -462,7 +461,7 @@ theorem Exists₃.imp {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c end Dependent -variable {α β : Sort*} {p q : α → Prop} +variable {α β : Sort*} {p : α → Prop} theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y := ⟨fun f x y ↦ f y x, fun f x y ↦ f y x⟩ @@ -745,7 +744,7 @@ noncomputable def Exists.classicalRecOn {α : Sort*} {p : α → Prop} (h : ∃ /-! ### Declarations about bounded quantifiers -/ section BoundedQuantifiers -variable {α : Sort*} {r p q : α → Prop} {P Q : ∀ x, p x → Prop} {b : Prop} +variable {α : Sort*} {r p q : α → Prop} {P Q : ∀ x, p x → Prop} theorem bex_def : (∃ (x : _) (_ : p x), q x) ↔ ∃ x, p x ∧ q x := ⟨fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩, fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩⟩ diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index d68413363ef4b..d8c4acbd7d587 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -1580,8 +1580,6 @@ namespace Equiv section -variable (P : α → Sort w) (e : α ≃ β) - /-- Transport dependent functions through an equivalence of the base space. -/ @[simps apply, simps (config := .lemmasOnly) symm_apply] diff --git a/Mathlib/Logic/Function/Conjugate.lean b/Mathlib/Logic/Function/Conjugate.lean index 76dc5be2b2999..69098eb142cbf 100644 --- a/Mathlib/Logic/Function/Conjugate.lean +++ b/Mathlib/Logic/Function/Conjugate.lean @@ -31,7 +31,7 @@ def Semiconj (f : α → β) (ga : α → α) (gb : β → β) : Prop := namespace Semiconj -variable {f fab : α → β} {fbc : β → γ} {ga ga' : α → α} {gb gb' : β → β} {gc gc' : γ → γ} +variable {f fab : α → β} {fbc : β → γ} {ga ga' : α → α} {gb gb' : β → β} {gc : γ → γ} /-- Definition of `Function.Semiconj` in terms of functional equality. -/ lemma _root_.Function.semiconj_iff_comp_eq : Semiconj f ga gb ↔ f ∘ ga = gb ∘ f := funext_iff.symm diff --git a/Mathlib/Logic/Relator.lean b/Mathlib/Logic/Relator.lean index 7e0f0e054c1ac..83b0b7e2046b8 100644 --- a/Mathlib/Logic/Relator.lean +++ b/Mathlib/Logic/Relator.lean @@ -96,8 +96,8 @@ lemma rel_not : (Iff ⇒ Iff) Not Not := lemma bi_total_eq {α : Type u₁} : Relator.BiTotal (@Eq α) := { left := fun a => ⟨a, rfl⟩, right := fun a => ⟨a, rfl⟩ } -variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} -variable {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop} +variable {α : Type*} {β : Type*} {γ : Type*} +variable {r : α → β → Prop} lemma LeftUnique.flip (h : LeftUnique r) : RightUnique (flip r) := fun _ _ _ h₁ h₂ => h h₁ h₂ diff --git a/Mathlib/Logic/Unique.lean b/Mathlib/Logic/Unique.lean index 145bc1d43f421..678d68e2ff016 100644 --- a/Mathlib/Logic/Unique.lean +++ b/Mathlib/Logic/Unique.lean @@ -247,7 +247,6 @@ instance {α} [IsEmpty α] : Unique (Option α) := end Option section Subtype -variable {α : Sort u} instance Unique.subtypeEq (y : α) : Unique { x // x = y } where default := ⟨y, rfl⟩ diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean index 628c729ea2354..08b21b2de4986 100644 --- a/Mathlib/Order/Basic.lean +++ b/Mathlib/Order/Basic.lean @@ -186,7 +186,7 @@ end namespace Eq -variable [Preorder α] {x y z : α} +variable [Preorder α] {x y : α} /-- If `x = y` then `y ≤ x`. Note: this lemma uses `y ≤ x` instead of `x ≥ y`, because `le` is used almost exclusively in mathlib. -/ diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean index c53c3b994e122..93e79ca56a566 100644 --- a/Mathlib/Order/Defs.lean +++ b/Mathlib/Order/Defs.lean @@ -552,7 +552,6 @@ lemma max_lt (h₁ : a < c) (h₂ : b < c) : max a b < c := by cases le_total a b <;> simp [max_eq_left, max_eq_right, *] section Ord -variable {o : Ordering} lemma compare_lt_iff_lt : compare a b = .lt ↔ a < b := by rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq] diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean index 8964e28ae8b2a..53ccb40f79265 100644 --- a/Mathlib/Order/Interval/Finset/Basic.lean +++ b/Mathlib/Order/Interval/Finset/Basic.lean @@ -683,7 +683,7 @@ variable [LinearOrder α] section LocallyFiniteOrder -variable [LocallyFiniteOrder α] {a b : α} +variable [LocallyFiniteOrder α] theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by @@ -790,7 +790,7 @@ end LinearOrder section Lattice -variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α} +variable [Lattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ x : α} theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding := Icc_toDual _ _ @@ -862,7 +862,7 @@ end Lattice section DistribLattice -variable [DistribLattice α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α} +variable [DistribLattice α] [LocallyFiniteOrder α] {a b c : α} theorem eq_of_mem_uIcc_of_mem_uIcc : a ∈ [[b, c]] → b ∈ [[a, c]] → a = b := by simp_rw [mem_uIcc] @@ -883,7 +883,7 @@ end DistribLattice section LinearOrder -variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c x : α} +variable [LinearOrder α] [LocallyFiniteOrder α] {a a₁ a₂ b b₁ b₂ c : α} theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] := rfl diff --git a/Mathlib/Order/Max.lean b/Mathlib/Order/Max.lean index b355050f7aea9..61f5b1037d505 100644 --- a/Mathlib/Order/Max.lean +++ b/Mathlib/Order/Max.lean @@ -356,7 +356,7 @@ end PartialOrder section Prod -variable [Preorder α] [Preorder β] {a a₁ a₂ : α} {b b₁ b₂ : β} {x y : α × β} +variable [Preorder α] [Preorder β] {a : α} {b : β} {x : α × β} theorem IsBot.prod_mk (ha : IsBot a) (hb : IsBot b) : IsBot (a, b) := fun _ => ⟨ha _, hb _⟩ diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean index d8d173cca893a..aef647a6f8d31 100644 --- a/Mathlib/Order/SuccPred/Basic.lean +++ b/Mathlib/Order/SuccPred/Basic.lean @@ -927,7 +927,7 @@ lemma gc_pred_succ : GaloisConnection (pred : α → α) succ := fun _ _ ↦ pre end Preorder -variable [PartialOrder α] [SuccOrder α] [PredOrder α] {a b : α} +variable [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α} @[simp] theorem succ_pred_of_not_isMin (h : ¬IsMin a) : succ (pred a) = a := diff --git a/Mathlib/Probability/Kernel/Disintegration/Integral.lean b/Mathlib/Probability/Kernel/Disintegration/Integral.lean index f712bc83a22b8..026257adcaf92 100644 --- a/Mathlib/Probability/Kernel/Disintegration/Integral.lean +++ b/Mathlib/Probability/Kernel/Disintegration/Integral.lean @@ -146,12 +146,12 @@ end ProbabilityTheory namespace MeasureTheory.Measure -variable {α β Ω : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} +variable {β Ω : Type*} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] section Lintegral -variable [CountableOrCountablyGenerated α β] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] +variable {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {f : β × Ω → ℝ≥0∞} lemma lintegral_condKernel_mem {s : Set (β × Ω)} (hs : MeasurableSet s) : diff --git a/Mathlib/Topology/AlexandrovDiscrete.lean b/Mathlib/Topology/AlexandrovDiscrete.lean index b03c9b2cb45eb..517c0d910bfeb 100644 --- a/Mathlib/Topology/AlexandrovDiscrete.lean +++ b/Mathlib/Topology/AlexandrovDiscrete.lean @@ -114,8 +114,6 @@ lemma closure_sUnion (S : Set (Set α)) : closure (⋃₀ S) = ⋃ s ∈ S, clos end AlexandrovDiscrete -variable {s t : Set α} {a x y : α} - lemma Inducing.alexandrovDiscrete [AlexandrovDiscrete α] {f : β → α} (h : Inducing f) : AlexandrovDiscrete β where isOpen_sInter S hS := by diff --git a/Mathlib/Topology/MetricSpace/Infsep.lean b/Mathlib/Topology/MetricSpace/Infsep.lean index 027a2e3139f9c..e451f9e7817b3 100644 --- a/Mathlib/Topology/MetricSpace/Infsep.lean +++ b/Mathlib/Topology/MetricSpace/Infsep.lean @@ -171,7 +171,7 @@ end EDist section PseudoEMetricSpace -variable [PseudoEMetricSpace α] {x y z : α} {s t : Set α} +variable [PseudoEMetricSpace α] {x y z : α} {s : Set α} theorem einfsep_pair (hxy : x ≠ y) : ({x, y} : Set α).einfsep = edist x y := by nth_rw 1 [← min_self (edist x y)] @@ -238,7 +238,7 @@ end PseudoMetricSpace section EMetricSpace -variable [EMetricSpace α] {x y z : α} {s t : Set α} {C : ℝ≥0∞} {sC : Set ℝ≥0∞} +variable [EMetricSpace α] {s : Set α} theorem einfsep_pos_of_finite [Finite s] : 0 < s.einfsep := by cases nonempty_fintype s @@ -312,7 +312,7 @@ end EDist section PseudoEMetricSpace -variable [PseudoEMetricSpace α] {x y : α} {s : Set α} +variable [PseudoEMetricSpace α] {x y : α} theorem infsep_pair_eq_toReal : ({x, y} : Set α).infsep = (edist x y).toReal := by by_cases hxy : x = y diff --git a/Mathlib/Topology/MetricSpace/ShrinkingLemma.lean b/Mathlib/Topology/MetricSpace/ShrinkingLemma.lean index 058f2115e3541..b7b081e3fb55d 100644 --- a/Mathlib/Topology/MetricSpace/ShrinkingLemma.lean +++ b/Mathlib/Topology/MetricSpace/ShrinkingLemma.lean @@ -27,7 +27,7 @@ open Set Metric open Topology variable {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {c : ι → α} -variable {x : α} {r : ℝ} {s : Set α} +variable {s : Set α} /-- **Shrinking lemma** for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by