diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
index e60a76b..485f77f 100644
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -13,15 +13,15 @@ namespace IterProd
 
 variable {A B : Type u}
 
-instance instLattice [Lattice A] [Lattice B] :
+instance lattice [Lattice A] [Lattice B] :
     ∀ k, Lattice (IterProd A B k)
   | 0 => inferInstanceAs (Lattice B)
-  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
+  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (lattice k)
 
-instance instDecidableEq [DecidableEq A] [DecidableEq B] :
+instance decidableEq [DecidableEq A] [DecidableEq B] :
     ∀ k, DecidableEq (IterProd A B k)
   | 0 => inferInstanceAs (DecidableEq B)
-  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
+  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (decidableEq k)
 
 def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
   | 0 => b
@@ -32,9 +32,9 @@ variable [Lattice A] [Lattice B]
 def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
     ∀ k, FiniteHeightLattice (IterProd A B k)
   | 0 => inferInstanceAs (FiniteHeightLattice B)
-  | k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)
+  | k + 1 => @Spa.prod A (IterProd A B k) _ (lattice k) _ (fixedHeight k)
 
-instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
+instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
     FiniteHeightLattice (IterProd A B k) := fixedHeight k
 
 theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :