feat: Generalize OFE over the type of step indices

Iris/Iris/Algebra.lean

@@ -34,6 +34,7 @@ public import Iris.Algebra.OFE
 public import Iris.Algebra.Porting
 public import Iris.Algebra.ReservationMap
 public import Iris.Algebra.StepIndex
+public import Iris.Algebra.StepIndexFinite
 public import Iris.Algebra.UFrac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.UPred

Iris/Iris/Algebra/Agree.lean

@@ -6,11 +6,13 @@ Authors: Leo Stefanesco, Puming Liu, Sergei Stepanenko
 module
 
 public import Iris.Algebra.CMRA
-public import Iris.Algebra.OFE
+public import Iris.Algebra.StepIndexFinite
 public import Iris.Algebra.IsOp
 
 @[expose] public section
 
+local stepindex Nat
+
 namespace Iris
 
 /-!
@@ -272,7 +274,7 @@ theorem mem_of_forall_dist {a : α} {l : List α} (h : ∀ n, ∃ b ∈ l, a ≡
     by_cases hc : a = c
     · exact hc ▸ List.mem_cons_self
     · refine List.mem_cons_of_mem _ (ih fun n => ?_)
-      obtain ⟨n₀, hn₀⟩ := Classical.not_forall.mp fun hall => hc (OFE.eq_dist_2 hall)
+      obtain ⟨n₀, hn₀⟩ := Classical.not_forall.mp fun hall => hc (OFE.eq_of_dist hall)
       obtain ⟨b, hb, hd⟩ := h (max n n₀)
       rcases List.mem_cons.mp hb with rfl | hb'
       · exact absurd (hd.le (Nat.le_max_right n n₀)) hn₀
@@ -382,16 +384,16 @@ theorem dist_mk {n} {x y : Raw α} : mk x ≡{n}≡ mk y ↔ Raw.dist n x y := .
 
 @[rocq_alias agree_comm]
 theorem op_comm {x y : Agree α} : op x y = op y x :=
-  OFE.eq_dist_2 (ind₂ (fun _ _ => Raw.op_comm) x y)
+  OFE.eq_of_dist (ind₂ (fun _ _ => Raw.op_comm) x y)
 
 theorem op_commN {x y : Agree α} : op x y ≡{n}≡ op y x := op_comm.dist
 
 @[rocq_alias agree_assoc]
 theorem op_assoc {x y z : Agree α} : op x (op y z) = op (op x y) z :=
-  OFE.eq_dist_2 (ind₃ (fun _ _ _ => Raw.op_assoc) x y z)
+  OFE.eq_of_dist (ind₃ (fun _ _ _ => Raw.op_assoc) x y z)
 
 theorem op_idemp {x : Agree α} : op x x = x :=
-  OFE.eq_dist_2 (x.ind fun _ => Raw.idemp)
+  OFE.eq_of_dist (x.ind fun _ => Raw.idemp)
 
 @[rocq_alias agree_validN_ne]
 theorem validN_ne {x y : Agree α} : x ≡{n}≡ y → validN n x → validN n y :=
@@ -418,7 +420,7 @@ theorem op_invN {x y : Agree α} : validN n (op x y) → x ≡{n}≡ y :=
 
 @[rocq_alias agree_op_inv]
 theorem op_inv {x y : Agree α} : valid (op x y) → x = y :=
-  ind₂ (fun _ _ h => OFE.eq_dist_2 (Raw.op_inv h)) x y
+  ind₂ (fun _ _ h => OFE.eq_of_dist (Raw.op_inv h)) x y
 
 @[instance_reducible] def cmraData : CMRAData (Agree α) where
   pcore := some
@@ -470,7 +472,7 @@ theorem idemp {x : Agree α} : x • x = x := op_idemp
 #rocq_ignore to_agree_op_inv "Use the general Agree.op_inv theorem"
 
 instance instDiscrete [OFE.Discrete α] : OFE.Discrete (Agree α) where
-  discrete_0 {x y} := ind₂ (fun _ _ h => OFE.eq_dist_2 (Raw.discrete_0 h)) x y
+  discrete_0 {x y} := ind₂ (fun _ _ h => OFE.eq_of_dist (Raw.discrete_0 h)) x y
 
 @[rocq_alias agree_cmra_discrete]
 instance instORADiscrete [OFE.Discrete α] : ORA.Discrete (Agree α) where
@@ -489,7 +491,7 @@ theorem ordN {x y : Agree α} : x ≼ₒ{n} y ↔ y ≡{n}≡ y • x := by
 theorem includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x := incN_iff_ordN.trans ordN
 
 theorem ord {x y : Agree α} : x ≼ₒ y ↔ y = y • x :=
-  ⟨fun ⟨z, h⟩ => OFE.eq_dist_2 fun _ => ordN.mp ⟨z, h.dist⟩, fun h => ⟨y, h.trans op_comm⟩⟩
+  ⟨fun ⟨z, h⟩ => OFE.eq_of_dist fun _ => ordN.mp ⟨z, h.dist⟩, fun h => ⟨y, h.trans op_comm⟩⟩
 
 @[rocq_alias agree_included]
 theorem included {x y : Agree α} : x ≼ y ↔ y = y • x := inc_iff_ord.trans ord
@@ -541,7 +543,7 @@ theorem Agree.toAgree_injN {a b : α} : toAgree a ≡{n}≡ toAgree b → a ≡{
 
 @[rocq_alias to_agree_inj]
 theorem Agree.toAgree_inj {a b : α} : toAgree a = toAgree b → a = b :=
-  fun heq => OFE.eq_dist_2 fun _ => toAgree_injN heq.dist
+  fun heq => OFE.eq_of_dist fun _ => toAgree_injN heq.dist
 
 @[simp] theorem Agree.toAgree_validN {a : α} : ✓{n} toAgree a := Raw.toAgree_validN (a := a) (n := n)
 
@@ -554,7 +556,7 @@ theorem Agree.toAgree_uninjN {x : Agree α} : ✓{n} x → ∃ a, toAgree a ≡{
 
 @[rocq_alias to_agree_uninj]
 theorem Agree.toAgree_uninj {x : Agree α} : ✓ x → ∃ a, toAgree a = x :=
-  x.ind fun _ h => (Raw.toAgree_uninj h).imp fun _ h => OFE.eq_dist_2 fun n => h n
+  x.ind fun _ h => (Raw.toAgree_uninj h).imp fun _ h => OFE.eq_of_dist fun n => h n
 
 instance toAgree.ne : OFE.NonExpansive (toAgree : α → Agree α) := instNonExpansive_toAgree
 
@@ -614,7 +616,7 @@ theorem toAgree_op_validN_iff_dist {a b : α} :
 
 @[rocq_alias to_agree_discrete]
 instance toAgree.is_discrete {a : α} [OFE.DiscreteE a] : OFE.DiscreteE (toAgree a) where
-  discrete {y} := y.ind fun _ h => OFE.eq_dist_2 (Raw.toAgree_discrete h)
+  discrete {y} := y.ind fun _ h => OFE.eq_of_dist (Raw.toAgree_discrete h)
 
 end Agree
 
@@ -684,7 +686,7 @@ theorem Agree.map_ne {f g : α → β} [OFE.NonExpansive f] [OFE.NonExpansive g]
 @[rocq_alias agree_map_ext]
 theorem Agree.agree_map_ext {f g : α → β} [OFE.NonExpansive f] [OFE.NonExpansive g] {x : Agree α}
     (H : ∀ a, f a = g a) : map f x = map g x :=
-  OFE.eq_dist_2 fun _ => map_ne (H · |>.dist)
+  OFE.eq_of_dist fun _ => map_ne (H · |>.dist)
 
 @[rocq_alias agree_map_id]
 theorem Agree.map_id (x : Agree α) : Agree.map id x = x :=

Iris/Iris/Algebra/Auth.lean

@@ -18,6 +18,8 @@ The authoritative camera has 2 types of elements:
 
 @[expose] public section
 
+local stepindex Nat
+
 open Iris
 
 open OFE ORA UORA View
@@ -120,15 +122,15 @@ nonrec theorem auth_dist_inj {n : Nat} {dq1 dq2 : DFrac} {a1 a2 : A}
 @[rocq_alias auth_auth_inj]
 theorem auth_inj {dq1 dq2 : DFrac} {a1 a2 : A} (h : (●{dq1} a1) = ●{dq2} a2) :
     dq1 = dq2 ∧ a1 = a2 :=
-  ⟨auth_inj_frac (n := 0) h.dist, OFE.eq_dist_2 fun _ => dist_of_auth_dist h.dist⟩
+  ⟨auth_inj_frac (n := 0) h.dist, OFE.eq_of_dist fun _ => dist_of_auth_dist h.dist⟩
 
 @[rocq_alias auth_frag_dist_inj]
 theorem frag_dist_inj {n : Nat} {b1 b2 : A} (h : (◯ b1 : Auth A) ≡{n}≡ ◯ b2) : b1 ≡{n}≡ b2 :=
   dist_of_frag_dist h
 
 @[rocq_alias auth_frag_inj]
 theorem frag_inj {b1 b2 : A} (h : (◯ b1 : Auth A) = ◯ b2) : b1 = b2 :=
-  OFE.eq_dist_2 fun _ => dist_of_frag_dist h.dist
+  OFE.eq_of_dist fun _ => dist_of_frag_dist h.dist
 
 @[rocq_alias auth_auth_discrete]
 nonrec instance auth_discrete {dq : DFrac} {a : A} [DiscreteE a] [DiscreteE (unit : A)] :

Iris/Iris/Algebra/BigOp.lean

@@ -17,6 +17,8 @@ public import Iris.Std.Equivalence
 
 namespace Iris.Algebra
 
+local stepindex Nat
+
 /-! # Big Operators
 
 This file defines big operators (fold operations) at the abstract OFE level.

Iris/Iris/Algebra/CMRA.lean

@@ -5,11 +5,13 @@ Authors: Mario Carneiro, Сухарик (@suhr), Markus de Medeiros, Puming Liu,
 -/
 module
 
-public import Iris.Algebra.OFE
+public import Iris.Algebra.StepIndexFinite
 public import Iris.Algebra.Monoid
 
 @[expose] public section
 
+local stepindex Nat
+
 namespace Iris
 open OFE
 
@@ -1288,7 +1290,7 @@ section cancelableElements
 
 @[rocq_alias cancelable]
 theorem cancelable {x y z : α} [Cancelable x] (v : ✓ (x • y)) (e : x • y = x • z) : y = z :=
-  OFE.eq_dist_2 fun _ => cancelableN v.validN e.dist
+  OFE.eq_of_dist fun _ => cancelableN v.validN e.dist
 
 @[rocq_alias discrete_cancelable]
 theorem discrete_cancelable {x : α} [Discrete α]
@@ -1558,7 +1560,7 @@ infixr:25 " -C> " => Hom
 instance [ORA β] : CoeFun (α -C> β) (fun _ => α → β) := ⟨fun F => F.f⟩
 
 instance [ORA β] : OFE (α -C> β) where
-  Dist n f g := f.toHom ≡{n}≡ g.toHom
+  dist n f g := f.toHom ≡{n}≡ g.toHom
   dist_eqv := {
     refl _ := dist_eqv.refl _
     symm h := dist_eqv.symm h
@@ -2138,13 +2140,15 @@ def raPCore : PCore (Option α) where
   pcore x := some (optionCore x)
   pcore_ne {n} x y cx H := by
     simp only [Option.some.injEq]; rintro rfl
-    rcases x, y with ⟨_|x, _|y⟩ <;> simp_all [Dist, Option.Forall₂]
-    cases Hv : pcore x <;> cases Hv' : pcore y <;> simp only []
-    · cases pcore_ne H.symm Hv'; simp_all
-    · cases pcore_ne H Hv; simp_all
-    · obtain ⟨w, Hw1, Hw2⟩ := pcore_ne H.symm Hv'
-      cases Hv.symm.trans Hw1
-      exact Hw2.symm
+    refine ⟨_, rfl, ?_⟩
+    rcases x, y with ⟨_|x, _|y⟩ <;> simp_all [optionCore]
+    cases Hv : pcore x <;> cases Hv' : pcore y
+    · rfl
+    · obtain ⟨_, Hw, -⟩ := pcore_ne H.symm Hv'; simp_all
+    · obtain ⟨_, Hw, -⟩ := pcore_ne H Hv; simp_all
+    · obtain ⟨_, Hw1, Hw2⟩ := pcore_ne H Hv
+      cases Hv'.symm.trans Hw1
+      exact Hw2
   pcore_idem := by
     rintro (_|x) <;> simp
     rcases H : pcore x with _|y <;> simp
@@ -2155,7 +2159,7 @@ def raValid : _root_.Iris.Valid (Option α) where
   ValidN := optionValidN
   Valid := optionValid
   validN_ne {n} x y H := by
-    rcases x, y with ⟨_|_, _|_⟩ <;> simp_all [Dist, Option.Forall₂]
+    rcases x, y with ⟨_|_, _|_⟩ <;> simp_all [Dist]
     exact Dist.validN H |>.mp
   valid_iff_validN {x} := by
     rcases x with ⟨_|_⟩ <;> simp [valid_iff_validN]
@@ -2166,7 +2170,7 @@ def raValid : _root_.Iris.Valid (Option α) where
   OrderN := optionOrderN
   Order := optionOrder
   ordN_ne {n x x' y y'} ex ey h := by
-    rcases x, x', y, y' with ⟨_|x, _|x', _|y, _|y'⟩ <;> simp_all [Dist, Option.Forall₂]
+    rcases x, x', y, y' with ⟨_|x, _|x', _|y, _|y'⟩ <;> simp_all [Dist]
     · exact h.of_dist ey
     · exact Ordered.OrderNR.ne ex ey h
   ordN_succ {n x y} h := by
@@ -2941,8 +2945,8 @@ abbrev Order (x y : α × β) := x.fst ≼ₒ y.fst ∧ x.snd ≼ₒ y.snd
 def raOp : Op (α × β) where
   op := op
   op_ne.ne _ _ _ h := dist_prod_ext (Dist.op_r <| dist_fst h) (Dist.op_r <| dist_snd h)
-  assoc := equiv_prod_ext assoc assoc
-  comm := equiv_prod_ext comm comm
+  assoc := Prod.ext assoc assoc
+  comm := Prod.ext comm comm
 
 @[reducible, rocq_alias prod_pcore_instance]
 def raPCore : PCore (α × β) where
@@ -2961,7 +2965,7 @@ def raPCore : PCore (α × β) where
     have ⟨cx₂, hcx₂, hcx⟩ := Option.bind_eq_some_iff.mp this
     have ⟨a, ha, ea⟩ := equiv_some (pcore_idem hcx₁)
     have ⟨b, hb, eb⟩ := equiv_some (pcore_idem hcx₂)
-    have g : (a, b) = (cx₁, cx₂) := equiv_prod_ext ea eb
+    have g : (a, b) = (cx₁, cx₂) := Prod.ext ea eb
     rw [Option.some.inj hcx.symm]
     simp only [ha, hb, pcore]
     exact congrArg some g
@@ -3017,11 +3021,11 @@ instance cmraProd : ORA (α × β) where
   pcore_op_left h :=
     let ⟨_, ha, ho⟩ := Option.bind_eq_some_iff.mp h
     let ⟨_, hb, hh⟩ := Option.bind_eq_some_iff.mp ho
-    (Option.some.inj hh) ▸ (equiv_prod_ext (pcore_op_left ha) (pcore_op_left hb))
+    (Option.some.inj hh) ▸ (Prod.ext (pcore_op_left ha) (pcore_op_left hb))
   extend := fun ⟨vx₁, vx₂⟩ e =>
     let ⟨z₁, w₁, hx₁, hz₁, hw₁⟩ := extend vx₁ (OFE.dist_fst e)
     let ⟨z₂, w₂, hx₂, hz₂, hw₂⟩ := extend vx₂ (OFE.dist_snd e)
-    ⟨(z₁, z₂), (w₁, w₂), equiv_prod_ext hx₁ hx₂, ⟨hz₁, hz₂⟩, ⟨hw₁, hw₂⟩⟩
+    ⟨(z₁, z₂), (w₁, w₂), Prod.ext hx₁ hx₂, ⟨hz₁, hz₂⟩, ⟨hw₁, hw₂⟩⟩
   toOrdered := raOrdered
   op_monoN_left_ord z h := ⟨op_monoN_left_ord z.1 h.1, op_monoN_left_ord z.2 h.2⟩
   op_mono_left_ord z h := ⟨op_mono_left_ord z.1 h.1, op_mono_left_ord z.2 h.2⟩
@@ -3342,7 +3346,7 @@ def Prod.mapC (f : A -C> A') (g : B -C> B') : A × B -C> A' × B' where
       cases _ : ORA.pcore (f.f x.fst) <;>
       cases _ : ORA.pcore (g.f x.snd) <;>
       simp_all
-  op x y := equiv_prod_ext (f.op x.fst y.fst) (g.op x.snd y.snd)
+  op x y := Prod.ext (f.op x.fst y.fst) (g.op x.snd y.snd)
   monoN_ord h := ⟨f.monoN_ord h.1, g.monoN_ord h.2⟩
   mono_ord h := ⟨f.mono_ord h.1, g.mono_ord h.2⟩
   increasing h :=
@@ -3359,9 +3363,9 @@ instance instRFunctorProdOF [RFunctor F1] [RFunctor F2] : RFunctor (ProdOF F1 F2
   map f g := Prod.mapC (map f g) (map f g)
   map_ne.ne _ _ _ Hx _ _ Hy _ :=
     Prod.map_ne (fun _ => map_ne.ne Hx Hy _) (fun _ => map_ne.ne Hx Hy _)
-  map_id _ := equiv_prod_ext (map_id _) (map_id _)
+  map_id _ := Prod.ext (map_id _) (map_id _)
   map_comp _ _ _ _ _ :=
-    equiv_prod_ext (map_comp _ _ _ _ _) (map_comp _ _ _ _ _)
+    Prod.ext (map_comp _ _ _ _ _) (map_comp _ _ _ _ _)
 
 instance instRFunctorAffineProdOF [RFunctor F1] [RFunctor F2] [RFunctorAffine F1]
     [RFunctorAffine F2] : RFunctorAffine (ProdOF F1 F2) where
@@ -3380,9 +3384,9 @@ instance instURFunctorProdOF [URFunctor F1] [URFunctor F2] : URFunctor (ProdOF F
   map f g := Prod.mapC (URFunctor.map f g) (URFunctor.map f g)
   map_ne.ne _ _ _ Hx _ _ Hy _ :=
     Prod.map_ne (fun _ => URFunctor.map_ne.ne Hx Hy _) (fun _ => URFunctor.map_ne.ne Hx Hy _)
-  map_id _ := equiv_prod_ext (URFunctor.map_id _) (URFunctor.map_id _)
+  map_id _ := Prod.ext (URFunctor.map_id _) (URFunctor.map_id _)
   map_comp _ _ _ _ _ :=
-    equiv_prod_ext (URFunctor.map_comp _ _ _ _ _) (URFunctor.map_comp _ _ _ _ _)
+    Prod.ext (URFunctor.map_comp _ _ _ _ _) (URFunctor.map_comp _ _ _ _ _)
 
 @[rocq_alias prodURF_contractive]
 instance instURFunctorContractiveProdOF

Iris/Iris/Algebra/CMRABigOp.lean

@@ -10,6 +10,8 @@ public import Iris.Algebra.CMRA
 
 @[expose] public section
 
+local stepindex Nat
+
 namespace Iris.Algebra
 open ORA
 

Iris/Iris/Algebra/COFESolver.lean

@@ -5,10 +5,12 @@ Authors: Mario Carneiro, Sebastian Graf
 -/
 module
 
-public import Iris.Algebra.OFE
+public import Iris.Algebra.StepIndexFinite
 
 @[expose] public section
 
+local stepindex Nat
+
 #rocq_ignore solution "Use OFE.iso + Inhabited + COFE"
 
 namespace Iris.COFE.OFunctor
@@ -56,10 +58,10 @@ def down (k : Nat) : A F (k+1) -n> A F k := (updown F k).2
 @[rocq_alias solver.gf]
 theorem down_up : ∀ {k} x, down F k (up F k x) = x
   | 0, ⟨()⟩ => rfl
-  | _+1, x => OFE.eq_dist_2 fun _ => (map_comp _ _ _ _ _).dist.symm.trans <|
-    Dist.trans
-      (map_ne.ne (fun y => (down_up y).dist) (fun y => (down_up y).dist) x)
-      (map_id _).dist
+  | _+1, x =>
+    have h : (down F _).comp (up F _) = Hom.id := Hom.ext (funext down_up)
+    OFE.eq_of_dist fun _ => (map_comp _ _ _ _ _).dist.symm.trans <|
+      Dist.trans (map_ne.ne h.dist h.dist x) (map_id _).dist
 
 @[rocq_alias solver.fg]
 theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ x := by
@@ -78,13 +80,15 @@ instance : CoeFun (Tower F) (fun _ => ∀ k, A F k) := ⟨Tower.val⟩
 
 @[rocq_alias solver.T]
 instance : OFE (Tower F) where
-  Dist n f g := ∀ k, f k ≡{n}≡ g k
+  dist n f g := ∀ k, f k ≡{n}≡ g k
   dist_eqv := {
     refl _ _ := dist_eqv.refl _
     symm h _ := dist_eqv.symm (h _)
     trans h1 h2 _ := dist_eqv.trans (h1 _) (h2 _)
   }
-  eq_dist' {_ _} := by rw [Tower.ext_iff, funext_iff]; simpa only [eq_dist] using forall_comm
+  eq_dist' {_ _} := by
+    rw [Tower.ext_iff, funext_iff]
+    exact (forall_congr' fun _ => eq_dist).trans forall_comm
   dist_lt h1 h2 _ := dist_lt (h1 _) h2
 
 #rocq_ignore solver.tower_equiv "Included in OFE (Tower F) instance"
@@ -99,10 +103,13 @@ def towerChain (c : Chain (Tower F)) (k : Nat) : Chain (A F k) where
 instance : COFE (Tower F) where
   compl c := by
     refine ⟨fun k => compl ⟨fun i => c.1 i k, fun h => c.cauchy h k⟩, ?_⟩
-    refine OFE.eq_dist_2 (fun n => ?_)
+    refine OFE.eq_of_dist (fun n => ?_)
     refine ((down ..).ne.1 conv_compl).trans <| .trans ?_ conv_compl.symm
     exact (c.chain n).down.dist
   conv_compl _ := conv_compl
+  lbcompl := (·.elim)
+  conv_lbcompl := (·.elim)
+  lbcompl_ne := (·.elim)
 
 #rocq_ignore solver.tower_cofe "Use IsCOFE instance"
 #rocq_ignore solver.tower_compl "Use IsCOFE instance"
@@ -206,7 +213,7 @@ protected def Tower.embed (k) : A F k -n> Tower F := by
 @[rocq_alias solver.embed_f]
 theorem Tower.embed_up (x : A F k) :
     Tower.embed (k+1) (up F k x) = Tower.embed k x := by
-  refine OFE.eq_dist_2 (fun (n : Nat) i => ?_)
+  refine OFE.eq_of_dist (fun (n : Nat) i => ?_)
   dsimp [Tower.embed, embed]; split <;> rename_i h₁
   · simp [Nat.le_of_succ_le h₁]
     suffices ∀ a b (e₁ : k + 1 + a = i) (e₂ : k+b = i),
@@ -265,7 +272,7 @@ def unfoldChain (X : Tower F) : Chain (F (Tower F) (Tower F)) where
 def Tower.isoAux : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
   hom.f X := {
     val n := (down F n).comp (map (Tower.embed _) (Tower.proj _)) X
-    down {n} := OFE.eq_dist_2 fun m => (down ..).ne.1 <|
+    down {n} := OFE.eq_of_dist fun m => (down ..).ne.1 <|
       (map_comp _ _ _ _ _).dist.symm.trans <|
         map_ne.ne (fun Y => (Tower.embed_up Y).dist) (fun Y => Y.down.dist) _
   }
@@ -274,7 +281,7 @@ def Tower.isoAux : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
   inv.ne.1 n _ _ h := by
     refine conv_compl.trans <| .trans ?_ conv_compl.symm
     exact (map ..).ne.1 (h (n+1))
-  hom_inv {X} := OFE.eq_dist_2 fun n => by
+  hom_inv {X} := OFE.eq_of_dist fun n => by
     intro k
     refine ((down ..).ne.1 (.trans ?_ (X.downN n).dist)).trans X.down.dist
     refine ((map ..).ne.1 (conv_compl.trans
@@ -303,7 +310,7 @@ def Tower.isoAux : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
         refine (map_comp _ _ _ _ _).dist.trans <|
           (ih (Nat.succ.inj e) _).trans (congrArg (fun a => (downN ..) a) ?_).dist
         exact (down_eqToHom _).symm
-  inv_hom := OFE.eq_dist_2 fun n => by
+  inv_hom := OFE.eq_of_dist fun n => by
     refine (conv_compl' n.le_succ).trans ?_
     dsimp [unfoldChain]; rw [down]
     refine ((map_comp _ _ _ _ _).trans