diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
index a09a861c..5d604df0 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean
@@ -24,7 +24,7 @@ variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
 variable {V : Type*} [AddCommGroup V] [Module R V]
 variable {A : Type*} [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 variable {W : Type*} [AddCommGroup W] [Module R W] [ConvexSpace R W]
-variable [hom : Affine.IsHomogenization R A W]
+variable {ℋ : Affine.IsHomogenization R A W}
 
 section Module
 
@@ -33,54 +33,55 @@ variable [IsModuleConvexSpace R W]
 /-- If the homogenization of a point lies in the conic hull of a subset `s` of the homogenization
 plane, the point can be written as a convex combination of points in the preimage of `s` under the
 homogenization embedding. -/
-theorem exists_sConvexComb_preimage_of_mem_hull {x} {s : Set W} (hs : s ⊆ Set.range hom.ofPoint)
-    (hx : hom.ofPoint x ∈ hull R s) : ∃ c' : StdSimplex R A,
-      sConvexComb c' = x ∧ (c'.weights.support : Set A) ⊆ (hom.ofPoint ⁻¹' s) := by
+theorem exists_sConvexComb_preimage_of_mem_hull {x} {s : Set W} (hs : s ⊆ Set.range ℋ.ofPoint)
+    (hx : ℋ.ofPoint x ∈ hull R s) : ∃ c' : StdSimplex R A,
+      sConvexComb c' = x ∧ (c'.weights.support : Set A) ⊆ (ℋ.ofPoint ⁻¹' s) := by
   obtain ⟨c, ha, hb, hc⟩ := mem_hull_set.mp hx
   -- use the same weights, just un-embed the domain
-  use StdSimplex.mk (c.comapDomain hom.ofPoint hom.ofPoint_injective.injOn) ?_ ?_
+  use StdSimplex.mk (c.comapDomain ℋ.ofPoint ℋ.ofPoint_injective.injOn) ?_ ?_
   constructor
   · -- the convex combo yields x
-    apply hom.ofPoint_injective
-    rw [hom.ofPoint.isAffineMap.map_sConvexComb, sConvexComb_eq_sum,
-      StdSimplex.weights_map, ← hc, Finsupp.mapDomain_comapDomain _ hom.ofPoint_injective]
+    apply ℋ.ofPoint_injective
+    rw [ℋ.ofPoint.isAffineMap.map_sConvexComb, sConvexComb_eq_sum,
+      StdSimplex.weights_map, ← hc, Finsupp.mapDomain_comapDomain _ ℋ.ofPoint_injective]
     exact ha.trans hs
   · -- the weights are a subset of the preimage of s
     simpa using (Set.preimage_mono ha)
   · -- they're always nonneg
     intro y
-    simpa using hb (hom.ofPoint y)
+    simpa using hb (ℋ.ofPoint y)
   · -- its actually a convex combo, i.e. weights sum to 1
-    have hsum : c.sum (fun a b => b * hom.weight a) = c.sum (fun a b => b) := by
+    have hsum : c.sum (fun a b => b * ℋ.weight a) = c.sum (fun a b => b) := by
         refine Finsupp.sum_congr (fun a h => ?_)
         obtain ⟨_, _, rfl⟩ := (ha.trans hs) h
-        simp [hom.weight_one]
+        simp [ℋ.weight_one]
     -- apply weights map to both sides
-    have := congrArg hom.weight hc
-    simp only [map_finsuppSum, map_smul, smul_eq_mul, hsum, hom.weight_one] at this
+    have := congrArg ℋ.weight hc
+    simp only [map_finsuppSum, map_smul, smul_eq_mul, hsum, ℋ.weight_one] at this
     rw [← this]
     simp only [Finsupp.sum, Finsupp.comapDomain_support, Finsupp.comapDomain_apply]
-    rw [Finset.sum_preimage hom.ofPoint _ (hom.ofPoint_injective.injOn)]
+    rw [Finset.sum_preimage ℋ.ofPoint _ (ℋ.ofPoint_injective.injOn)]
     exact fun _ hx hnx ↦ Finsupp.notMem_support_iff.mp fun _ ↦ hnx (hs (ha hx))
 
 /-- The preimage of the conic hull of a set in the homogenization plane is the convex hull of the
 preimage of the set. -/
-theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range hom.ofPoint) :
-    hom.ofPoint ⁻¹' hull R s = Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
+theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range ℋ.ofPoint) :
+    ℋ.ofPoint ⁻¹' hull R s = Convexity.convexHull R (ℋ.ofPoint ⁻¹' s) := by
   refine subset_antisymm ?_ ?_
   · intro x hx
     obtain ⟨c', rfl, hs⟩ := exists_sConvexComb_preimage_of_mem_hull hs hx
     exact IsConvexSet.convexHull.sConvexComb_mem (le_trans hs subset_convexHull_self)
   · apply Set.image_subset_iff.mp
-    rw [hom.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
+    rw [ℋ.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
     exact (hull R s).isConvexSet.convexHull_subset_iff.mpr subset_hull
 
+variable (hom) in
 /-- The homogenization embedding of the convex hull of a set is contained in the hull of the
 embedding of the set. -/
-theorem preimage_hull_eq_convexHull_preimagke {s : Set A} :
-    hom.ofPoint '' Convexity.convexHull R s ⊆ hull R (hom.ofPoint '' s) := by
+theorem image_hull_eq_convexHull_image {s : Set A} :
+    ℋ.ofPoint '' Convexity.convexHull R s ⊆ hull R (ℋ.ofPoint '' s) := by
   apply Set.image_subset_iff.mp
-  rw [hom.ofPoint.isAffineMap.image_convexHull]
+  rw [ℋ.ofPoint.isAffineMap.image_convexHull]
   simpa using (hull R _).isConvexSet.convexHull_subset_iff.mpr subset_hull
 
 end Module
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean
index 518a7dbe..0bc19c89 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean
@@ -32,11 +32,9 @@ include V in
 /-- Faces of polytopes are polytopes. -/
 theorem IsPolytope.face_isPolytope (hC : IsPolytope R (C : Set A)) (hF : IsFaceOf F C) :
     IsPolytope R (F : Set A) := by
-  let W := Homogenization R A
-  let : ConvexSpace R W := ConvexSpace.ofModule
-  have homC := IsPolytope.homogenize_fg (W := W) hC
-  have homF := IsHomogenization.homogenize_isFaceOf (W := W) hF
-  have := PointedCone.IsFaceOf.fg homC homF
+  let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+  have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hF
+  have := PointedCone.IsFaceOf.fg (IsPolytope.homogenize_fg _ hC) homF
   convert FG.dehomogenize_isPolytope this (fun _ a b ↦ weight_pos_of_mem_homogenize a b)
   simp [dehomogenize_homogenize]
 
@@ -52,13 +50,12 @@ This is private since it does not yet have the correct grading (off-by-one).
 -/
 private noncomputable instance Polytope.faceHomogenizationGradeOrder (P : Polytope R A) :
     GradeOrder ℕ (Face (P : ConvexSet R A)) := by
-  let W := Homogenization R A
-  letI : ConvexSpace R W := ConvexSpace.ofModule
-  have : PointedCone.FG (homogenize W (P : ConvexSet R A)) :=
-    IsPolytope.homogenize_fg (W := W) P.isPolytope
+  let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+  have : PointedCone.FG (homogenize _ (P : ConvexSet R A)) :=
+    IsPolytope.homogenize_fg (IsHomogenization.canonical R A) P.isPolytope
   let := PointedCone.FG.gradeOrder_finrank this
-  refine GradeOrder.liftRight (β := (homogenize W (P : ConvexSet R A)).Face) _
-    IsHomogenization.Face.homogenizeIso.strictMono ?_
+  refine GradeOrder.liftRight _
+    (IsHomogenization.Face.homogenizeIso (IsHomogenization.canonical R A) _).strictMono ?_
   exact fun x y ↦ (apply_covBy_apply_iff _).mpr
 
 end Field
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
index 1f1930d8..af88ac64 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean
@@ -28,46 +28,46 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 open PointedCone
 
 /-- The homogenization of a polytope is a finitely generated cone. -/
 theorem IsPolytope.homogenize_fg {C : ConvexSet R A} (hCfg : IsPolytope R (C : Set A)) :
-    (homogenize W C).FG := by
+    (homogenize ℋ C).FG := by
   obtain ⟨t, ht⟩ := hCfg
   have : C = ⟨convexHull R t, IsConvexSet.convexHull⟩ := SetLike.ext' ht
-  have := congrArg (ConvexSet.homogenize W) this
+  have := congrArg (ConvexSet.homogenize ℋ) this
   rw [this]
-  use t.map ⟨_, hom.ofPoint_injective⟩
+  use t.map ⟨_, ℋ.ofPoint_injective⟩
   simp only [Finset.coe_map, Function.Embedding.coeFn_mk, homogenize,
     PointedCone.hull, ConvexSet.mk_eq]
-  rw [hom.ofPoint.isAffineMap.image_convexHull t]
-  exact (PointedCone.hull_convexHull (hom.ofPoint '' t)).symm
+  rw [ℋ.ofPoint.isAffineMap.image_convexHull t]
+  exact (PointedCone.hull_convexHull (ℋ.ofPoint '' t)).symm
 
 /-- A convex set is a polytope iff its homogenization is a finitely generated cone. -/
 theorem IsPolytope.iff_homogenize_fg {C : ConvexSet R A} :
-    IsPolytope R (C : Set A) ↔ (homogenize W C).FG := by classical
-  refine ⟨homogenize_fg, fun hfg ↦ ?_⟩
+    IsPolytope R (C : Set A) ↔ (homogenize ℋ C).FG := by classical
+  refine ⟨homogenize_fg _, fun hfg ↦ ?_⟩
   -- get cone generators that lie in the embedding of A
   obtain ⟨g, hg, hs⟩ := homogenize_fg_ofPoint_range hfg
   -- un-embed them
-  use g.preimage hom.ofPoint hom.ofPoint_injective.injOn
+  use g.preimage ℋ.ofPoint ℋ.ofPoint_injective.injOn
   -- show they generate C
   simp only [Finset.coe_preimage]
   apply le_antisymm
   · intro x hx
     rw [← preimage_hull_eq_convexHull_preimage hs]
     simp only [hg, homogenize]
-    exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem hom.ofPoint hx
+    exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem ℋ.ofPoint hx
   · apply C.isConvexSet.convexHull_subset_iff.mpr
     intro x hx
     simp only [Set.mem_preimage, SetLike.mem_coe] at hx
     have := Set.mem_preimage.mpr <| Submodule.mem_span_of_mem (R := {c : R // 0 ≤ c}) hx
     simp_rw [hg, homogenize] at this
-    rw [preimage_hull_eq_convexHull_preimage (Set.image_subset_range hom.ofPoint C)] at this
+    rw [preimage_hull_eq_convexHull_preimage (Set.image_subset_range ℋ.ofPoint C)] at this
     rw [← C.isConvexSet.convexHull_eq_self]
-    simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ hom.ofPoint_injective]
+    simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ ℋ.ofPoint_injective]
 
 end Ring
 
@@ -80,13 +80,13 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : IsHomogenization R A W]
+variable {ℋ : IsHomogenization R A W}
 
 open Pointwise Submodule in
 /-- Dehomogenizing a finitely generated positive cone yields a polytope. -/
 theorem FG.dehomogenize_isPolytope {C : PointedCone R W} (h : C.FG)
-    (hc : C ≤ hom.weight.positive) : IsPolytope R (dehomogenize A C : Set A) := by
-  rw [IsPolytope.iff_homogenize_fg (W := W)]
+    (hc : C ≤ ℋ.weight.positive) : IsPolytope R (dehomogenize ℋ C : Set A) := by
+  rw [IsPolytope.iff_homogenize_fg ℋ]
   simpa [homogenize_dehomogenize_of_le_positive hc]
 
 end Field
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean
index 77cff520..eeaadbea 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean
@@ -28,33 +28,34 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : Affine.IsHomogenization R A W]
+variable (ℋ : Affine.IsHomogenization R A W)
 
