diff --git a/lean/Spa/Isomorphism.lean b/lean/Spa/Isomorphism.lean
index ce900f8..d05b0cd 100644
--- a/lean/Spa/Isomorphism.lean
+++ b/lean/Spa/Isomorphism.lean
@@ -5,20 +5,18 @@ namespace Spa
 def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
     [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
     (hf : Monotone f) (hg : Monotone g)
-    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
     FiniteHeightLattice β where
   bot := f ⊥
   top := f ⊤
   height := I.height
   longestChain :=
     { series :=
-        I.longestChain.series.map f
-          (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
+        I.longestChain.series.map f (hf.strictMono_of_injective hgf.injective)
       head_series := congrArg f I.longestChain.head_series
       last_series := congrArg f I.longestChain.last_series
       length_series := I.longestChain.length_series }
   chains_bounded := fun c =>
-    I.chains_bounded
-      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
+    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
 
 end Spa
diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean
index 3bfd6bc..680e5da 100644
--- a/lean/Spa/Lattice/FiniteMap.lean
+++ b/lean/Spa/Lattice/FiniteMap.lean
@@ -516,7 +516,7 @@ def fixedHeight [FiniteHeightLattice B] (ks : List A) :
     FiniteHeightLattice (FiniteMap A B ks) :=
   FiniteHeightLattice.transport
     (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
-    (toIter_ofIter ks) (fun fm => ofIter_toIter fm)
+    (toIter_ofIter ks) ofIter_toIter
 
 instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
   fixedHeight ks