awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (k + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) k 0).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
zero :
  ∀ (ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0})),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (HAdd.hAdd (α := ℕ) 0 1) 0).repr;
    let R := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr;
    ∀
      (IH :
        (Ne (α := ℕ) 0 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑0 : Ordinal.{0}))) ∧
          HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * α' + R =
            HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑0 : Ordinal.{0})))
      (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
      (Rl : R < ω ^ (a0.repr * succ (↑0 : Ordinal.{0}))), R = 0
⊢ R = 0
have succ : ∀ (n_1 : ℕ) (ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0})),
  let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1 + 1) 0).repr;
  let R := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1) 0).repr;
  ∀
    (IH :
      (n_1 + 1 ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑(n_1 + 1) : Ordinal.{0}))) ∧
        HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * α' + R =
          HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑(n_1 + 1) : Ordinal.{0})))
    (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
    (Rl : R < ω ^ (a0.repr * succ (↑(n_1 + 1) : Ordinal.{0}))), R = 0
Tactic: cases k
Cleared hypotheses: k, ω00, R', R, IH, RR, Rl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (k + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) k 0).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑0 : Ordinal.{0}) + R =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑0 : Ordinal.{0})
have this : R = 0
Tactic: have : R = 0 := by cases k <;> simp [R, opowAux]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1)).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑(n_1 + 1) : Ordinal.{0}) + R =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑(n_1 + 1) : Ordinal.{0})
have succ : R + HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
Tactic: rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1)).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ R + HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
have succ : ω ^ (a0.repr * succ (↑k : Ordinal.{0})) ≤ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
Tactic: apply add_of_omega0_opow_le Rl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1)).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ ω ^ (a0.repr * succ (↑k : Ordinal.{0})) ≤ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
have succ : HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr ≤
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
Tactic: rw [opow_mul, opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1)).repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
have succ : ω ^ a0.repr ≤ α'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have rcases : ∀ (a : ONote) (m : ℕ) (e₁ : o₁.split = (a, m)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: rcases e₁ : split o₁ with ⟨a, m⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have N₁ : a.NF
Tactic: obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
N₁ : a.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have r₁ : o₁.repr = a.repr + (↑m : Ordinal.{0})
Tactic: obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
N₁ : a.NF
r₁ : o₁.repr = a.repr + (↑m : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have zero : ∀ (e₁ : o₁.split = (zero, m)) (N₁ : zero.NF) (r₁ : o₁.repr = zero.repr + (↑m : Ordinal.{0})),
  (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: obtain - | ⟨a0, n, a'⟩ := a
Cleared hypotheses: a, e₁, N₁, r₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
N₁ : a.NF
r₁ : o₁.repr = a.repr + (↑m : Ordinal.{0})
zero :
  ∀ (e₁ : o₁.split = (ONote.zero, m)) (N₁ : ONote.zero.NF) (r₁ : o₁.repr = ONote.zero.repr + (↑m : Ordinal.{0})),
    (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have oadd : ∀ (a0 : ONote) (n : ℕ+) (a' : ONote) (e₁ : o₁.split = (a0.oadd n a', m)) (N₁ : (a0.oadd n a').NF)
  (r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: obtain - | ⟨a0, n, a'⟩ := a
Cleared hypotheses: a, e₁, N₁, r₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
e₁ : o₁.split = (zero, m)
N₁ : zero.NF
r₁ : o₁.repr = zero.repr + (↑m : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have zero : ∀ (e₁ : o₁.split = (zero, 0)) (r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: rcases m with - | m
Cleared hypotheses: m, e₁, r₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
e₁ : o₁.split = (ONote.zero, m)
N₁ : ONote.zero.NF
r₁ : o₁.repr = ONote.zero.repr + (↑m : Ordinal.{0})
zero :
  ∀ (e₁ : o₁.split = (ONote.zero, 0)) (r₁ : o₁.repr = ONote.zero.repr + (↑0 : Ordinal.{0})),
    (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have zero₁ : ∀ (m : ℕ) (e₁ : o₁.split = (ONote.zero, m + 1)) (r₁ : o₁.repr = ONote.zero.repr + (↑(m + 1) : Ordinal.{0})),
  (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: rcases m with - | m
Cleared hypotheses: m, e₁, r₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have pos : ∀ (h : o₂ = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: by_cases h : o₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})
pos : ∀ (h : o₂ = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have neg : ∀ (h : ¬o₂ = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: by_cases h : o₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have zero : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: rcases e₂ : split' o₂ with ⟨b', k⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have left : b'.NF
Tactic: obtain ⟨_, r₂⟩ := nf_repr_split' e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
Tactic: obtain ⟨_, r₂⟩ := nf_repr_split' e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have pos : ∀ (h : m = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
pos : ∀ (h : m = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have neg : ∀ (h : ¬m = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have neg : ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
  HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))
Tactic: simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add,
          add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))
have neg : ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
  ω ^ b'.repr * HPow.hPow (β := Ordinal.{0}) (HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1) (↑k : Ordinal.{0})
Tactic: rw [opow_add, opow_mul, opow_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
neg :
  ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    ω ^ b'.repr * HPow.hPow (β := Ordinal.{0}) (HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1) (↑k : Ordinal.{0})
⊢ ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))
have neg₁ : 1 < HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1
Tactic: rw [opow_add, opow_mul, opow_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
neg :
  ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    ω ^ b'.repr * HPow.hPow (β := Ordinal.{0}) (HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1) (↑k : Ordinal.{0})
neg₁ : 1 < HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1
⊢ ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))
have neg₂ : HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 < ω
Tactic: rw [opow_add, opow_mul, opow_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 < ω
have neg : ∃ (n : ℕ), Eq (α := Ordinal.{0}) (↑m.succ : Ordinal.{0}) (↑n : Ordinal.{0})
Tactic: rw [← Nat.cast_succ, lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have this : a0.NF
Tactic: haveI := N₁.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this : a0.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have this₁ : a'.NF
Tactic: haveI := N₁.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have a00 : a0.repr ≠ 0
Tactic: obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have ad : ω ∣ a'.repr
Tactic: obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
Tactic: have al := split_add_lt e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
Tactic: have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have oadd : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Tactic: rcases e₂ : split' o₂ with ⟨b', k⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have left : b'.NF
Tactic: obtain ⟨_, r₂⟩ := nf_repr_split' e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
Tactic: obtain ⟨_, r₂⟩ := nf_repr_split' e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
have oadd : repr
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
  (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
Tactic: simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]