Merge branch 'master' into FR_clean_setoid_r

Mathlib/Analysis/Convex/Between.lean

@@ -5,6 +5,7 @@ Authors: Joseph Myers
 -/
 import Mathlib.Algebra.CharP.Invertible
 import Mathlib.Algebra.Order.Interval.Set.Group
+import Mathlib.Analysis.Convex.Basic
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import Mathlib.Tactic.FieldSimp
@@ -128,6 +129,14 @@ variable {R}
 lemma mem_segment_iff_wbtw {x y z : V} : y ∈ segment R x z ↔ Wbtw R x y z := by
   rw [Wbtw, affineSegment_eq_segment]
 
+alias ⟨_, Wbtw.mem_segment⟩ := mem_segment_iff_wbtw
+
+lemma Convex.mem_of_wbtw {p₀ p₁ p₂ : V} {s : Set V} (hs : Convex R s) (h₀₁₂ : Wbtw R p₀ p₁ p₂)
+    (h₀ : p₀ ∈ s) (h₂ : p₂ ∈ s) : p₁ ∈ s := hs.segment_subset h₀ h₂ h₀₁₂.mem_segment
+
+lemma AffineSubspace.mem_of_wbtw {s : AffineSubspace R P} {x y z : P} (hxyz : Wbtw R x y z)
+    (hx : x ∈ s) (hz : z ∈ s) : y ∈ s := by obtain ⟨ε, -, rfl⟩ := hxyz; exact lineMap_mem _ hx hz
+
 theorem Wbtw.map {x y z : P} (h : Wbtw R x y z) (f : P →ᵃ[R] P') : Wbtw R (f x) (f y) (f z) := by
   rw [Wbtw, ← affineSegment_image]
   exact Set.mem_image_of_mem _ h
@@ -574,7 +583,7 @@ end LinearOrderedRing
 
 section LinearOrderedField
 
-variable [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P]
+variable [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {x y z : P}
 variable {R}
 
 theorem wbtw_iff_left_eq_or_right_mem_image_Ici {x y z : P} :
@@ -653,6 +662,12 @@ theorem Sbtw.left_mem_image_Ioi {x y z : P} (h : Sbtw R x y z) :
 theorem Sbtw.left_mem_affineSpan {x y z : P} (h : Sbtw R x y z) : x ∈ line[R, z, y] :=
   h.symm.right_mem_affineSpan
 
+lemma AffineSubspace.right_mem_of_wbtw {s : AffineSubspace R P} (hxyz : Wbtw R x y z) (hx : x ∈ s)
+    (hy : y ∈ s) (hxy : x ≠ y) : z ∈ s := by
+  obtain ⟨ε, -, rfl⟩ := hxyz
+  have hε : ε ≠ 0 := by rintro rfl; simp at hxy
+  simpa [hε] using lineMap_mem ε⁻¹ hx hy
+
 theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁)
     (hr₂ : r₁ ≤ r₂) : Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) := by
   refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩

Mathlib/CategoryTheory/Iso.lean

@@ -332,7 +332,7 @@ instance id (X : C) : IsIso (𝟙 X) := ⟨⟨𝟙 X, by simp⟩⟩
 @[deprecated (since := "2024-05-15")] alias of_iso := CategoryTheory.Iso.isIso_hom
 @[deprecated (since := "2024-05-15")] alias of_iso_inv := CategoryTheory.Iso.isIso_inv
 
-variable {f g : X ⟶ Y} {h : Y ⟶ Z}
+variable {f : X ⟶ Y} {h : Y ⟶ Z}
 
 instance inv_isIso [IsIso f] : IsIso (inv f) :=
   (asIso f).isIso_inv
@@ -509,7 +509,7 @@ theorem cancel_iso_inv_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y)
 
 section
 
-variable {D E : Type*} [Category D] [Category E] {X Y : C} (e : X ≅ Y)
+variable {D : Type*} [Category D] {X Y : C} (e : X ≅ Y)
 
 @[reassoc (attr := simp)]
 lemma map_hom_inv_id (F : C ⥤ D) :

Mathlib/CategoryTheory/NatTrans.lean

@@ -72,7 +72,7 @@ open CategoryTheory.Functor
 
 section
 
-variable {F G H I : C ⥤ D}
+variable {F G H : C ⥤ D}
 
 /-- `vcomp α β` is the vertical compositions of natural transformations. -/
 def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where

Mathlib/Data/List/Enum.lean

@@ -19,7 +19,7 @@ Any downstream users who can not easily adapt may remove the deprecations as nee
 
 namespace List
 
-variable {α β : Type*}
+variable {α : Type*}
 
 @[deprecated getElem?_enumFrom (since := "2024-08-15")]
 theorem get?_enumFrom (n) (l : List α) (m) :

