awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
H :
  (∀ ⦃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})) :
            ℕ∞) ≤
          n) ↔
    ⨆ (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})) :
            ℕ∞) ≤
      n
H₁ H₂ :
  (∀ ⦃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})) :
            ℕ∞) ≤
          n) ↔
    ∀ (i : LTSeries α)
      (j :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i =
          a),
      (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
⊢ height a ≤ n ↔
    ⨆ (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})) :
            ℕ∞) ≤
      n

Tactic:
rw [height_le_iff', iSup₂_le_iff]

Premises used: iSup₂_le_iff, Order.height_le_iff'
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
rw :
  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})) :
          ℕ∞))
⊢ height a =
    ⨆ (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:
rw [height_eq_iSup_last_eq]

Premises used: Order.height_eq_iSup_last_eq
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ∀
    (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})) :
          ℕ∞))

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
rw :
  ⨆ (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})) :
            ℕ∞) ≤
      n ↔
    ∀ ⦃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})) :
            ℕ∞) ≤
          n
rw₁ rw₂ :
  (∀ (i : LTSeries α)
      (j :
        RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i =
          a),
      (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) ↔
    ∀ ⦃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})) :
            ℕ∞) ≤
          n
⊢ coheight a ≤ n ↔
    ∀ ⦃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})) :
            ℕ∞) ≤
          n

Tactic:
rw [coheight_eq_iSup_head_eq, iSup₂_le_iff]

Premises used: Order.coheight_eq_iSup_head_eq, iSup₂_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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})) :
          ℕ∞) ≤
        n
⊢ coheight a ≤ n

Tactic:
coheight_le_iff'.mpr h

Premises used: Iff.mpr, Order.coheight_le_iff'
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
pos :
  ∀
    (hlen0 :
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
    (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x
neg :
  ∀
    (hlen0 :
      ¬p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
    (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
by_cases hlen0 : p.length ≠ 0

Premises used: RelSeries.length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
hab :
  (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      ⟨p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) -
            1,
          ⋯⟩.succ
hbc :
  p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) -
              1,
            ⋯⟩ :
          Fin
            (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}))).succ ≤
    x
b : α
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    ((RelSeries.eraseLast (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}),
      x)

Tactic:
apply lt_of_lt_of_le

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
⊢ p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      1 <
    p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
⊢ (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      ⟨p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) -
            1,
          ⋯⟩.succ

Tactic:
apply p.step ⟨p.length - 1, by lia⟩

Premises used: HSub.hSub, Fin.mk, RelSeries.length, RelSeries.step, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x

Tactic:
hlast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
h :
  p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) -
              1,
            ⋯⟩ :
          Fin
            (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}))).succ =
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p
⊢ p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) -
              1,
            ⋯⟩ :
          Fin
            (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}))).succ ≤
    x

Tactic:
convert! hlast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
h :
  p.toFun (r := {x : α × α | x.1 < x.2})
      (⟨p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1, ⋯⟩ : Fin (p.length (r := {x : α × α | x.1 < x.2}) + 1)) =
    p.toFun (r := {x : α × α | x.1 < x.2}) ⟨p.length (r := {x : α × α | x.1 < x.2}), ⋯⟩
⊢ p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) -
              1,
            ⋯⟩ :
          Fin
            (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}))).succ =
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p

Tactic:
simp only [Fin.succ_mk, RelSeries.last, Fin.last]

Premises used: RelSeries.last, Fin.succ_mk, Fin.last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
h : p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1 = p.length (r := {x : α × α | x.1 < x.2})
⊢ p.toFun (r := {x : α × α | x.1 < x.2})
      (⟨p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1, ⋯⟩ : Fin (p.length (r := {x : α × α | x.1 < x.2}) + 1)) =
    p.toFun (r := {x : α × α | x.1 < x.2}) ⟨p.length (r := {x : α × α | x.1 < x.2}), ⋯⟩

Tactic:
congr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
⊢ p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1 = p.length (r := {x : α × α | x.1 < x.2})

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
this :
  (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
⊢ HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x

Tactic:
simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.coe_sub,
        Nat.cast_one, p'] at this

Premises used: RelSeries.snoc_length, Nat.cast_add, ENat.coe_sub, RelSeries.eraseLast_length, Nat.cast_one
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
this : HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x
⊢ HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x

Tactic:
this
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
this : HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
convert! this
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
this : HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x
h :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1

Tactic:
norm_cast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
this : HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1 ≤ height x
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1

Tactic:
lia