diff --git a/Mathlib/Combinatorics/Digraph/Basic.lean b/Mathlib/Combinatorics/Digraph/Basic.lean
index f29d31b9e8121..bc72f31b7b8b4 100644
--- a/Mathlib/Combinatorics/Digraph/Basic.lean
+++ b/Mathlib/Combinatorics/Digraph/Basic.lean
@@ -96,7 +96,7 @@ Any bipartite digraph may be regarded as a subgraph of one of these.
 def completeBipartiteGraph (V W : Type*) : Digraph (Sum V W) where
   Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft
 
-variable {ι : Sort*} {V W X : Type*} (G : Digraph V) (G' : Digraph W) {a b c u v w : V}
+variable {ι : Sort*} {V : Type*} (G : Digraph V) {a b : V}
 
 theorem adj_injective : Injective (Adj : Digraph V → V → V → Prop) := fun _ _ ↦ Digraph.ext
 
diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
index a7d1c6345f5ca..d2173e136b147 100644
--- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
+++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@@ -100,8 +100,7 @@ variable {α β : Type*}
 /-! ### Truncated supremum, truncated infimum -/
 
 section SemilatticeSup
-variable [SemilatticeSup α] [SemilatticeSup β]
-  [BoundedOrder β] {s t : Finset α} {a b : α}
+variable [SemilatticeSup α] [SemilatticeSup β] [BoundedOrder β] {s t : Finset α} {a : α}
 
 private lemma sup_aux [@DecidableRel α (· ≤ ·)] : a ∈ lowerClosure s → {b ∈ s | a ≤ b}.Nonempty :=
   fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩
@@ -283,7 +282,7 @@ lemma truncatedInf_sups_of_not_mem (ha : a ∉ upperClosure s ⊔ upperClosure t
 end DistribLattice
 
 section BooleanAlgebra
-variable [BooleanAlgebra α] [@DecidableRel α (· ≤ ·)] {s : Finset α} {a : α}
+variable [BooleanAlgebra α] [@DecidableRel α (· ≤ ·)]
 
 @[simp] lemma compl_truncatedSup (s : Finset α) (a : α) :
     (truncatedSup s a)ᶜ = truncatedInf sᶜˢ aᶜ := map_truncatedSup (OrderIso.compl α) _ _
@@ -329,7 +328,7 @@ open Finset hiding card
 open Fintype Nat
 
 namespace AhlswedeZhang
-variable {α : Type*} [Fintype α] [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s : Finset α}
+variable {α : Type*} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}
 
 /-- Weighted sum of the size of the truncated infima of a set family. Relevant to the
 Ahlswede-Zhang identity. -/
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean
index 537a0a3db2b6f..cb2a27b1ef1eb 100644
--- a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean
+++ b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean
@@ -70,7 +70,7 @@ namespace UV
 section GeneralizedBooleanAlgebra
 
 variable [GeneralizedBooleanAlgebra α] [DecidableRel (@Disjoint α _ _)]
-  [DecidableRel ((· ≤ ·) : α → α → Prop)] {s : Finset α} {u v a b : α}
+  [DecidableRel ((· ≤ ·) : α → α → Prop)] {s : Finset α} {u v a : α}
 
 /-- UV-compressing `a` means removing `v` from it and adding `u` if `a` and `u` are disjoint and
 `v ≤ a` (it replaces the `v` part of `a` by the `u` part). Else, UV-compressing `a` doesn't do
@@ -265,7 +265,7 @@ end GeneralizedBooleanAlgebra
 
 open FinsetFamily
 
-variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v a : Finset α} {r : ℕ}
+variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v : Finset α} {r : ℕ}
 
 /-- Compressing a finset doesn't change its size. -/
 theorem card_compress (huv : #u = #v) (a : Finset α) : #(compress u v a) = #a := by
diff --git a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
index 6f6dbafc9c630..7e044d51a7439 100644
--- a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
+++ b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean
@@ -58,8 +58,8 @@ open scoped FinsetFamily
 variable {α β : Type*}
 
 section Finset
-variable [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 ℬ : Finset (Finset α)}
-  {a : α} {f f₁ f₂ f₃ f₄ g μ : Finset α → β} {s t u : Finset α}
+variable [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)}
+  {a : α} {f f₁ f₂ f₃ f₄ : Finset α → β} {s t u : Finset α}
 
 /-- The `n = 1` case of the Ahlswede-Daykin inequality. Note that we can't just expand everything
 out and bound termwise since `c₀ * d₁` appears twice on the RHS of the assumptions while `c₁ * d₀`
