Clean up Lattice.lean's namespaces

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

lean/Spa/Lattice.lean

@@ -61,12 +61,11 @@ class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where
   longestChain : PointedLTSeries α ⊥ ⊤ height
   chains_bounded : BoundedChains α height
 
-namespace FixedHeight
+namespace FiniteHeightLattice
 
-variable {α : Type*} [Lattice α] {h : ℕ}
+variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
 
-theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
+theorem bot_le (a : α) : (⊥ : α) ≤ a := by
-  intro a
   by_cases heq : ⊥ ⊓ a = ⊥
   · exact inf_eq_left.mp heq
   · exfalso
@@ -78,14 +77,6 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by
     rw [RelSeries.cons_length, lc.length_series] at hbound
     omega
 
-end FixedHeight
-
-namespace FiniteHeightLattice
-
-variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
-
-theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a
-
 end FiniteHeightLattice
 
 end Spa