Mathlib/Data/List/Infix.lean

@@ -25,11 +25,11 @@ All those (except `insert`) are defined in `Mathlib.Data.List.Defs`.
 * `l₁ <:+: l₂`: `l₁` is an infix of `l₂`.
 -/
 
-variable {α β : Type*}
+variable {α : Type*}
 
 namespace List
 
-variable {l l₁ l₂ l₃ : List α} {a b : α} {m n : ℕ}
+variable {l l₁ l₂ : List α} {a b : α}
 
 /-! ### prefix, suffix, infix -/
 

Mathlib/Data/List/InsertNth.lean

@@ -19,9 +19,9 @@ open Nat hiding one_pos
 
 namespace List
 
-universe u v w
+universe u
 
-variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {l₁ l₂ : List α}
+variable {α : Type u}
 
 section InsertNth
 

Mathlib/Data/List/Pairwise.lean

@@ -29,7 +29,7 @@ open Nat Function
 
 namespace List
 
-variable {α β : Type*} {R S T : α → α → Prop} {a : α} {l : List α}
+variable {α β : Type*} {R : α → α → Prop} {l : List α}
 
 mk_iff_of_inductive_prop List.Pairwise List.pairwise_iff
 
@@ -69,9 +69,6 @@ theorem pairwise_of_reflexive_of_forall_ne {l : List α} {r : α → α → Prop
 
 /-! ### Pairwise filtering -/
 
-
-variable [DecidableRel R]
-
 alias ⟨_, Pairwise.pwFilter⟩ := pwFilter_eq_self
 
 -- Porting note: commented out

Mathlib/Data/Quot.lean

@@ -21,6 +21,7 @@ variable {α : Sort*} {β : Sort*}
 
 namespace Setoid
 
+-- Pretty print `@Setoid.r _ s a b` as `s a b`.
 run_cmd Lean.Elab.Command.liftTermElabM do
   Lean.Meta.registerCoercion ``Setoid.r
     (some { numArgs := 2, coercee := 1, type := .coeFun })

Mathlib/Data/Seq/Seq.lean

@@ -512,8 +512,6 @@ def zipWith (f : α → β → γ) (s₁ : Seq α) (s₂ : Seq β) : Seq γ :=
   ⟨fun n => Option.map₂ f (s₁.get? n) (s₂.get? n), fun {_} hn =>
     Option.map₂_eq_none_iff.2 <| (Option.map₂_eq_none_iff.1 hn).imp s₁.2 s₂.2⟩
 
-variable {s : Seq α} {s' : Seq β} {n : ℕ}
-
 @[simp]
 theorem get?_zipWith (f : α → β → γ) (s s' n) :
     (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n) :=

Mathlib/RingTheory/Binomial.lean

@@ -175,7 +175,7 @@ theorem ascPochhammer_smeval_cast (R : Type*) [Semiring R] {S : Type*} [NonAssoc
     simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
     simp only [nsmul_eq_mul, Nat.cast_id]
 
-variable {R S : Type*}
+variable {R : Type*}
 
 theorem ascPochhammer_smeval_eq_eval [Semiring R] (r : R) (n : ℕ) :
     (ascPochhammer ℕ n).smeval r = (ascPochhammer R n).eval r := by

Mathlib/RingTheory/Derivation/MapCoeffs.lean

@@ -22,7 +22,7 @@ open Polynomial Module
 namespace Derivation
 
 variable {R A M : Type*} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M]
-  [Module A M] [Module R M] (d : Derivation R A M) (a : A)
+  [Module A M] [Module R M] (d : Derivation R A M)
 
 /--
 The `R`-derivation from `A[X]` to `M[X]` which applies the derivative to each

Mathlib/RingTheory/Etale/Basic.lean

@@ -56,7 +56,6 @@ section
 
 variable {R : Type u} [CommSemiring R]
 variable {A : Type u} [Semiring A] [Algebra R A]
-variable {B : Type u} [CommRing B] [Algebra R B] (I : Ideal B)
 
 theorem iff_unramified_and_smooth :
     FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A := by

Mathlib/RingTheory/Idempotents.lean

@@ -214,8 +214,6 @@ A family `{ eᵢ }` of idempotent elements is complete orthogonal if
 structure CompleteOrthogonalIdempotents (e : I → R) extends OrthogonalIdempotents e : Prop where
   complete : ∑ i, e i = 1
 
-variable (he : CompleteOrthogonalIdempotents e)
-
 lemma CompleteOrthogonalIdempotents.unique_iff [Unique I] :
     CompleteOrthogonalIdempotents e ↔ e default = 1 := by
   rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique,

Mathlib/RingTheory/Jacobson.lean

@@ -144,7 +144,7 @@ section Localization
 
 open IsLocalization Submonoid
 
-variable {R S : Type*} [CommRing R] [CommRing S] {I : Ideal R}
+variable {R S : Type*} [CommRing R] [CommRing S]
 variable (y : R) [Algebra R S] [IsLocalization.Away y S]
 
 variable (S)

Mathlib/RingTheory/Kaehler/CotangentComplex.lean

@@ -157,10 +157,6 @@ lemma map_comp_cotangentComplex (f : Hom P P') :
 
 end CotangentSpace
 
-universe uT
-
-variable {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
-
 lemma Hom.sub_aux (f g : Hom P P') (x y) :
     letI := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
     f.toAlgHom (x * y) - g.toAlgHom (x * y) -

Mathlib/RingTheory/Kaehler/Polynomial.lean

@@ -16,7 +16,7 @@ open Algebra
 
 universe u v
 
-variable (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
+variable (R : Type u) [CommRing R]
 
 suppress_compilation
 

Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

@@ -146,7 +146,7 @@ variable (σ) in
 noncomputable def esymmAlgHomMonomial (t : Fin n →₀ ℕ) (r : R) :
     MvPolynomial σ R := (esymmAlgHom σ R n <| monomial t r).val
 
-variable {i : Fin n} {j : Fin m} {r : R}
+variable {i : Fin n} {r : R}
 
 lemma isSymmetric_esymmAlgHomMonomial (t : Fin n →₀ ℕ) (r : R) :
     (esymmAlgHomMonomial σ t r).IsSymmetric := (esymmAlgHom _ _ _ _).2

Mathlib/RingTheory/Smooth/Basic.lean

@@ -60,7 +60,7 @@ section
 
 variable {R : Type u} [CommSemiring R]
 variable {A : Type u} [Semiring A] [Algebra R A]
-variable {B : Type u} [CommRing B] [Algebra R B] (I : Ideal B)
+variable {B : Type u} [CommRing B] [Algebra R B]
 
 theorem exists_lift {B : Type u} [CommRing B] [_RB : Algebra R B]
     [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) :
@@ -187,9 +187,9 @@ end Comp
 
 section OfSurjective
 
-variable {R S : Type u} [CommRing R] [CommSemiring S]
+variable {R : Type u} [CommRing R]
 variable {P A : Type u} [CommRing A] [Algebra R A] [CommRing P] [Algebra R P]
-variable (I : Ideal P) (f : P →ₐ[R] A)
+variable (f : P →ₐ[R] A)
 
 theorem of_split [FormallySmooth R P] (g : A →ₐ[R] P ⧸ (RingHom.ker f.toRingHom) ^ 2)
     (hg : f.kerSquareLift.comp g = AlgHom.id R A) : FormallySmooth R A := by

Mathlib/RingTheory/WittVector/Basic.lean

@@ -49,7 +49,7 @@ noncomputable section
 
 open MvPolynomial Function
 
-variable {p : ℕ} {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
+variable {p : ℕ} {R S : Type*} [CommRing R] [CommRing S]
 variable {α : Type*} {β : Type*}
 
 local notation "𝕎" => WittVector p

Mathlib/RingTheory/WittVector/Frobenius.lean

@@ -48,7 +48,7 @@ and bundle it into `WittVector.frobenius`.
 
 namespace WittVector
 
-variable {p : ℕ} {R S : Type*} [hp : Fact p.Prime] [CommRing R] [CommRing S]
+variable {p : ℕ} {R : Type*} [hp : Fact p.Prime] [CommRing R]
 
 local notation "𝕎" => WittVector p -- type as `\bbW`
 

Mathlib/RingTheory/WittVector/IsPoly.lean

@@ -92,7 +92,7 @@ namespace WittVector
 
 universe u
 
-variable {p : ℕ} {R S : Type u} {σ idx : Type*} [CommRing R] [CommRing S]
+variable {p : ℕ} {R S : Type u} {idx : Type*} [CommRing R] [CommRing S]
 
 local notation "𝕎" => WittVector p -- type as `\bbW`
 

Mathlib/SetTheory/Game/Birthday.lean

@@ -126,7 +126,7 @@ theorem le_birthday : ∀ x : PGame, x ≤ x.birthday.toPGame
         Or.inl ⟨toLeftMovesToPGame ⟨_, birthday_moveLeft_lt i⟩, by simp [le_birthday (xL i)]⟩,
         isEmptyElim⟩
 
-variable (a b x : PGame.{u})
+variable (x : PGame.{u})
 
 theorem neg_birthday_le : -x.birthday.toPGame ≤ x := by
   simpa only [birthday_neg, ← neg_le_iff] using le_birthday (-x)

Mathlib/SetTheory/Ordinal/Nimber.lean

@@ -152,8 +152,6 @@ theorem not_small_nimber : ¬ Small.{u} Nimber.{max u v} :=
 
 namespace Ordinal
 
-variable {a b c : Ordinal.{u}}
-
 @[simp]
 theorem toNimber_symm_eq : toNimber.symm = Nimber.toOrdinal :=
   rfl

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

@@ -27,7 +27,7 @@ open CategoryTheory CategoryTheory.FreeBicategory
 
 open scoped Bicategory
 
-variable {B : Type u} [Bicategory.{w, v} B] {a b c d e : B}
+variable {B : Type u} [Bicategory.{w, v} B] {a b c d : B}
 
 namespace Mathlib.Tactic.BicategoryCoherence
 

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -79,7 +79,7 @@ theorem Filter.Tendsto.const_smul {f : β → α} {l : Filter β} {a : α} (hf :
     (c : M) : Tendsto (fun x => c • f x) l (𝓝 (c • a)) :=
   ((continuous_const_smul _).tendsto _).comp hf
 
-variable [TopologicalSpace β] {f : β → M} {g : β → α} {b : β} {s : Set β}
+variable [TopologicalSpace β] {g : β → α} {b : β} {s : Set β}
 
 @[to_additive]
 nonrec theorem ContinuousWithinAt.const_smul (hg : ContinuousWithinAt g s b) (c : M) :

Mathlib/Topology/Compactification/OnePoint.lean

@@ -187,7 +187,7 @@ instance : TopologicalSpace (OnePoint X) where
     rw [preimage_sUnion]
     exact isOpen_biUnion fun s hs => (ho s hs).2
 
-variable {s : Set (OnePoint X)} {t : Set X}
+variable {s : Set (OnePoint X)}
 
 theorem isOpen_def :
     IsOpen s ↔ (∞ ∈ s → IsCompact ((↑) ⁻¹' s : Set X)ᶜ) ∧ IsOpen ((↑) ⁻¹' s : Set X) :=

Mathlib/Topology/ContinuousMap/Defs.lean

@@ -67,8 +67,7 @@ end ContinuousMapClass
 
 namespace ContinuousMap
 
-variable {X Y γ δ : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace γ]
-  [TopologicalSpace δ]
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
 instance instFunLike : FunLike C(X, Y) X Y where
   coe := ContinuousMap.toFun
@@ -111,8 +110,6 @@ theorem coe_copy (f : C(X, Y)) (f' : X → Y) (h : f' = f) : ⇑(f.copy f' h) =
 theorem copy_eq (f : C(X, Y)) (f' : X → Y) (h : f' = f) : f.copy f' h = f :=
   DFunLike.ext' h
 
-variable {f g : C(X, Y)}
-
 /-- Deprecated. Use `map_continuous` instead. -/
 protected theorem continuous (f : C(X, Y)) : Continuous f :=
   f.continuous_toFun

Mathlib/Topology/LocalAtTarget.lean

@@ -23,7 +23,7 @@ open TopologicalSpace Set Filter
 open Topology Filter
 
 variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {f : α → β}
-variable {s : Set β} {ι : Type*} {U : ι → Opens β}
+variable {ι : Type*} {U : ι → Opens β}
 
 theorem Set.restrictPreimage_inducing (s : Set β) (h : Inducing f) :
     Inducing (s.restrictPreimage f) := by

Mathlib/Topology/Order/LawsonTopology.lean

@@ -49,7 +49,7 @@ Lawson topology, preorder
 
 open Set TopologicalSpace
 
-variable {α β : Type*}
+variable {α : Type*}
 
 namespace Topology
 

Mathlib/Topology/Order/ScottTopology.lean

@@ -107,7 +107,7 @@ lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := fun _d _ _ _a ha ↦ (
 end Preorder
 
 section CompleteLattice
-variable [CompleteLattice α] {s t : Set α}
+variable [CompleteLattice α] {s : Set α}
 
 lemma dirSupInacc_iff_forall_sSup :
     DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by
@@ -124,7 +124,7 @@ namespace Topology
 /-! ### Scott-Hausdorff topology -/
 
 section ScottHausdorff
-variable [Preorder α] {s : Set α}
+variable [Preorder α]
 
 /-- The Scott-Hausdorff topology.
 

Mathlib/Topology/Sets/Order.lean

@@ -15,7 +15,7 @@ In this file we define the type of clopen upper sets.
 
 open Set TopologicalSpace
 
-variable {α β : Type*} [TopologicalSpace α] [LE α] [TopologicalSpace β] [LE β]
+variable {α : Type*} [TopologicalSpace α] [LE α]
 
 /-! ### Compact open sets -/