+variable {ℋ} in
 /-- If the homogenization of a point `q` is a positive combination of the homogenization
 of two other points, then `q` lies in the open segment between them. -/
 theorem pos_combo_openSegment {r₁ r₂ t : R} {p₁ p₂ q : A}
     (h₁ : 0 < r₁) (h₂ : 0 < r₂) (hₜ : 0 < t)
-    (h : r₁ • hom.ofPoint p₁ + r₂ • hom.ofPoint p₂ = t • hom.ofPoint q) :
+    (h : r₁ • ℋ.ofPoint p₁ + r₂ • ℋ.ofPoint p₂ = t • ℋ.ofPoint q) :
       q ∈ Convexity.openSegment R p₁ p₂ := by
-  have : r₁ + r₂ = t := by simpa [hom.weight_one, map_add, map_smul] using congr_arg hom.weight h
+  have : r₁ + r₂ = t := by simpa [ℋ.weight_one, map_add, map_smul] using congr_arg ℋ.weight h
   have : t⁻¹ • r₁ + t⁻¹ • r₂ = 1 := by
       simp_rw [← smul_add, smul_eq_mul, this, mul_comm, Field.mul_inv_cancel _ hₜ.ne.symm]
   use (t⁻¹ • r₁), (t⁻¹ • r₂), (smul_pos (by positivity) h₁), (smul_pos (by positivity) h₂), this
-  apply hom.ofPoint_injective
-  have : t⁻¹ • (r₁ • hom.ofPoint p₁ + r₂ • hom.ofPoint p₂) = hom.ofPoint q := by
+  apply ℋ.ofPoint_injective
+  have : t⁻¹ • (r₁ • ℋ.ofPoint p₁ + r₂ • ℋ.ofPoint p₂) = ℋ.ofPoint q := by
     rw [h, smul_smul, inv_mul_cancel₀ (ne_of_gt hₜ), one_smul]
-  simp [hom.ofPoint.isAffineMap.map_convexCombPair, convexCombPair_eq_sum, ← this, smul_smul]
+  simp [ℋ.ofPoint.isAffineMap.map_convexCombPair, convexCombPair_eq_sum, ← this, smul_smul]
 
 /-- If `F` is a face of `P`, then the homogenization of `F` is a face of the homogenization
 of `P`. -/
 theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
-    (F.homogenize W).IsFaceOf (P.homogenize W) where
-  le := homogenizeOrderHom.monotone' he.le
+    (F.homogenize ℋ).IsFaceOf (P.homogenize ℋ) where
+  le := (homogenizeOrderHom ℋ).monotone' he.le
   mem_of_smul_add_mem := by
     intro v w a hv hw ha hvw
-    have hhom : (P.homogenize W).Salient := homogenize_salient
+    have hhom := homogenize_salient ℋ P
     by_cases hnf : (F : Set A).Nonempty
-    · have cF := F.isConvexSet.image hom.ofPoint.isAffineMap
+    · have cF := F.isConvexSet.image ℋ.ofPoint.isAffineMap
       apply (Set.ext_iff.mp (PointedCone.hull_eq_smul (hnf.image _) cF) _).mpr
       by_cases hv0 : v = 0
       · exact ⟨0, le_rfl, mem_smul_set.mpr (by simpa [hv0] using nonempty_def.mp hnf)⟩
@@ -70,13 +71,13 @@ theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
           rw [smul_assoc, hra, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ ha.ne.symm, one_smul]
         · obtain ⟨rw, rw0, q, ⟨q', qq, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hw hw0
           obtain ⟨rv, rv0, _, ⟨p', pp, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hv hv0
-          have : a • (rv • hom.ofPoint p') + (rw • hom.ofPoint q') ≠ 0 := by
+          have : a • (rv • ℋ.ofPoint p') + (rw • ℋ.ofPoint q') ≠ 0 := by
             intro hc
