diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index d50c8fa..3957f4a 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -50,7 +50,7 @@ end Folds
 def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
   ∀ c : LTSeries α, c.length ≤ n
 
-structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where
+structure PointedLTSeries (α : Type*) (f t : α) (n : ℕ) [Preorder α] where
   series : LTSeries α
   head_series : series.head = f
   last_series : series.last = t
diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean
index 5959fba..a5763f6 100644
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -12,7 +12,11 @@ instance : FiniteHeightLattice PUnit where
   bot := PUnit.unit
   top := PUnit.unit
   height := 0
-  longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ }
+  longestChain :=
+    { series := RelSeries.singleton _ PUnit.unit
+      head_series := rfl
+      last_series := rfl
+      length_series := rfl }
   chains_bounded := boundedChains_of_subsingleton PUnit 0
 
 end Spa