awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ 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
have 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
Tactic: rw [coheight_eq_iSup_head_eq, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have 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
Tactic: by_cases hlen0 : p.length ≠ 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have 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
Tactic: by_cases hlen0 : p.length ≠ 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ 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)
have 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,
        sorry⟩.succ
Tactic: apply lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ 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)
have 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,
          sorry⟩ :
        Fin
          (p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))).succ ≤
  x
Tactic: apply lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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
have 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,
          sorry⟩ :
        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: convert! hlast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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
have h : p.toFun (r := {x : α × α | x.1 < x.2})
    (⟨p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1, sorry⟩ : 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}), sorry⟩
Tactic: simp only [Fin.succ_mk, RelSeries.last, Fin.last]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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}), ⋯⟩
have h : p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1 = p.length (r := {x : α × α | x.1 < x.2})
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
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
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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})) :
      ℕ∞) ≤
    height x
have 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
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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})) :
      ℕ∞) =
    HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) 1 + 1
have h : p.length (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) =
  p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ⋯
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have pos : (↑(p'.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  height x
Tactic: suffices p'.length ≤ height x by
      simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.coe_sub,
        Nat.cast_one, p'] at this
      convert! this
      norm_cast
      lia
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ⋯
⊢ (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have pos : p'.last (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) ≤
  x
Tactic: refine le_iSup₂_of_le p' ?_ le_rfl
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i) =
    (↑(↑i : ℕ) : ℕ∞)
have refine : ∀ (p_1 : LTSeries α),
  RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p_1 =
      p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i →
    LE.le (α := ℕ∞)
      (↑(p_1.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      (↑(↑i : ℕ) : ℕ∞)
Tactic: refine le_antisymm (height_le ?_) (index_le_height p i)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  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})
      i
⊢ LE.le (α := ℕ∞)
    (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(↑i : ℕ) : ℕ∞)
have hp'' : (↑((RelSeries.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p'
            (RelSeries.drop (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p i)
            sorry).length
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  height
    ((RelSeries.smash (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p'
          (RelSeries.drop (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p i)
          sorry).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
Tactic: have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  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})
      i
hp'' :
  (↑((RelSeries.smash (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p'
              (RelSeries.drop (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p i)
              ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      ((RelSeries.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p'
            (RelSeries.drop (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p i)
            ⋯).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
⊢ LE.le (α := ℕ∞)
    (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(↑i : ℕ) : ℕ∞)
have hp''₁ : (↑(p'.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) +
    HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) (↑(↑i : ℕ) : ℕ∞) ≤
  (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
Tactic: simp [← h] at hp''
Cleared hypotheses: hp''
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  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})
      i
hp'' :
  (↑(p'.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) +
      HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) (↑(↑i : ℕ) : ℕ∞) ≤
    (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
⊢ LE.le (α := ℕ∞)
    (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(↑i : ℕ) : ℕ∞)
have norm_cast : ∀
  (hp'' :
    p'.length (r := {x : α × α | x.1 < x.2}) + (p.length (r := {x : α × α | x.1 < x.2}) - (↑i : ℕ)) ≤
      p.length (r := {x : α × α | x.1 < x.2})),
  p'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    (↑i : ℕ)
Tactic: norm_cast at *
Cleared hypotheses: hp''
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a : α
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
have hne : Nonempty.{max 1 (u_1 + 1)}
  { p : LTSeries α //
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p =
      a }
Tactic: have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