-            exact (smul_ne_zero rw0.ne.symm (ofPoint_ne_zero q')) <|
+            exact (smul_ne_zero rw0.ne.symm (ℋ.ofPoint_ne_zero q')) <|
               hhom _ hw _ (PointedCone.smul_mem _ ha.le hv) (by simpa [add_comm] using hc)
           obtain ⟨_, rvw0, _, ⟨_, qqp, rfl⟩, pdp⟩ := smul_pos_of_mem_homogenize hvw this
           have := he.left_mem_of_mem_openSegment pp qq qqp ?_
-          · refine ⟨rv, rv0.le, smul_mem_smul_set <| mem_image_of_mem ofPoint this⟩
+          · refine ⟨rv, rv0.le, smul_mem_smul_set <| mem_image_of_mem ℋ.ofPoint this⟩
           rw [← smul_assoc _ rv] at pdp
           exact pos_combo_openSegment (smul_pos ha rv0) rw0 rvw0 pdp.symm
     · have := not_nonempty_iff_eq_empty.mp hnf
@@ -89,17 +90,16 @@ theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
         rw [this]
         exact PointedCone.smul_mem _ (by positivity) hw) (add_neg_cancel v)
 
-variable (A) in
 /-- If `F` is a face of `C`, then the dehomogenization of `F` is a face of the dehomogenization
 of `C`. -/
 theorem dehomogenize_isFaceOf {F C : PointedCone R W} (hf : F.IsFaceOf C) :
-    (ConvexSet.dehomogenize A F).IsFaceOf (ConvexSet.dehomogenize A C) where
+    (ConvexSet.dehomogenize ℋ F).IsFaceOf (ConvexSet.dehomogenize ℋ C) where
   le := preimage_mono (fun _ x ↦ hf.le x)
   left_mem_of_mem_openSegment  := by
     rintro x hx y hy z hz ⟨a, b, ha, hb, hab, hzo⟩
     refine hf.mem_of_smul_add_mem hx (C.smul_mem hb.le hy) ha ?_
     rwa [← convexCombPair_eq_sum _ _ ha.le hb.le hab,
-      ← hom.ofPoint.isAffineMap.map_convexCombPair, hzo]
+      ← ℋ.ofPoint.isAffineMap.map_convexCombPair, hzo]
 
 /-- The isomorphism between the face lattice of a convex set `P` and the face lattice of
 its homogenization cone.
@@ -107,16 +107,16 @@ its homogenization cone.
 This isomorphism is used to translate results between face lattices of cones and face lattices
 of convex sets.
 -/
-def Face.homogenizeIso {P : ConvexSet R A} :
-    Face P ≃o PointedCone.Face (P.homogenize W) where
-  toFun F := ⟨_, hom.homogenize_isFaceOf F.isFaceOf⟩
-  invFun F := ⟨dehomogenize A F.toSubmodule,
-    by simpa [dehomogenize_homogenize] using dehomogenize_isFaceOf A F.isFaceOf⟩
+def Face.homogenizeIso (P : ConvexSet R A) :
+    Face P ≃o PointedCone.Face (P.homogenize ℋ) where
+  toFun F := ⟨_, ℋ.homogenize_isFaceOf F.isFaceOf⟩
+  invFun F := ⟨dehomogenize ℋ F.toSubmodule,
+    by simpa [dehomogenize_homogenize ℋ] using dehomogenize_isFaceOf ℋ F.isFaceOf⟩
   map_rel_iff' := by
     intro a b
     refine ⟨fun h x xm ↦ ?_, fun h _ xm ↦ span_mono (image_mono h) xm⟩
-    refine (ofPoint_mem_homogenize_iff_mem W x b.toConvexSet).mp (h ?_)
-    exact (ofPoint_mem_homogenize_iff_mem W x a.toConvexSet).mpr xm
+    refine (ofPoint_mem_homogenize_iff_mem _ x b.toConvexSet).mp (h ?_)
+    exact (ofPoint_mem_homogenize_iff_mem _ x a.toConvexSet).mpr xm
   left_inv _ := by simp [dehomogenize_homogenize]
   right_inv F := by
     have := homogenize_dehomogenize_of_le_positive
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
index 5a389742..3b091332 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean
@@ -31,60 +31,62 @@ variable [AddCommGroup V] [Module R V]
 variable [AddCommGroup W] [Module R W]
 variable [AddTorsor V A] [ConvexSpace R A]
 
-variable [hom : Affine.IsHomogenization R A W]
+variable (ℋ : Affine.IsHomogenization R A W)
 
-variable (W) in
 /-- The homogenization cone of a convex set in an affine space. -/
-def homogenize (P : ConvexSet R A) : PointedCone R W := hull R (hom.ofPoint '' P)
+def homogenize (P : ConvexSet R A) : PointedCone R W := hull R (ℋ.ofPoint '' P)
 
 lemma homogenize_mono {K₁ K₂ : ConvexSet R A} (h : K₁ ≤ K₂) :
-    K₁.homogenize W ≤ K₂.homogenize W := Submodule.span_mono <| Set.image_mono h
+    K₁.homogenize ℋ ≤ K₂.homogenize ℋ := Submodule.span_mono <| Set.image_mono h
 
-lemma homogenize_monotone : Monotone (homogenize W : ConvexSet R A → PointedCone R W) :=
-  fun _ _ => homogenize_mono
+lemma homogenize_monotone : Monotone (homogenize ℋ : ConvexSet R A → PointedCone R W) :=
+  fun _ _ => homogenize_mono _
 
 /-- Homogenization from convex set to convex cones as an order homomorphism. -/
 def homogenizeOrderHom : ConvexSet R A →o PointedCone R W where
-  toFun := homogenize W
-  monotone' := homogenize_monotone
+  toFun := homogenize ℋ
+  monotone' := homogenize_monotone _
 
 @[simp]
-lemma homogenize_bot : homogenize W (⊥ : ConvexSet R A) = ⊥ := by
-  simp [homogenize]
+lemma homogenize_bot : homogenize ℋ (⊥ : ConvexSet R A) = ⊥ := by
+  simp [homogenize, Bot.bot]
 
 @[simp]
-lemma homogenize_eq_bot_iff (P : ConvexSet R A) : homogenize W P = ⊥ ↔ P = ⊥ := by
+lemma homogenize_eq_bot_iff (P : ConvexSet R A) : homogenize ℋ P = ⊥ ↔ P = ⊥ := by
   refine ⟨fun h ↦ ?_, by simp +contextual [-SetLike.bot_eq_empty]⟩
   ext x
   simp only [homogenize, span_eq_bot, mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂] at h
-  simpa using fun hx ↦ hom.ofPoint_ne_zero _ (h x hx)
+  simpa using fun hx ↦ ℋ.ofPoint_ne_zero _ (h x hx)
 
-/- NOTE: `homogenize_top`, stating `homogenize W (⊤ : ConvexSet R A) = hom.weight.positive`,
+/- NOTE: `homogenize_top`, stating `homogenize ℋ (⊤ : ConvexSet R A) = ℋ.weight.positive`,
 only holds over linearly ordered fields and is proven in the `Field` section below. Over a
 general ordered ring it fails: for `R = ℤ[ε]` with `ε` a positive infinitesimal, the point
 `(1, ε)` lies in `weight.positive` but not in the cone hull of the weight-one hyperplane, since
 all nonnegative coefficients bounded by `ε` lie in the ideal `(ε)`. -/
 
 lemma homogenize_le_weight_positive (K : ConvexSet R A) :
-    homogenize W K ≤ hom.weight.positive := by
+    homogenize ℋ K ≤ ℋ.weight.positive := by
   exact LinearMap.hull_le_positive_of_subset_preimage_singleton one_pos fun _ ↦ by
     rintro ⟨x, -, rfl⟩
-    simp [hom.weight_one]
+    simp [ℋ.weight_one]
 
-lemma weight_pos_of_mem_homogenize {x} {P : ConvexSet R A} (h : x ∈ homogenize W P) (hx : x ≠ 0) :
-    0 < hom.weight x := homogenize_le_weight_positive P h hx
+variable {hom} in
+lemma weight_pos_of_mem_homogenize {x} {P : ConvexSet R A} (h : x ∈ homogenize ℋ P) (hx : x ≠ 0) :
+    0 < ℋ.weight x := homogenize_le_weight_positive _ P h hx
 
-lemma weight_nonneg_of_mem_homogenize {x : W} {P : ConvexSet R A} (h : x ∈ homogenize W P) :
-    0 ≤ hom.weight x :=
-  (LinearMap.mem_positive'.mp (homogenize_le_weight_positive (W := W) P h)).1
+variable {hom} in
+lemma weight_nonneg_of_mem_homogenize {x : W} {P : ConvexSet R A} (h : x ∈ homogenize ℋ P) :
+    0 ≤ ℋ.weight x :=
+  (LinearMap.mem_positive'.mp (homogenize_le_weight_positive _ P h)).1
 
-lemma homogenize_salient {K : ConvexSet R A} : PointedCone.Salient (homogenize W K) :=
-  Salient.of_le_salient hom.weight.positive_salient (homogenize_le_weight_positive K)
+lemma homogenize_salient (K : ConvexSet R A) : PointedCone.Salient (homogenize ℋ K) :=
+  Salient.of_le_salient ℋ.weight.positive_salient (homogenize_le_weight_positive _ K)
 
-theorem homogenize_fg_ofPoint_range {C : ConvexSet R A} (h : (homogenize W C).FG) :
-    ∃ g : Finset W, PointedCone.hull R g = homogenize W C ∧
-      (g : Set W) ⊆ Set.range hom.ofPoint := by
+variable {hom} in
+theorem homogenize_fg_ofPoint_range {C : ConvexSet R A} (h : (homogenize ℋ C).FG) :
+    ∃ g : Finset W, PointedCone.hull R g = homogenize ℋ C ∧
+      (g : Set W) ⊆ Set.range ℋ.ofPoint := by
   obtain ⟨g, hg⟩ := h
   -- express each generator as a positive combo of stuff in the embedding of C
   have gsum {x} (hx : x ∈ g) := mem_hull_set.mp (hg ▸ (Submodule.mem_span_of_mem hx))
@@ -92,7 +94,7 @@ theorem homogenize_fg_ofPoint_range {C : ConvexSet R A} (h : (homogenize W C).FG
   -- collect all said stuff and use as the new generators
   let g' := g.attach.biUnion (fun x => (Classical.choose (gsum x.2)).support)
   use g'
-  have g'sub : (g' : Set W) ⊆ hom.ofPoint '' C := by
+  have g'sub : (g' : Set W) ⊆ ℋ.ofPoint '' C := by
     simpa [g'] using fun _ b ↦ (Classical.choose_spec (gsum b)).1
   have gsubhull : (g : Set W) ⊆ hull R (g' : Set W) := by
     intro x hx
@@ -107,38 +109,35 @@ section Module
 
 variable [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A]
 
-variable (A) in
 def dehomogenize (C : PointedCone R W) : ConvexSet R A :=
-  ⟨_, C.isConvexSet.preimage hom.ofPoint.isAffineMap⟩
+  ⟨_, C.isConvexSet.preimage ℋ.ofPoint.isAffineMap⟩
 
 alias _root_.PointedCone.dehomogenize := dehomogenize
 
 @[simp]
-lemma dehomogenize_bot : dehomogenize A (⊥ : PointedCone R W) = ⊥ := by
+lemma dehomogenize_bot : dehomogenize ℋ (⊥ : PointedCone R W) = ⊥ := by
   ext
   simp [dehomogenize, Affine.IsHomogenization.ofPoint_ne_zero]
 
 @[simp]
-lemma dehomogenize_top : dehomogenize A (⊤ : PointedCone R W) = ⊤ := by
+lemma dehomogenize_top : dehomogenize ℋ (⊤ : PointedCone R W) = ⊤ := by
   ext
   simp [dehomogenize, SetLike.mem_coe.mp]
 
 @[simp]
-lemma dehomogenize_weight_positive : dehomogenize A hom.weight.positive = ⊤ :=
-  SetLike.eq_top_of_forall fun _ ↦ LinearMap.mem_positive'.mpr (by simp [hom.weight_one])
+lemma dehomogenize_weight_positive : dehomogenize ℋ ℋ.weight.positive = ⊤ :=
+  SetLike.eq_top_of_forall fun _ ↦ LinearMap.mem_positive'.mpr (by simp [ℋ.weight_one])
 
-variable (A) in
 lemma dehomogenize_mono {C₁ C₂ : PointedCone R W} (h : C₁ ≤ C₂) :
-    dehomogenize A C₁ ≤ dehomogenize A C₂ := Set.preimage_mono <| Set.preimage_mono h
+    dehomogenize ℋ C₁ ≤ dehomogenize ℋ C₂ := Set.preimage_mono <| Set.preimage_mono h
     -- Q: why Set.preimage_mono twice?
 
-variable (A) in
-lemma dehomogenize_monotone : Monotone (dehomogenize A : PointedCone R W → ConvexSet R A) :=
-  fun _ _ => dehomogenize_mono A
+lemma dehomogenize_monotone : Monotone (dehomogenize ℋ : PointedCone R W → ConvexSet R A) :=
+  fun _ _ => dehomogenize_mono _
 
 -- This lemma is just `Set.image_preimage_eq_inter_range` in disguise. It is likely not needed.
 lemma ofPoint_dehomogenize_eq_inter_ofPoint (C : PointedCone R W) :
-    hom.ofPoint '' dehomogenize A C = (C : Set W) ∩ hom.ofPoint.range := by
+    ℋ.ofPoint '' dehomogenize ℋ C = (C : Set W) ∩ ℋ.ofPoint.range := by
   ext x
   simp only [Set.mem_image, SetLike.mem_coe, Set.mem_inter_iff, AffineMap.mem_range]
   constructor
@@ -151,8 +150,8 @@ lemma ofPoint_dehomogenize_eq_inter_ofPoint (C : PointedCone R W) :
 /-- The preimage of the conic hull of a set in the homogenization plane is the convex hull of the
 preimage of the set. -/
 theorem hull_image_ofPoint_eq_homogenize_convexHull {s : Set A} :
-    hull R (hom.ofPoint '' s) = homogenize W (ConvexSet.convexHull R s) := by
-  simp [homogenize, ConvexSet.convexHull, hom.ofPoint.isAffineMap.image_convexHull]
+    hull R (ℋ.ofPoint '' s) = homogenize ℋ (ConvexSet.convexHull R s) := by
+  simp [homogenize, ConvexSet.convexHull, ℋ.ofPoint.isAffineMap.image_convexHull]
 
 end Module
 
@@ -162,86 +161,86 @@ section Field
 
 variable [Field R] [LinearOrder R] [IsOrderedRing R]
 variable [AddCommGroup V] [Module R V]
-variable [AddCommGroup W] [Module R W] [ConvexSpace R W]
-variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
-
-variable [IsModuleConvexSpace R W]
+variable [AddCommGroup W] [Module R W]
+variable [AddTorsor V A] [ConvexSpace R A]
 
-variable [hom : Affine.IsHomogenization R A W]
+variable (ℋ : Affine.IsHomogenization R A W)
 
-omit [IsModuleConvexSpace R W] in
 /-- The homogenization of the full affine space is the positive cone of the weight functional. -/
-lemma homogenize_top : homogenize W (⊤ : ConvexSet R A) = hom.weight.positive := by
-  rw [homogenize, LinearMap.positive_eq_hull_preimage_singleton hom.weight one_pos,
-    ← hom.ofPoint_range_eq_preimage_weight_one]
+lemma homogenize_top : homogenize ℋ (⊤ : ConvexSet R A) = ℋ.weight.positive := by
+  rw [homogenize, LinearMap.positive_eq_hull_preimage_singleton ℋ.weight one_pos,
+    ← ℋ.ofPoint_range_eq_preimage_weight_one]
   congr! with x
   simp
 
-lemma smul_pos_of_mem_homogenize {P : ConvexSet R A} {x} (h : x ∈ homogenize W P) (hx : x ≠ 0) :
-    x ∈ Set.Ioi (0 : R) • hom.ofPoint '' (P : Set A) :=
+variable [ConvexSpace R W] [IsModuleConvexSpace R W] [IsAffineConvexSpace R V A]
+
+variable {ℋ} in
+lemma smul_pos_of_mem_homogenize {P : ConvexSet R A} {x} (h : x ∈ homogenize ℋ P) (hx : x ≠ 0) :
+    x ∈ Set.Ioi (0 : R) • ℋ.ofPoint '' (P : Set A) :=
   (mem_hull_iff_mem_pos_smul_of_convex_nonzero
-    (P.isConvexSet.image hom.ofPoint.isAffineMap) hx).mp h
+    (P.isConvexSet.image ℋ.ofPoint.isAffineMap) hx).mp h
 
 -- TODO: This lemma should be proven for general sets (homogenizing to SubMulAction) and then
 --  applied here as a special case.
-variable (W) in
 lemma ofPoint_mem_homogenize_iff_mem (x : A) (P : ConvexSet R A) :
-    hom.ofPoint x ∈ homogenize W P ↔ x ∈ P := by
-  refine ⟨fun h ↦ ?_, fun h ↦ mem_span_of_mem (Set.mem_image_of_mem hom.ofPoint h)⟩
-  obtain ⟨_, _, h'⟩ := smul_pos_of_mem_homogenize (Set.mem_preimage.mpr h) (hom.ofPoint_ne_zero x)
+    ℋ.ofPoint x ∈ homogenize ℋ P ↔ x ∈ P := by
+  refine ⟨fun h ↦ ?_, fun h ↦ mem_span_of_mem (Set.mem_image_of_mem ℋ.ofPoint h)⟩
+  obtain ⟨_, _, h'⟩ := smul_pos_of_mem_homogenize (Set.mem_preimage.mpr h) (ℋ.ofPoint_ne_zero x)
   obtain ⟨_, ⟨_, _, hyy'⟩, hy'⟩ := Set.mem_smul_set.mp h'
-  have := congrArg hom.weight hy'
-  simp [← hyy', hom.weight_one] at this
+  have := congrArg ℋ.weight hy'
+  simp [← hyy', ℋ.weight_one] at this
   simp only [this, Set.mem_image, one_smul, exists_eq_right] at h'
   obtain ⟨_, _, hxx'⟩ := h'
-  simpa [← hom.ofPoint_injective hxx']
+  simpa [← ℋ.ofPoint_injective hxx']
 
 /-- Dehomogenizing the homogenization of a convex set yields the same set again. -/
 @[simp] theorem dehomogenize_homogenize (P : ConvexSet R A) :
-    dehomogenize A (homogenize W P) = P := by
+    dehomogenize ℋ (homogenize ℋ P) = P := by
   ext x; exact ofPoint_mem_homogenize_iff_mem _ _ _
 
-lemma homogenize_injective : Function.Injective (homogenize (hom := hom) W) := by
+lemma homogenize_injective : Function.Injective (homogenize ℋ) := by
   intro P Q h
-  have hh := congr_arg (ConvexSet.dehomogenize A) h
+  have hh := congr_arg (ConvexSet.dehomogenize ℋ) h
   simp [dehomogenize_homogenize] at hh
   assumption
 
+variable {ℋ} in
 /-- If the entire cone save the origin are at positive weight, homogenizing the dehomogenization
 of the homogenize yields the cone again. -/
 theorem homogenize_dehomogenize_of_le_positive {C : PointedCone R W}
-    (hC : C ≤ hom.weight.positive) : homogenize W (dehomogenize A C) = C := by
+    (hC : C ≤ ℋ.weight.positive) : homogenize ℋ (dehomogenize ℋ C) = C := by
   by_cases hbot : C = ⊥
   · simp [hbot, homogenize, dehomogenize]
   · apply SetLike.ext'
     unfold homogenize
     rw [eq_Ici_zero_smul_inter_preimage_of_pos_of_ne_bot hC zero_lt_one hbot,
-      ofPoint_dehomogenize_eq_inter_ofPoint, ← hom.ofPoint_range_eq_preimage_weight_one]
+      ofPoint_dehomogenize_eq_inter_ofPoint, ← ℋ.ofPoint_range_eq_preimage_weight_one]
     apply hull_eq_smul
     · obtain ⟨y, hyC, hy0⟩ := exists_mem_ne_zero_of_ne_bot hbot
-      let y' := (hom.weight y)⁻¹ • y
+      let y' := (ℋ.weight y)⁻¹ • y
       have hy'C : y' ∈ C :=
         C.smul_mem (inv_nonneg.mpr (@hC y hyC hy0).le) hyC
-      have hy' : y' ∈ Set.range hom.ofPoint := by
-        simpa [y', hom.ofPoint_range_eq_preimage_weight_one]
+      have hy' : y' ∈ Set.range ℋ.ofPoint := by
+        simpa [y', ℋ.ofPoint_range_eq_preimage_weight_one]
           using inv_mul_cancel₀ (@hC y hyC hy0).ne.symm
       exact ⟨y', hy'C, hy'⟩
-    · exact C.isConvexSet.inter hom.ofPoint.range_isConvexSet
+    · exact C.isConvexSet.inter ℋ.ofPoint.range_isConvexSet
 
 lemma homogenize_mono_iff {K₁ K₂ : ConvexSet R A} :
-    K₁.homogenize W ≤ K₂.homogenize W ↔ K₁ ≤ K₂ where
-  mp h := by simpa using dehomogenize_mono A h
-  mpr := homogenize_mono
+    K₁.homogenize ℋ ≤ K₂.homogenize ℋ ↔ K₁ ≤ K₂ where
+  mp h := by simpa using dehomogenize_mono ℋ h
+  mpr := homogenize_mono _
 
 -- Issue #66
 /-- The lattice of convex sets is isomorphic to the lattice of convex sub-cones of the
 positive cone. -/
-def homogenizeOrderEquiv : ConvexSet R A ≃o Set.Iic hom.weight.positive where
-  toFun K := ⟨_, K.homogenize_le_weight_positive⟩
-  invFun C := dehomogenize A C.1
-  left_inv K := dehomogenize_homogenize K
+def homogenizeOrderEquiv : ConvexSet R A ≃o Set.Iic ℋ.weight.positive where
+  toFun K := ⟨_, K.homogenize_le_weight_positive _⟩
+  invFun C := dehomogenize ℋ C.1
+  left_inv K := dehomogenize_homogenize _ K
   right_inv C := by dsimp; congr; exact homogenize_dehomogenize_of_le_positive C.2
-  map_rel_iff' := homogenize_mono_iff
+  map_rel_iff' := homogenize_mono_iff _
 
 end Field
 
diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean
index 3b585afd..5cc5bef7 100644
--- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean
+++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Basic.lean
@@ -44,7 +44,7 @@ variable (R A W) in
 weight-1 hyperplane under a given linear weight map.
 Follows Definition 4.2 in [Gallier2011GeometricMethods]
 https://www.cis.upenn.edu/~jean/gma-v2-root.pdf -/
-class IsHomogenization where
+structure IsHomogenization where
   ofPoint : A →ᵃ[R] W
   ofPoint_injective : Injective ofPoint
   weight : W →ₗ[R] R
@@ -52,7 +52,7 @@ class IsHomogenization where
 
 variable (R A) in
 /-- The canonical homogenization is a homogenization. -/
-noncomputable instance IsHomogenization.canonical :
+noncomputable def IsHomogenization.canonical :
     IsHomogenization R A (Homogenization R A) where
   ofPoint := Homogenization.ofPoint
   ofPoint_injective := Homogenization.ofPoint_injective
@@ -66,117 +66,116 @@ noncomputable instance IsHomogenization.canonical :
 
 namespace IsHomogenization
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
-abbrev ofVector := hom.ofPoint.linear
+abbrev ofVector := ℋ.ofPoint.linear
 
-theorem ofVector_injective : Injective hom.ofVector := by
-  simp [hom.ofPoint_injective]
+theorem ofVector_injective : Injective ℋ.ofVector := by
+  simp [ℋ.ofPoint_injective]
 
 /-- Embedding the underlying vector space is exactly the weight-0 hyperplane. -/
-theorem ofVector_range_eq_weight_ker : hom.ofVector.range = hom.weight.ker := by
+theorem ofVector_range_eq_weight_ker : ℋ.ofVector.range = ℋ.weight.ker := by
   ext x
   let a₀ := Classical.arbitrary A
   simp only [LinearMap.mem_range, LinearMap.mem_ker]
-  have : (∃ y, hom.ofVector y = x) ↔ ∃ a b : A, hom.ofVector (a -ᵥ b) = x :=
+  have : (∃ y, ℋ.ofVector y = x) ↔ ∃ a b : A, ℋ.ofVector (a -ᵥ b) = x :=
     ⟨fun ⟨y, hy⟩ => ⟨y +ᵥ a₀, a₀, by simp [vadd_vsub, hy]⟩, fun ⟨a, b, hab⟩ => ⟨a -ᵥ b, hab⟩⟩
   rw [this]
-  have hh := Set.ext_iff.mp hom.ofPoint_range_eq_preimage_weight_one
+  have hh := Set.ext_iff.mp ℋ.ofPoint_range_eq_preimage_weight_one
   constructor
   · rintro ⟨a, b, hab⟩
     simp only [Set.mem_preimage, Set.mem_singleton_iff] at hh
-    simp [← hab, map_sub, (hh (ofPoint b)).mp ⟨b, rfl⟩, (hh (ofPoint a)).mp ⟨a, rfl⟩]
+    simp [← hab, map_sub, (hh (ℋ.ofPoint b)).mp ⟨b, rfl⟩, (hh (ℋ.ofPoint a)).mp ⟨a, rfl⟩]
   · intro h
-    have ha := Set.mem_preimage.mp <| (hh (hom.ofPoint a₀)).mp (by simp)
-    obtain ⟨b, hb⟩ : x + hom.ofPoint a₀ ∈ (Set.range hom.ofPoint) := by
-      simpa [hom.ofPoint_range_eq_preimage_weight_one, Set.mem_preimage, map_add, h]
+    have ha := Set.mem_preimage.mp <| (hh (ℋ.ofPoint a₀)).mp (by simp)
+    obtain ⟨b, hb⟩ : x + ℋ.ofPoint a₀ ∈ (Set.range ℋ.ofPoint) := by
+      simpa [ℋ.ofPoint_range_eq_preimage_weight_one, Set.mem_preimage, map_add, h]
     exact ⟨b, a₀, by simp [AffineMap.linearMap_vsub, hb]⟩
 
 /-- The homogenization of a point in `A` has weight 1. -/
-lemma weight_one (a₀ : A) : hom.weight (hom.ofPoint a₀) = 1 := by
-  convert Set.ext_iff.mp hom.ofPoint_range_eq_preimage_weight_one (hom.ofPoint a₀)
+lemma weight_one (a₀ : A) : ℋ.weight (ℋ.ofPoint a₀) = 1 := by
+  convert Set.ext_iff.mp ℋ.ofPoint_range_eq_preimage_weight_one (ℋ.ofPoint a₀)
   simp [exists_apply_eq_apply, Set.mem_preimage, Set.mem_singleton_iff, true_iff]
 
 variable [Nontrivial R] in
-theorem ofPoint_ne_zero (x : A) : hom.ofPoint x ≠ (0 : W) := by
+theorem ofPoint_ne_zero (x : A) : ℋ.ofPoint x ≠ (0 : W) := by
   intro hn
-  have := congrArg hom.weight hn
-  simp [weight_one x] at this
+  have := congrArg ℋ.weight hn
+  simp [ℋ.weight_one x] at this
 
 /-- The homogenization of a point in `V` has weight 0. -/
-lemma weight_zero (v : V) : hom.weight (hom.ofVector v) = 0 := by
+lemma weight_zero (v : V) : ℋ.weight (ℋ.ofVector v) = 0 := by
   simp [LinearMap.mem_ker.mp, ← ofVector_range_eq_weight_ker]
 
-theorem span_range_ofPoint : span R (Set.range hom.ofPoint) = ⊤ := by
+theorem span_range_ofPoint : span R (Set.range ℋ.ofPoint) = ⊤ := by
   refine eq_top_iff'.mpr (fun x ↦ ?_)
   let a₀ := Classical.arbitrary A
   -- projecting x to weight 0 along a₀ gives sth in the span of image of ofPoint
-  have hlin : x - hom.weight x • hom.ofPoint a₀ ∈ Submodule.span R hom.ofPoint.range := by
-    obtain ⟨v, hv⟩ : x - hom.weight x • hom.ofPoint a₀ ∈ hom.ofVector.range := by
-      simp [ofVector_range_eq_weight_ker, weight_one a₀]
-    have : hom.ofVector v = hom.ofPoint (v +ᵥ a₀) - hom.ofPoint a₀ := by simp
+  have hlin : x - ℋ.weight x • ℋ.ofPoint a₀ ∈ Submodule.span R ℋ.ofPoint.range := by
+    obtain ⟨v, hv⟩ : x - ℋ.weight x • ℋ.ofPoint a₀ ∈ ℋ.ofVector.range := by
+      simp [ofVector_range_eq_weight_ker, ℋ.weight_one a₀]
+    have : ℋ.ofVector v = ℋ.ofPoint (v +ᵥ a₀) - ℋ.ofPoint a₀ := by simp
     rw [← hv, this]
     apply Submodule.sub_mem <;> apply Submodule.subset_span
     · exact ⟨v +ᵥ a₀, rfl⟩
     · exact ⟨a₀, rfl⟩
   simpa using
-    Submodule.add_mem _ hlin <| smul_mem _ (hom.weight x) (subset_span ⟨a₀, rfl⟩)
+    Submodule.add_mem _ hlin <| smul_mem _ (ℋ.weight x) (subset_span ⟨a₀, rfl⟩)
 
-variable (hom) in
 /-- The canonical linear map from `Homogenization R A` to any homogenization `W` of `A`. -/
-noncomputable def ofCanonical : Homogenization R A →ₗ[R] W := Homogenization.lift hom.ofPoint
+noncomputable def ofCanonical : Homogenization R A →ₗ[R] W := Homogenization.lift ℋ.ofPoint
 
 @[simp] lemma ofCanonical_ofPoint (a : A) :
-    hom.ofCanonical (Homogenization.ofPoint a) = hom.ofPoint a := by
+    ℋ.ofCanonical (Homogenization.ofPoint a) = ℋ.ofPoint a := by
   simp [ofCanonical]
 
 @[simp] lemma ofCanonical_ofVector (v : V) :
-    hom.ofCanonical (Homogenization.ofVector v) = hom.ofVector v := by
+    ℋ.ofCanonical (Homogenization.ofVector v) = ℋ.ofVector v := by
   simp [ofCanonical]
 
 lemma weight_comp_ofCanonical :
-    hom.weight ∘ₗ hom.ofCanonical = (Homogenization.weight : Homogenization R A →ₗ[R] R) :=
+    ℋ.weight ∘ₗ ℋ.ofCanonical = (Homogenization.weight : Homogenization R A →ₗ[R] R) :=
   Homogenization.hom_ext fun a ↦ by simp [weight_one]
 
 @[simp] lemma weight_ofCanonical (x : Homogenization R A) :
-    hom.weight (hom.ofCanonical x) = Homogenization.weight x :=
-  congr($(weight_comp_ofCanonical (hom := hom)) x)
+    ℋ.weight (ℋ.ofCanonical x) = Homogenization.weight x :=
+  congr($(weight_comp_ofCanonical _) x)
 
-theorem ofCanonical_bijective : Bijective hom.ofCanonical := by
+theorem ofCanonical_bijective : Bijective ℋ.ofCanonical := by
   constructor
   · rw [injective_iff_map_eq_zero]
     intro x hx
     have hw : Homogenization.weight x = 0 := by
-      rw [← weight_ofCanonical (W := W) x, hx, map_zero]
+      rw [← ℋ.weight_ofCanonical x, hx, map_zero]
     obtain ⟨v, rfl⟩ := Homogenization.weight_eq_zero_iff.mp hw
-    rw [ofCanonical_ofVector, map_eq_zero_iff _ hom.ofVector_injective] at hx
+    rw [ofCanonical_ofVector, map_eq_zero_iff _ ℋ.ofVector_injective] at hx
     simp [hx]
-  · rw [← LinearMap.range_eq_top, ← top_le_iff, ← hom.span_range_ofPoint, Submodule.span_le,
+  · rw [← LinearMap.range_eq_top, ← top_le_iff, ← ℋ.span_range_ofPoint, Submodule.span_le,
       Set.range_subset_iff]
     exact fun a ↦ ⟨Homogenization.ofPoint a, by simp⟩
 
 /-- Every homogenization is linearly equivalent to the canonical homogenization. -/
 noncomputable def canonEquiv : W ≃ₗ[R] Homogenization R A :=
-  (LinearEquiv.ofBijective _ hom.ofCanonical_bijective).symm
+  (LinearEquiv.ofBijective _ ℋ.ofCanonical_bijective).symm
 
 @[simp] lemma canonEquiv_symm_apply (x : Homogenization R A) :
-    hom.canonEquiv.symm x = hom.ofCanonical x :=
+    ℋ.canonEquiv.symm x = ℋ.ofCanonical x :=
   rfl
 
-@[simp] lemma ofCanonical_canonEquiv (x : W) : hom.ofCanonical (hom.canonEquiv x) = x :=
-  hom.canonEquiv.symm_apply_apply x
+@[simp] lemma ofCanonical_canonEquiv (x : W) : ℋ.ofCanonical (ℋ.canonEquiv x) = x :=
+  ℋ.canonEquiv.symm_apply_apply x
 
 @[simp] lemma canonEquiv_ofPoint (a : A) :
-    hom.canonEquiv (hom.ofPoint a) = Homogenization.ofPoint a :=
-  hom.canonEquiv.symm.injective <| by simp
+    ℋ.canonEquiv (ℋ.ofPoint a) = Homogenization.ofPoint a :=
+  ℋ.canonEquiv.symm.injective <| by simp
 
 theorem canonEquiv_canonical_ofPoint :
-    hom.canonEquiv ∘ hom.ofPoint = Homogenization.ofPoint := by
+    ℋ.canonEquiv ∘ ℋ.ofPoint = Homogenization.ofPoint := by
   ext a; simp
 
-theorem weight_canonEquiv : Homogenization.weight ∘ hom.canonEquiv = hom.weight := by
+theorem weight_canonEquiv : Homogenization.weight ∘ ℋ.canonEquiv = ℋ.weight := by
   ext x
-  rw [Function.comp_apply, ← weight_ofCanonical (W := W) (hom.canonEquiv x),
+  rw [Function.comp_apply, ← ℋ.weight_ofCanonical (ℋ.canonEquiv x),
     ofCanonical_canonEquiv]
 
 -- proving the universal property using the equiv
@@ -184,36 +183,36 @@ theorem weight_canonEquiv : Homogenization.weight ∘ hom.canonEquiv = hom.weigh
 into any vector space extends uniquely to a linear map from `W` to the vector space. -/
 theorem extend (U : Type*) [AddCommGroup U] [Module R U]
     (f : A →ᵃ[R] U) :
-    ∃! (F : W →ₗ[R] U), F ∘ hom.ofPoint = f := by
-  refine ⟨Homogenization.lift f ∘ₗ hom.canonEquiv.toLinearMap, funext fun a ↦ by simp, ?_⟩
+    ∃! (F : W →ₗ[R] U), F ∘ ℋ.ofPoint = f := by
+  refine ⟨Homogenization.lift f ∘ₗ ℋ.canonEquiv.toLinearMap, funext fun a ↦ by simp, ?_⟩
   intro g hg
-  have : g ∘ₗ hom.canonEquiv.symm.toLinearMap = Homogenization.lift f :=
+  have : g ∘ₗ ℋ.canonEquiv.symm.toLinearMap = Homogenization.lift f :=
     Homogenization.hom_ext fun a ↦ by simpa using congrFun hg a
   rw [← this, LinearMap.comp_assoc]
   simp
 
 open AffineMap LinearEquiv in
 /-- The linear equivalence between the underlying vector space and its embedding. -/
-noncomputable def ofVectorRangeEquiv : V ≃ₗ[R] hom.ofVector.range := {
-  toFun v := ⟨hom.ofVector v, hom.ofVector.mem_range_self v⟩
+noncomputable def ofVectorRangeEquiv : V ≃ₗ[R] ℋ.ofVector.range := {
+  toFun v := ⟨ℋ.ofVector v, ℋ.ofVector.mem_range_self v⟩
   map_add' v w := by simp
   map_smul' r v := by simp
   invFun :=
-    (ofInjective hom.ofVector (linear_injective_iff _ |>.mpr ofPoint_injective)).invFun
+    (ofInjective ℋ.ofVector (linear_injective_iff _ |>.mpr ℋ.ofPoint_injective)).invFun
   left_inv :=
-    (ofInjective hom.ofVector (linear_injective_iff _ |>.mpr ofPoint_injective)).left_inv
+    (ofInjective ℋ.ofVector (linear_injective_iff _ |>.mpr ℋ.ofPoint_injective)).left_inv
   right_inv v' := by simp
 }
 
 /-- The affine equivalence between the affine space space and its embedding. -/
-public noncomputable def ofPointRangeEquiv : A ≃ᵃ[R] hom.ofPoint.range :=
+public noncomputable def ofPointRangeEquiv : A ≃ᵃ[R] ℋ.ofPoint.range :=
   .ofBijective
-    ⟨hom.ofPoint.rangeRestrict_injective_iff.mpr hom.ofPoint_injective, fun ⟨_, a, rfl⟩ => ⟨a, rfl⟩⟩
+    ⟨ℋ.ofPoint.rangeRestrict_injective_iff.mpr ℋ.ofPoint_injective, fun ⟨_, a, rfl⟩ => ⟨a, rfl⟩⟩
 
-lemma apply_ofPointRangeEquiv_symm (x : hom.ofPoint.range) :
-    hom.ofPoint (ofPointRangeEquiv.symm x) = x := by
-  rw [← ofPointRangeEquiv.right_inv x]
-  congr; exact ofPointRangeEquiv.symm_apply_apply _
+lemma apply_ofPointRangeEquiv_symm (x : ℋ.ofPoint.range) :
+    ℋ.ofPoint (ℋ.ofPointRangeEquiv.symm x) = x := by
+  rw [← ℋ.ofPointRangeEquiv.right_inv x]
+  congr; exact ℋ.ofPointRangeEquiv.symm_apply_apply _
 
 end IsHomogenization
 
diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean
index b830599e..dbed16a0 100644
--- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean
+++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean
@@ -34,84 +34,84 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 variable {x : A} {s : Set A}
 
-variable (R W) in
-def homogenize (s : Set A) : SubMulAction₀ R≥0 W := R≥0 ∙ (hom.ofPoint '' s)
+def homogenize (s : Set A) : SubMulAction₀ R≥0 W := R≥0 ∙ (ℋ.ofPoint '' s)
 
 -- potential notations for homogenization: `R≥0 ∙[W] s` or `R ∙₊[W] s`
 --
 -- /- Note that the character `∙` U+2219 used below is different from the scalar multiplication
 -- character `•` U+2022. -/
--- /-- Notation for the homogenizationof a set `s`, short for `homogenize R W s`. -/
--- scoped notation:70 R:70 " ∙[" W "] " s:70 => homogenize R W s
+-- /-- Notation for the homogenizationof a set `s`, short for `homogenize ℋ s`. -/
+-- scoped notation:70 R:70 " ∙[" W "] " s:70 => homogenize ℋ s
 
 lemma mem_homogenize {s : Set A} {x : W} :
-    x ∈ homogenize R W s ↔ x = 0 ∨ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • hom.ofPoint y := by
+    x ∈ homogenize ℋ s ↔ x = 0 ∨ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • ℋ.ofPoint y := by
   simp [homogenize, mem_smulSet]
 
-lemma mem_homogenize_iff_exist_lt_zero {s : Set A} {x : W} (hx : x ∈ homogenize R W s) :
-    x = 0 ∨ ∃ y ∈ s, ∃ r : R, 0 < r ∧ x = r • hom.ofPoint y := by
+variable {ℋ} in
+lemma mem_homogenize_iff_exist_lt_zero {s : Set A} {x : W} (hx : x ∈ homogenize ℋ s) :
+    x = 0 ∨ ∃ y ∈ s, ∃ r : R, 0 < r ∧ x = r • ℋ.ofPoint y := by
   obtain (rfl | ⟨y, ⟨z, hz, rfl⟩, _, ⟨r, _⟩, hr0, rfl⟩) := mem_smulSet_iff_exists_ne_zero hx
   · exact .inl rfl
   · exact .inr ⟨z, hz, r, by rwa [← zero_lt_iff] at hr0, rfl⟩
 
 lemma mem_homogenize_iff_ne_zero {s : Set A} {x : W} (hx : x ≠ 0) :
-    x ∈ homogenize R W s ↔ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • hom.ofPoint y := by
+    x ∈ homogenize ℋ s ↔ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • ℋ.ofPoint y := by
   simp [homogenize, mem_smulSet_of_ne_zero hx]
 
 lemma mem_homogenize_iff_nonempty {s : Set A} {x : W} (hs : s.Nonempty) :
-    x ∈ homogenize R W s ↔ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • hom.ofPoint y := by
-  have : (hom.ofPoint '' s).Nonempty := Set.image_nonempty.mpr hs
+    x ∈ homogenize ℋ s ↔ ∃ y ∈ s, ∃ r : R, 0 ≤ r ∧ x = r • ℋ.ofPoint y := by
+  have : (ℋ.ofPoint '' s).Nonempty := Set.image_nonempty.mpr hs
   simp [homogenize, mem_smulSet_of_nonempty this]
 
-@[simp] lemma homogenize_empty : homogenize R W (∅ : Set A) = ⊥ := by
+@[simp] lemma homogenize_empty : homogenize ℋ (∅ : Set A) = ⊥ := by
   ext x; simp [homogenize]
 
-lemma ofPoint_image_subset_homogenize : hom.ofPoint '' s ⊆ homogenize R W s :=
+lemma ofPoint_image_subset_homogenize : ℋ.ofPoint '' s ⊆ homogenize ℋ s :=
   subset_smulSet
 
-lemma ofPoint_mem_homogenize (hx : x ∈ s) : hom.ofPoint x ∈ homogenize R W s :=
-  ofPoint_image_subset_homogenize ⟨x, hx, rfl⟩
+lemma ofPoint_mem_homogenize (hx : x ∈ s) : ℋ.ofPoint x ∈ homogenize ℋ s :=
+  ofPoint_image_subset_homogenize _ ⟨x, hx, rfl⟩
 
 lemma smul_ofPoint_mem_homogenize {r : R} (hr : 0 ≤ r) (h : x ∈ s) :
-    r • hom.ofPoint x ∈ homogenize R W s :=
-  smul_mem _ ⟨r, hr⟩ (ofPoint_mem_homogenize h)
+    r • ℋ.ofPoint x ∈ homogenize ℋ s :=
+  smul_mem _ ⟨r, hr⟩ (ofPoint_mem_homogenize _ h)
 
-lemma homogenize_mono {s t : Set A} (h : s ⊆ t) : homogenize R W s ≤ homogenize R W t :=
+lemma homogenize_mono {s t : Set A} (h : s ⊆ t) : homogenize ℋ s ≤ homogenize ℋ t :=
   smulSet_mono <| Set.image_mono h
 
-lemma homogenize_monotone : Monotone (homogenize R W : Set A → SubMulAction₀ R≥0 W) :=
-  fun _ _ => homogenize_mono
+lemma homogenize_monotone : Monotone (homogenize ℋ : Set A → SubMulAction₀ R≥0 W) :=
+  fun _ _ => homogenize_mono _
 
 /-- Homogenization from sets to `SubMulAction₀` as an order homomorphism. -/
 def homogenizeOrderHom : Set A →o SubMulAction₀ R≥0 W where
-  toFun := homogenize R W
-  monotone' := homogenize_monotone
+  toFun := homogenize ℋ
+  monotone' := homogenize_monotone _
 
 lemma homogenize_union (s t : Set A) :
-    homogenize R W (s ∪ t) = homogenize R W s ⊔ homogenize R W t := by
+    homogenize ℋ (s ∪ t) = homogenize ℋ s ⊔ homogenize ℋ t := by
   simp only [homogenize, Set.image_union, smulSet_union]
 
 lemma homogenize_inter_le (s t : Set A) :
-    homogenize R W (s ∩ t) ≤ homogenize R W s ⊓ homogenize R W t := by
+    homogenize ℋ (s ∩ t) ≤ homogenize ℋ s ⊓ homogenize ℋ t := by
   unfold homogenize
-  rw [Set.image_inter hom.ofPoint_injective]
+  rw [Set.image_inter ℋ.ofPoint_injective]
   exact smulSet_inter_le _ _
 
 lemma homogenize_sSup (S : Set (Set A)) :
-    homogenize R W (sSup S) = sSup (homogenize R W '' S) := by
+    homogenize ℋ (sSup S) = sSup (homogenize ℋ '' S) := by
   unfold homogenize
   rw [Set.image_sSup, smulSet_sSup, Set.image_image]
 
 def homogenizeSSupHom : sSupHom (Set A) (SubMulAction₀ R≥0 W) where
-  toFun := homogenize R W
-  map_sSup' := homogenize_sSup
+  toFun := homogenize ℋ
+  map_sSup' := homogenize_sSup _
 
 lemma homogenize_sInf_le (S : Set (Set A)) :
-    homogenize R W (sInf S) ≤ sInf (homogenize R W '' S) := by
+    homogenize ℋ (sInf S) ≤ sInf (homogenize ℋ '' S) := by
   unfold homogenize
   apply le_trans <| smulSet_mono (Set.image_sInter_subset_sInf_image _ _)
   apply le_trans (smulSet_sInf_le _)
@@ -122,42 +122,42 @@ section Nontrivial
 variable [Nontrivial R]
 
 @[simp] lemma ofPoint_mem_homogenize_iff {x : A} {s : Set A} :
-    hom.ofPoint x ∈ homogenize R W s ↔ x ∈ s where
+    ℋ.ofPoint x ∈ homogenize ℋ s ↔ x ∈ s where
   mp := by
     rintro (h | ⟨x, ⟨y, hy, rfl⟩, r, h⟩)
-    · exfalso; exact ofPoint_ne_zero _ h
-    · have := congrArg hom.weight h
+    · exfalso; exact ofPoint_ne_zero _ _ h
+    · have := congrArg ℋ.weight h
       simp only [weight_one, ← Nonneg.coe_smul, map_smul, smul_eq_mul, mul_one,
         Eq.comm, Nonneg.coe_eq_one] at this
       rw [this, one_smul] at h
-      rwa [hom.ofPoint_injective h]
-  mpr := ofPoint_mem_homogenize
+      rwa [ℋ.ofPoint_injective h]
+  mpr := ofPoint_mem_homogenize _
 
 lemma ofPoint_mem_homogenize_singleton {x y : A} :
-    hom.ofPoint x ∈ homogenize R W {y} ↔ x = y := by simp
+    ℋ.ofPoint x ∈ homogenize ℋ {y} ↔ x = y := by simp
 
 lemma homogenize_injective :
-    Injective (homogenize R W : Set A → SubMulAction₀ R≥0 W) := by
+    Injective (homogenize ℋ : Set A → SubMulAction₀ R≥0 W) := by
   intro s t h; ext
   repeat rw [← ofPoint_mem_homogenize_iff (R := R) (W := W)]
   rw [h]
 
-@[simp] lemma homogenize_inj {s t : Set A} : homogenize R W s = homogenize R W t ↔ s = t :=
-  homogenize_injective.eq_iff
+@[simp] lemma homogenize_inj {s t : Set A} : homogenize ℋ s = homogenize ℋ t ↔ s = t :=
+  (homogenize_injective _).eq_iff
 
-lemma homogenize_strictMono : StrictMono (homogenize R W : Set A → SubMulAction₀ R≥0 W) :=
-  homogenize_monotone.strictMono_of_injective homogenize_injective
+lemma homogenize_strictMono : StrictMono (homogenize ℋ : Set A → SubMulAction₀ R≥0 W) :=
+  (homogenize_monotone _).strictMono_of_injective (homogenize_injective _)
 
 lemma homogenize_mono_iff {s t : Set A} :
-    homogenize R W s ≤ homogenize R W t ↔ s ⊆ t where
+    homogenize ℋ s ≤ homogenize ℋ t ↔ s ⊆ t where
   mp := by
     intro h x hx
     rw [← ofPoint_mem_homogenize_iff (R := R) (W := W)] at ⊢ hx
     exact h hx
-  mpr := homogenize_mono
+  mpr := homogenize_mono _
 
 lemma homogenize_singleton_eq {x y : A} :
-    homogenize R W {x} = homogenize R W {y} ↔ x = y := by simp
+    homogenize ℋ {x} = homogenize ℋ {y} ↔ x = y := by simp
 
 end Nontrivial
 
@@ -170,44 +170,43 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 variable {x : A} {s : Set A}
 
-variable (A) in
 def _root_.SubMulAction₀.dehomogenize (S : SubMulAction₀ R≥0 W) : Set A :=
-  hom.ofPoint ⁻¹' S
+  ℋ.ofPoint ⁻¹' S
 
 lemma dehomogenize_mono {S T : SubMulAction₀ R≥0 W} (h : S ≤ T) :
-    dehomogenize A S ≤ dehomogenize A T :=
+    dehomogenize ℋ S ≤ dehomogenize ℋ T :=
   Set.preimage_mono h
 
-lemma dehomogenize_monotone : Monotone (dehomogenize A : SubMulAction₀ R≥0 W → Set A) :=
-  fun _ _ => dehomogenize_mono
+lemma dehomogenize_monotone : Monotone (dehomogenize ℋ : SubMulAction₀ R≥0 W → Set A) :=
+  fun _ _ => dehomogenize_mono _
 
 /-- Homogenization from sets to `SubMulAction₀` as an order homomorphism. -/
 def dehomogenizeOrderHom : SubMulAction₀ R≥0 W →o Set A where
-  toFun := dehomogenize A
-  monotone' := dehomogenize_monotone
+  toFun := dehomogenize ℋ
+  monotone' := dehomogenize_monotone _
 
-lemma dehomogenize_top : dehomogenize A (⊤ : SubMulAction₀ R≥0 W) = Set.univ := by
+lemma dehomogenize_top : dehomogenize ℋ (⊤ : SubMulAction₀ R≥0 W) = Set.univ := by
   ext x; simp [dehomogenize]
 
 lemma dehomogenize_inf (s t : SubMulAction₀ R≥0 W) :
-    dehomogenize A (s ⊓ t) = dehomogenize A s ∩ dehomogenize A t := by
+    dehomogenize ℋ (s ⊓ t) = dehomogenize ℋ s ∩ dehomogenize ℋ t := by
   ext x; simp [dehomogenize]
 
 lemma dehomogenize_sup (s t : SubMulAction₀ R≥0 W) :
-    dehomogenize A (s ⊔ t) = dehomogenize A s ∪ dehomogenize A t := by
+    dehomogenize ℋ (s ⊔ t) = dehomogenize ℋ s ∪ dehomogenize ℋ t := by
   ext x; simp [dehomogenize]
 
 def dehomogenizeLatticeHom : LatticeHom (SubMulAction₀ R≥0 W) (Set A) where
-  toFun := dehomogenize A
-  map_sup' := dehomogenize_sup
-  map_inf' := dehomogenize_inf
+  toFun := dehomogenize ℋ
+  map_sup' := dehomogenize_sup _
+  map_inf' := dehomogenize_inf _
 
 lemma dehomogenize_sInf (S : Set (SubMulAction₀ R≥0 W)) :
-    dehomogenize A (sInf S) = sInf (dehomogenize A '' S) := by
+    dehomogenize ℋ (sInf S) = sInf (dehomogenize ℋ '' S) := by
   ext x; simp [dehomogenize]
 
 section Nontrivial
@@ -215,27 +214,27 @@ section Nontrivial
 variable [Nontrivial R]
 
 lemma dehomogenize_sSup (S : Set (SubMulAction₀ R≥0 W)) :
-    dehomogenize A (sSup S) = sSup (dehomogenize A '' S) := by
-  ext x; simpa [dehomogenize] using fun h => (ofPoint_ne_zero x h).elim
+    dehomogenize ℋ (sSup S) = sSup (dehomogenize ℋ '' S) := by
+  ext x; simpa [dehomogenize] using fun h => (ofPoint_ne_zero _ x h).elim
 
 def dehomogenizeCompleteLatticeHom : CompleteLatticeHom (SubMulAction₀ R≥0 W) (Set A) where
-  toFun := dehomogenize A
-  map_sInf' := dehomogenize_sInf
-  map_sSup' := dehomogenize_sSup
+  toFun := dehomogenize ℋ
+  map_sInf' := dehomogenize_sInf _
+  map_sSup' := dehomogenize_sSup _
 
-@[simp] lemma dehomogenize_bot : (⊥ : SubMulAction₀ R≥0 W).dehomogenize A = ∅ := by
-  ext x; simp only [Set.mem_empty_iff_false, iff_false]; exact ofPoint_ne_zero _
+@[simp] lemma dehomogenize_bot : (⊥ : SubMulAction₀ R≥0 W).dehomogenize ℋ = ∅ := by
+  ext x; simp only [Set.mem_empty_iff_false, iff_false]; exact ofPoint_ne_zero _ _
 
 variable [IsOrderedRing R] in
 /-- Dehomogenizing the homogenization of a set yields the same set again. -/
 @[simp] theorem dehomogenize_homogenize (s : Set A) :
-    dehomogenize A (homogenize R W s) = s := by
+    dehomogenize ℋ (homogenize ℋ s) = s := by
   ext x; simp [dehomogenize]
 
 end Nontrivial
 
 variable [IsOrderedRing R] in
-lemma homogenize_gc : GaloisConnection (homogenize R W) (dehomogenize A) :=
+lemma homogenize_gc : GaloisConnection (homogenize ℋ) (dehomogenize ℋ) :=
   .compose Set.image_preimage smulSet_gc
 
 end Ring_no_OrderedRing
@@ -247,32 +246,32 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 @[simp] lemma dehomogenize_weight_positive :
-    dehomogenize A (hom.weight.positive : SubMulAction₀ R≥0 W) = Set.univ := by
+    dehomogenize ℋ (ℋ.weight.positive : SubMulAction₀ R≥0 W) = Set.univ := by
   ext x; simp [dehomogenize, weight_one]
 
 lemma nonneg_smulSet_ofPoint_range_le_weight_positive :
-    R≥0 ∙ (Set.range hom.ofPoint) ≤ hom.weight.positive := by
+    R≥0 ∙ (Set.range ℋ.ofPoint) ≤ ℋ.weight.positive := by
   rw [ofPoint_range_eq_preimage_weight_one]
   exact nonneg_smulSet_preimage_one_le_positive _
 
 @[simp] lemma homogenize_univ_le_weight_positive :
-    homogenize R W (Set.univ : Set A) ≤ hom.weight.positive := by
-  simpa [homogenize] using nonneg_smulSet_ofPoint_range_le_weight_positive
+    homogenize ℋ (Set.univ : Set A) ≤ ℋ.weight.positive := by
+  simpa [homogenize] using nonneg_smulSet_ofPoint_range_le_weight_positive _
 
 lemma homogenize_le_weight_positive (s : Set A) :
-    homogenize R W s ≤ hom.weight.positive :=
-  le_trans (homogenize_mono (Set.subset_univ _)) homogenize_univ_le_weight_positive
+    homogenize ℋ s ≤ ℋ.weight.positive :=
+  le_trans (homogenize_mono _ (Set.subset_univ _)) (homogenize_univ_le_weight_positive _)
 
 @[simp] theorem homogenize_dehomogenize_le_weight_positive {S : SubMulAction₀ R≥0 W} :
-    homogenize R W (S.dehomogenize A) ≤ S ⊓ hom.weight.positive := by
-  have aux : Set.range hom.ofPoint = hom.ofPoint.range := rfl
+    homogenize ℋ (S.dehomogenize ℋ) ≤ S ⊓ ℋ.weight.positive := by
+  have aux : Set.range ℋ.ofPoint = ℋ.ofPoint.range := rfl
   rw [homogenize, dehomogenize, Set.image_preimage_eq_inter_range, aux]
   refine le_trans (smulSet_inter_le _ _) ?_
   simp only [smulSet_eq, le_inf_iff, inf_le_left, true_and]
-  exact le_trans inf_le_right nonneg_smulSet_ofPoint_range_le_weight_positive
+  exact le_trans inf_le_right (nonneg_smulSet_ofPoint_range_le_weight_positive _)
 
 end IsStrictOrderedRing
 
@@ -283,49 +282,49 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W] [Module.IsTorsionFree R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 /-- For the weaker version with `r = 1` see `ofPoint_mem_homogenize_iff`. -/
 @[simp] lemma smul_ofPoint_mem_homogenize_iff {r : R} (hr : 0 < r) {x : A} (s : Set A) :
-    r • hom.ofPoint x ∈ homogenize R W s ↔ x ∈ s where
+    r • ℋ.ofPoint x ∈ homogenize ℋ s ↔ x ∈ s where
   mp := by
     rintro (h | ⟨x, ⟨y, hy, rfl⟩, ⟨r', hr'⟩, h⟩)
     · exfalso
-      exact smul_ne_zero hr.ne.symm (ofPoint_ne_zero x) h
-    · have := congrArg hom.weight h
+      exact smul_ne_zero hr.ne.symm (ofPoint_ne_zero _ x) h
+    · have := congrArg ℋ.weight h
       simp only [map_smul, weight_one, smul_eq_mul, mul_one, Nonneg.mk_smul] at this
       rw [this] at hr h
-      rw [Nonneg.mk_smul, smul_right_inj hr.ne.symm, ofPoint_injective.eq_iff] at h
+      rw [Nonneg.mk_smul, smul_right_inj hr.ne.symm, ℋ.ofPoint_injective.eq_iff] at h
       rwa [h]
-  mpr := smul_ofPoint_mem_homogenize hr.le
+  mpr := smul_ofPoint_mem_homogenize _ hr.le
 
 lemma homogenize_inter (s t : Set A) :
-    homogenize R W (s ∩ t) = homogenize R W s ⊓ homogenize R W t := by
+    homogenize ℋ (s ∩ t) = homogenize ℋ s ⊓ homogenize ℋ t := by
   apply le_antisymm
-  · exact homogenize_inter_le s t
+  · exact homogenize_inter_le _ s t
   · rintro x hx
     obtain (rfl | ⟨y, hys, r, hr, rfl⟩) := mem_homogenize_iff_exist_lt_zero hx.1
     · exact SubMulAction₀.zero_mem
-    refine smul_ofPoint_mem_homogenize hr.le ⟨hys, ?_⟩
-    exact (smul_ofPoint_mem_homogenize_iff hr t).mp hx.2
+    refine smul_ofPoint_mem_homogenize _ hr.le ⟨hys, ?_⟩
+    exact (smul_ofPoint_mem_homogenize_iff _ hr t).mp hx.2
 
 /-- Homogenization from sets to `SubMulAction₀` as a lattice homomorphism. -/
 def homogenizeLatticeHom : LatticeHom (Set A) (SubMulAction₀ R≥0 W) where
-  toFun := homogenize R W
-  map_sup' := homogenize_union
-  map_inf' := homogenize_inter
+  toFun := homogenize ℋ
+  map_sup' := homogenize_union _
+  map_inf' := homogenize_inter _
 
 lemma homogenize_sInf {S : Set (Set A)} (hS : S.Nonempty) :
-    homogenize R W (sInf S) = sInf (homogenize R W '' S) := by
+    homogenize ℋ (sInf S) = sInf (homogenize ℋ '' S) := by
   apply le_antisymm
-  · exact homogenize_sInf_le S
+  · exact homogenize_sInf_le _ S
   intro x hx
   simp only [SetLike.mem_sInf, Set.mem_image, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂] at hx
   obtain (rfl | ⟨y, hys, r, hr, rfl⟩) := mem_homogenize_iff_exist_lt_zero (hx _ hS.choose_spec)
   · exact SubMulAction₀.zero_mem
-  exact smul_ofPoint_mem_homogenize hr.le fun t ht =>
-    (smul_ofPoint_mem_homogenize_iff hr t).mp (hx _ ht)
+  exact smul_ofPoint_mem_homogenize _ hr.le fun t ht =>
+    (smul_ofPoint_mem_homogenize_iff _ hr t).mp (hx _ ht)
 
 end IsCancelMulZero_IsTorsionFree
 
@@ -336,15 +335,15 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 lemma nonneg_smulSet_ofPoint_range :
-    R≥0 ∙ (Set.range hom.ofPoint) = hom.weight.positive := by
+    R≥0 ∙ (Set.range ℋ.ofPoint) = ℋ.weight.positive := by
   rw [ofPoint_range_eq_preimage_weight_one]
   exact nonneg_smulSet_preimage_one_eq_positive _
 
-@[simp] lemma homogenize_univ : homogenize R W (Set.univ : Set A) = hom.weight.positive := by
-  simpa [homogenize] using nonneg_smulSet_ofPoint_range
+@[simp] lemma homogenize_univ : homogenize ℋ (Set.univ : Set A) = ℋ.weight.positive := by
+  simpa [homogenize] using nonneg_smulSet_ofPoint_range _
 
 end DivisionRing
 
@@ -355,23 +354,24 @@ variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A]
 variable [AddCommGroup W] [Module R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 @[simp] theorem homogenize_dehomogenize {S : SubMulAction₀ R≥0 W} :
-    homogenize R W (S.dehomogenize A) = S ⊓ hom.weight.positive := by
+    homogenize ℋ (S.dehomogenize ℋ) = S ⊓ ℋ.weight.positive := by
   rw [homogenize, dehomogenize, Set.image_preimage_eq_inter_range, smulSet_inter_left,
     nonneg_smulSet_ofPoint_range]
 
+variable {ℋ} in
 @[simp] theorem homogenize_dehomogenize_of_le_weight_positive {S : SubMulAction₀ R≥0 W}
-    (hS : S ≤ hom.weight.positive) : homogenize R W (S.dehomogenize A) = S := by
+    (hS : S ≤ ℋ.weight.positive) : homogenize ℋ (S.dehomogenize ℋ) = S := by
   simp [homogenize_dehomogenize, hS]
 
-def homogenizeOrderIso : Set A ≃o Set.Iic (hom.weight.positive : SubMulAction₀ R≥0 W) where
-  toFun s := ⟨_, homogenize_le_weight_positive s⟩
-  invFun S := S.1.dehomogenize A
-  left_inv := dehomogenize_homogenize
+def homogenizeOrderIso : Set A ≃o Set.Iic (ℋ.weight.positive : SubMulAction₀ R≥0 W) where
+  toFun s := ⟨_, homogenize_le_weight_positive _ s⟩
+  invFun S := S.1.dehomogenize ℋ
+  left_inv := dehomogenize_homogenize _
   right_inv S := by simp only [homogenize_dehomogenize_of_le_weight_positive S.2]
-  map_rel_iff' := homogenize_mono_iff
+  map_rel_iff' := homogenize_mono_iff _
 
 end LinearOrderDivisionRing