awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd : ∀ (he : e.cmp e' = Ordering.lt),
  repr
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: cases he : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
oadd :
  ∀ (he : e.cmp e' = Ordering.lt),
    repr
        (match (motive := Ordering → ONote) Ordering.lt with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd₁ : ∀ (he : e.cmp e' = Ordering.eq),
  repr
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: cases he : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
oadd :
  ∀ (he : e.cmp e' = Ordering.lt),
    repr
        (match (motive := Ordering → ONote) Ordering.lt with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
oadd₁ :
  ∀ (he : e.cmp e' = Ordering.eq),
    repr
        (match (motive := Ordering → ONote) Ordering.eq with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd₂ : ∀ (he : e.cmp e' = Ordering.gt),
  repr
      (match (motive := Ordering → ONote) Ordering.gt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: cases he : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.lt
⊢ repr
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have ee₁ : e < e'
Tactic: simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢
Cleared hypotheses: ee
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.eq
⊢ repr
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd : ∀ (ee : e = e'),
  ω ^ e.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢
Cleared hypotheses: ee
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
Tactic: rw [← add_assoc, @add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
oadd : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
⊢ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd₁ : ω ^ e'.repr ≤ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0})
Tactic: rw [← add_assoc, @add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
have this₁ : (e.oadd n a).repr < ω ^ e'.repr
Tactic: have := (h₁.below_of_lt ee).repr_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this : (e.oadd n a).repr < ω ^ e'.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
have this₁ : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
  HPow.hPow (β := Ordinal.{0}) ω
    (match (motive := ONote → Ordinal.{0}) e' with
      | zero => 0
      | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
      Ordinal.{0})
Tactic: unfold repr at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
have oadd : ∀ (he' : e' = zero), ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ zero.repr
Tactic: cases he' : e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
oadd : ∀ (he' : e' = zero), ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ zero.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
have oadd₁ : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (he' : e' = a.oadd a_1 a_2),
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ (a.oadd a_1 a_2).repr
Tactic: cases he' : e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
he' : e' = zero
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ zero.repr
have oadd : ∀ (this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < 1), ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < 1
Tactic: simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
a_1 : ONote
a_2 : ℕ+
a_3 : ONote
he' : e' = a_1.oadd a_2 a_3
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ (a_1.oadd a_2 a_3).repr
have this₁ : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ (ω ^ a_1.repr * (↑(↑a_2 : ℕ) : Ordinal.{0}) + a_3.repr)
Tactic: simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd : ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
  ω ^ e'.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: rw [ee, ← add_assoc, ← mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
oadd :
  ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e'.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ ω ^ e.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd₁ : ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
  ω ^ e'.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr
Tactic: rw [ee, ← add_assoc, ← mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
oadd :
  ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e'.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
oadd₁ :
  ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e'.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr
⊢ ω ^ e.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have oadd₂ : ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
  ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr
Tactic: rw [ee, ← add_assoc, ← mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
h : NFBelow 0 b
h₂ : o.NF
⊢ (0 - o).NFBelow b
have zero : ∀ (h₂ : zero.NF), (0 - zero).NFBelow b
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
h : NFBelow 0 b
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 - ONote.zero).NFBelow b
⊢ (0 - o).NFBelow b
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (h₂ : (a.oadd a_1 a_2).NF), (0 - a.oadd a_1 a_2).NFBelow b
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b
have h' : (a₁ - a₂).NFBelow e₁.repr
Tactic: have h' := sub_nfBelow h₁.snd h₂.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁ - a₂).NFBelow e₁.repr
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b
have simp : NFBelow
  (match (motive := Ordering → ONote) e₁.cmp e₂ with
  | Ordering.lt => 0
  | Ordering.gt => e₁.oadd n₁ a₁
  | Ordering.eq =>
    match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
    | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
    | k.succ => e₁.oadd k.succPNat a₁)
  b
Tactic: simp only [HSub.hSub, Sub.sub, sub] at h' ⊢
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
⊢ NFBelow
    (match (motive := Ordering → ONote) e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have this : (e₁.cmp e₂).Compares e₁ e₂
Tactic: have := @cmp_compares _ _ h₁.fst h₂.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
⊢ NFBelow
    (match (motive := Ordering → ONote) e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have lt : ∀ (h : e₁.cmp e₂ = Ordering.lt),
  NFBelow
    (match (motive := Ordering → ONote) Ordering.lt with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
Tactic: cases h : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
lt :
  ∀ (h : e₁.cmp e₂ = Ordering.lt),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
⊢ NFBelow
    (match (motive := Ordering → ONote) e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have eq : ∀ (h : e₁.cmp e₂ = Ordering.eq),
  NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
Tactic: cases h : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
lt :
  ∀ (h : e₁.cmp e₂ = Ordering.lt),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
eq :
  ∀ (h : e₁.cmp e₂ = Ordering.eq),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
⊢ NFBelow
    (match (motive := Ordering → ONote) e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have gt : ∀ (h : e₁.cmp e₂ = Ordering.gt),
  NFBelow
    (match (motive := Ordering → ONote) Ordering.gt with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
Tactic: cases h : cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.eq
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have eq : NFBelow
  (match (motive := Ordering → ONote) Ordering.eq with
  | Ordering.lt => 0
  | Ordering.gt => e₁.oadd n₁ a₁
  | Ordering.eq =>
    match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
    | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
    | k.succ => e₁.oadd k.succPNat a₁)
  b
Tactic: rw [Nat.sub_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.eq
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have this₁ : e₁ = e₂
Tactic: simp only [h, Ordering.compares_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
h : e₁.cmp e₂ = Ordering.eq
this : e₁ = e₂
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have h₃ : (e₁.oadd n₂ a₂).NF
Tactic: subst e₂
Cleared hypotheses: e₂, h₂, h, this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
h : e₁.cmp e₂ = Ordering.eq
this : e₁ = e₂
h₃ : (e₁.oadd n₂ a₂).NF
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
have h₄ : e₁.cmp e₁ = Ordering.eq
Tactic: subst e₂
Cleared hypotheses: e₂, h₂, h, this