-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
apply :
  ∀
    (x :
      RelSeries (α := αᵒᵈ)
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b}),
    Eq (α := ℕ∞)
      (⨆ (_ :
        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 := ⋯, right_inv := ⋯ } :
                (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) =
          a),
        (↑(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 := ⋯, right_inv := ⋯ } :
                  (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})) :
          ℕ∞))
⊢ Eq (α := ℕ∞)
    (⨆ (p : LTSeries αᵒᵈ),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : αᵒᵈ × αᵒᵈ |
                match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.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 _⟩

Premises used: RelSeries.reverse, Equiv.mk, Equiv.iSup_congr