diff --git a/Mathlib/Data/Finset/Sups.lean b/Mathlib/Data/Finset/Sups.lean
index 15185f0898be6..0b2bf2e8a4359 100644
--- a/Mathlib/Data/Finset/Sups.lean
+++ b/Mathlib/Data/Finset/Sups.lean
@@ -356,7 +356,7 @@ end DistribLattice
 
 section Finset
 variable [DecidableEq α]
-variable {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} {a : α}
+variable {𝒜 ℬ : Finset (Finset α)} {s t : Finset α}
 
 @[simp] lemma powerset_union (s t : Finset α) : (s ∪ t).powerset = s.powerset ⊻ t.powerset := by
   ext u
@@ -508,7 +508,7 @@ theorem disjSups_disjSups_disjSups_comm : s ○ t ○ (u ○ v) = s ○ u ○ (t
 end DistribLattice
 section Diffs
 variable [DecidableEq α]
-variable [GeneralizedBooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u v : Finset α)
+variable [GeneralizedBooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u : Finset α)
 
 /-- `s \\ t` is the finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`. -/
 def diffs : Finset α → Finset α → Finset α := image₂ (· \ ·)
@@ -592,7 +592,7 @@ lemma diffs_right_comm : s \\ t \\ u = s \\ u \\ t := image₂_right_comm sdiff_
 end Diffs
 
 section Compls
-variable [BooleanAlgebra α] (s s₁ s₂ t t₁ t₂ u v : Finset α)
+variable [BooleanAlgebra α] (s s₁ s₂ t : Finset α)
 
 /-- `sᶜˢ` is the finset of elements of the form `aᶜ` where `a ∈ s`. -/
 def compls : Finset α → Finset α := map ⟨compl, compl_injective⟩
@@ -602,7 +602,7 @@ scoped[FinsetFamily] postfix:max "ᶜˢ" => Finset.compls
 
 open FinsetFamily
 
-variable {s t} {a b c : α}
+variable {s t} {a : α}
 
 @[simp] lemma mem_compls : a ∈ sᶜˢ ↔ aᶜ ∈ s := by
   rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]
@@ -615,7 +615,7 @@ variable (s t)
 
 @[simp] lemma card_compls : #sᶜˢ = #s := card_map _
 
-variable {s s₁ s₂ t t₁ t₂ u}
+variable {s s₁ s₂ t}
 
 lemma compl_mem_compls : a ∈ s → aᶜ ∈ sᶜˢ := mem_map_of_mem _
 @[simp] lemma compls_subset_compls : s₁ᶜˢ ⊆ s₂ᶜˢ ↔ s₁ ⊆ s₂ := map_subset_map
diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean
index 054bfb7524698..8359ba6ca7c44 100644
--- a/Mathlib/GroupTheory/GroupAction/Blocks.lean
+++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean
@@ -348,7 +348,7 @@ theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] :
     exact .orbit_of_normal a
 
 section Group
-variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a b : G}
+variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a : G}
 
 /-!
 Annoyingly, it seems like the following two lemmas cannot be unified.
diff --git a/Mathlib/GroupTheory/GroupAction/Support.lean b/Mathlib/GroupTheory/GroupAction/Support.lean
index 392881eb03ad9..bda425911ec09 100644
--- a/Mathlib/GroupTheory/GroupAction/Support.lean
+++ b/Mathlib/GroupTheory/GroupAction/Support.lean
@@ -44,7 +44,7 @@ theorem Supports.mono (h : s ⊆ t) (hs : Supports G s b) : Supports G t b := fu
 end SMul
 
 variable [Group H] [SMul G α] [SMul G β] [MulAction H α] [SMul H β] [SMulCommClass G H β]
-  [SMulCommClass G H α] {s t : Set α} {b : β}
+  [SMulCommClass G H α] {s : Set α} {b : β}
 
 -- TODO: This should work without `SMulCommClass`
 @[to_additive]
diff --git a/Mathlib/GroupTheory/Order/Min.lean b/Mathlib/GroupTheory/Order/Min.lean
index 6cbf10250be02..3d1047b06f179 100644
--- a/Mathlib/GroupTheory/Order/Min.lean
+++ b/Mathlib/GroupTheory/Order/Min.lean
@@ -49,7 +49,7 @@ lemma minOrder_le_orderOf (ha : a ≠ 1) (ha' : IsOfFinOrder a) : minOrder α 
 
 end Monoid
 
-variable [Group α] {s : Subgroup α} {n : ℕ}
+variable [Group α] {s : Subgroup α}
 
 @[to_additive]
 lemma le_minOrder_iff_forall_subgroup {n : ℕ∞} :
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
index 624873b85abc2..806d527b92bc4 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
@@ -118,7 +118,7 @@ end List
 
 namespace Cycle
 
-variable [DecidableEq α] (s s' : Cycle α)
+variable [DecidableEq α] (s : Cycle α)
 
 /-- A cycle `s : Cycle α`, given `Nodup s` can be interpreted as an `Equiv.Perm α`
 where each element in the list is permuted to the next one, defined as `formPerm`.
diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
index 5b0fb0f4e2877..27fae6ed0d462 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
@@ -21,10 +21,9 @@ import Mathlib.LinearAlgebra.BilinearForm.Hom
 
 suppress_compilation
 
-universe u v w uι uR uA uM₁ uM₂ uN₁ uN₂
+universe u v w uR uA uM₁ uM₂ uN₁ uN₂
 
-variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁}
-  {N₂ : Type uN₂}
+variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂}
 
 open TensorProduct
 
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index 8f6b4168968e9..410d9c7363d47 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -46,7 +46,6 @@ This file is almost identical to `Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.le
 variable {R : Type*} [CommRing R]
 variable {M : Type*} [AddCommGroup M] [Module R M]
 variable (Q : QuadraticForm R M)
-variable {n : ℕ}
 
 namespace CliffordAlgebra
 
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
index 2285548a3e107..82b7f5635657c 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -354,7 +354,7 @@ open scoped DualNumber
 
 open DualNumber TrivSqZeroExt
 
-variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
+variable {R : Type*} [CommRing R]
 
 theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by
   rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul,
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean b/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean
index c662062c74bc4..4208354f24bc0 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean
@@ -17,7 +17,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 `Q₁ →qᵢ Q₂` is notation for `Q₁.Isometry Q₂`.
 -/
 
-variable {ι R M M₁ M₂ M₃ M₄ N : Type*}
+variable {R M M₁ M₂ M₃ M₄ N : Type*}
 
 namespace QuadraticMap
 
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
index e6c65901442b7..328b2319e0765 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
@@ -346,9 +346,7 @@ end Semiring
 namespace Ring
 
 variable [CommRing R]
-variable [∀ i, AddCommGroup (Mᵢ i)] [∀ i, AddCommGroup (Nᵢ i)] [AddCommGroup P]
-variable [∀ i, Module R (Mᵢ i)] [∀ i, Module R (Nᵢ i)] [Module R P]
-variable [Fintype ι]
+variable [∀ i, AddCommGroup (Mᵢ i)] [AddCommGroup P] [∀ i, Module R (Mᵢ i)] [Module R P] [Fintype ι]
 
 @[simp] theorem polar_pi (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (x y : ∀ i, Mᵢ i) :
     polar (pi Q) x y = ∑ i, polar (Q i) (x i) (y i) := by
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
index e9896dd5d9c21..de51f0a712aab 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
@@ -47,7 +47,7 @@ suppress_compilation
 
 open scoped TensorProduct DirectSum
 
-variable {R ι A B : Type*}
+variable {R ι : Type*}
 
 namespace TensorProduct
 
diff --git a/Mathlib/Order/Filter/Cocardinal.lean b/Mathlib/Order/Filter/Cocardinal.lean
index b0fed85fce86e..25e10e20a8fa3 100644
--- a/Mathlib/Order/Filter/Cocardinal.lean
+++ b/Mathlib/Order/Filter/Cocardinal.lean
@@ -22,9 +22,7 @@ In this file we define `Filter.cocardinal hc`: the filter of sets with cardinali
 open Set Filter Cardinal
 
 universe u
-variable {ι : Type u} {α β : Type u}
-variable {c : Cardinal.{u}} {hreg : c.IsRegular}
-variable {l : Filter α}
+variable {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular}
 
 namespace Filter
 
diff --git a/Mathlib/Order/KonigLemma.lean b/Mathlib/Order/KonigLemma.lean
index b38fa275198d5..3e2ecf7719504 100644
--- a/Mathlib/Order/KonigLemma.lean
+++ b/Mathlib/Order/KonigLemma.lean
@@ -51,7 +51,7 @@ Formulate the lemma as a statement about graphs.
 open Set
 section Sequence
 
-variable {α : Type*} [PartialOrder α] [IsStronglyAtomic α] {a b : α}
+variable {α : Type*} [PartialOrder α] [IsStronglyAtomic α] {b : α}
 
 /-- **Kőnig's infinity lemma** : if each element in a strongly atomic order
 is covered by only finitely many others, and `b` is an element with infinitely many things above it,
diff --git a/Mathlib/Order/PFilter.lean b/Mathlib/Order/PFilter.lean
index 5e663221d21fc..d461174544550 100644
--- a/Mathlib/Order/PFilter.lean
+++ b/Mathlib/Order/PFilter.lean
@@ -143,7 +143,7 @@ end SemilatticeInf
 
 section CompleteSemilatticeInf
 
-variable [CompleteSemilatticeInf P] {F : PFilter P}
+variable [CompleteSemilatticeInf P]
 
 theorem sInf_gc :
     GaloisConnection (fun x => toDual (principal x)) fun F => sInf (ofDual F : PFilter P) :=
diff --git a/Mathlib/RingTheory/WittVector/Defs.lean b/Mathlib/RingTheory/WittVector/Defs.lean
index 5003404660142..859c75ad0e563 100644
--- a/Mathlib/RingTheory/WittVector/Defs.lean
+++ b/Mathlib/RingTheory/WittVector/Defs.lean
@@ -156,8 +156,6 @@ evaluating this at `(x₀, x₁)` gives us the sum of two Witt vectors `x₀ + x
 def eval {k : ℕ} (φ : ℕ → MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → 𝕎 R) : 𝕎 R :=
   mk p fun n => peval (φ n) fun i => (x i).coeff
 
-variable (R) [Fact p.Prime]
-
 instance : Zero (𝕎 R) :=
   ⟨eval (wittZero p) ![]⟩
 
diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean
index 9ba22761bcd5e..c2745df6eff9a 100644
--- a/Mathlib/Tactic/Widget/StringDiagram.lean
+++ b/Mathlib/Tactic/Widget/StringDiagram.lean
@@ -182,7 +182,7 @@ def WhiskerLeft.nodes (v h₁ h₂ : ℕ) : WhiskerLeft → List Node
     let ss := η.nodes v (h₁ + 1) (h₂ + 1)
     s :: ss
 
-variable {ρ : Type} [Context ρ] [MonadMor₁ (CoherenceM ρ)]
+variable {ρ : Type} [MonadMor₁ (CoherenceM ρ)]
 
 /-- The list of nodes at the top of a string diagram. -/
 def topNodes (η : WhiskerLeft) : CoherenceM ρ (List Node) := do
diff --git a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean
index cea48f4937a02..cb59956edbce0 100644
--- a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean
+++ b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@@ -447,8 +447,6 @@ theorem zero_comp (g : β →co γ) : (0 : C_c(γ, δ)).comp g = 0 :=
 
 end
 
-variable [T2Space γ]
-
 /-- Composition as an additive monoid homomorphism. -/
 def compAddMonoidHom [AddMonoid δ] [ContinuousAdd δ] (g : β →co γ) : C_c(γ, δ) →+ C_c(β, δ) where
   toFun f := f.comp g
diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean
index 87a1362341a73..dfc2f24a5deeb 100644
--- a/Mathlib/Topology/FiberBundle/Trivialization.lean
+++ b/Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -50,7 +50,7 @@ type of linear trivializations is not even particularly well-behaved.
 open TopologicalSpace Filter Set Bundle Function
 open scoped Topology
 
-variable {ι : Type*} {B : Type*} (F : Type*) {E : B → Type*}
+variable {B : Type*} (F : Type*) {E : B → Type*}
 variable {Z : Type*} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B}
 
 /-- This structure contains the information left for a local trivialization (which is implemented
@@ -194,7 +194,7 @@ theorem symm_trans_target_eq (e e' : Pretrivialization F proj) :
     (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by
   rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
 
-variable (e' : Pretrivialization F (π F E)) {x' : TotalSpace F E} {b : B} {y : E b}
+variable (e' : Pretrivialization F (π F E)) {b : B} {y : E b}
 
 @[simp]
 theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet :=
@@ -502,7 +502,7 @@ theorem continuousAt_of_comp_left {X : Type*} [TopologicalSpace X] {f : X → Z}
   rw [e.source_eq, ← preimage_comp]
   exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)
 
-variable (e' : Trivialization F (π F E)) {x' : TotalSpace F E} {b : B} {y : E b}
+variable (e' : Trivialization F (π F E)) {b : B} {y : E b}
 
 protected theorem continuousOn : ContinuousOn e' e'.source :=
   e'.continuousOn_toFun
@@ -643,8 +643,6 @@ theorem coordChangeHomeomorph_coe (e₁ e₂ : Trivialization F proj) {b : B} (h
     (h₂ : b ∈ e₂.baseSet) : ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b :=
   rfl
 
-variable {B' : Type*} [TopologicalSpace B']
-
 theorem isImage_preimage_prod (e : Trivialization F proj) (s : Set B) :
     e.toPartialHomeomorph.IsImage (proj ⁻¹' s) (s ×ˢ univ) := fun x hx => by simp [e.coe_fst', hx]