-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ coheight a =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        a ≤
          RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
have apply : ∀
  (x :
    RelSeries (α := αᵒᵈ)
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}),
  Eq (α := ℕ∞)
    (⨆ (_ :
      a ≤
        RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (({
                toFun :=
                  RelSeries.reverse (r :=
                    {x : αᵒᵈ × αᵒᵈ |
                      match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                      | (a, b) => a < b}),
                invFun :=
                  RelSeries.reverse (r :=
                    SetRel.inv
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}),
                left_inv := sorry, right_inv := sorry } :
              (a :
                  RelSeries
                    {x : αᵒᵈ × αᵒᵈ |
                      match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                      | (a, b) => a < b}) →
                RelSeries
                  (SetRel.inv
                    {x : αᵒᵈ × αᵒᵈ |
                      match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                      | (a, b) => a < b}))
            x)),
      (↑(RelSeries.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (({
                  toFun :=
                    RelSeries.reverse (r :=
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}),
                  invFun :=
                    RelSeries.reverse (r :=
                      SetRel.inv
                        {x : αᵒᵈ × αᵒᵈ |
                          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                          | (a, b) => a < b}),
                  left_inv := sorry, right_inv := sorry } :
                (a :
                    RelSeries
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}) →
                  RelSeries
                    (SetRel.inv
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}))
              x)) :
        ℕ∞))
    (⨆ (_ :
      x.last (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b}) ≤
        a),
      (↑(x.length (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: apply Equiv.iSup_congr ⟨RelSeries.reverse, RelSeries.reverse, fun _ ↦ RelSeries.reverse_reverse _,
    fun _ ↦ RelSeries.reverse_reverse _⟩