awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n_1 : ℕ
e₂ : o₂.split' = (b', n_1 + 1 + 1)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd : ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
Tactic: cases m
Cleared hypotheses: m, e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n_1 : ℕ
e₂ : o₂.split' = (b', n_1 + 1 + 1)
oadd :
  ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd₁ : ∀ (n_2 : ℕ) (e₁ : o₁.split = (a0.oadd n a', n_2 + 1)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
        (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_2 + 1) : ONote)) k (n_2 + 1))
Tactic: cases m
Cleared hypotheses: m, e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m : ℕ
⊢ (e.opowAux a0 a 0 m).repr = ω ^ e.repr * (opowAux 0 a0 a 0 m).repr
have zero : (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m : ℕ
zero : (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr
⊢ (e.opowAux a0 a 0 m).repr = ω ^ e.repr * (opowAux 0 a0 a 0 m).repr
have succ : ∀ (n : ℕ), (e.opowAux a0 a 0 (n + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n + 1)).repr
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
have pos : ∀ (h : m = 0), (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
pos : ∀ (h : m = 0), (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
have neg : ∀ (h : ¬m = 0), (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
a' : Ordinal.{0}
e0 : e.repr ≠ 0
h : a' < ω ^ e.repr
aa : a.repr = a'
n : ℕ+
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a') ^ ω = (ω ^ e.repr) ^ ω
have subst : ∀ (h : a.repr < ω ^ e.repr), (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
Tactic: subst aa
Cleared hypotheses: a', h, aa
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
have No : (e.oadd n a).NF
Tactic: have No := Ne.oadd n (Na.below_of_lt' h)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
have this : ω ^ e.repr ≤ (e.oadd n a).repr
Tactic: have := omega0_le_oadd e n a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ (e.oadd n a).repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
have this₁ : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
Tactic: rw [repr] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
have refine : (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω ≤ (ω ^ e.repr) ^ ω
Tactic: refine le_antisymm ?_ (opow_le_opow_left _ this)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω ≤ (ω ^ e.repr) ^ ω
have apply : ∀ b' < ω, (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b' ≤ (ω ^ e.repr) ^ ω
Tactic: apply (opow_le_of_isSuccLimit ((opow_pos _ omega0_pos).trans_le this).ne' isSuccLimit_omega0).2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
have this₁ : (e.oadd n a).repr < ω ^ succ e.repr
Tactic: have := (No.below_of_lt (lt_succ _)).repr_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : (e.oadd n a).repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
have this₁ : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
Tactic: rw [repr] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
have apply : (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω
Tactic: apply (opow_le_opow_left b <| this.le).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
⊢ (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω
have rw : ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
Tactic: rw [← opow_mul, ← opow_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have inl : ∀ (h : ω ≤ e.repr), ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
Tactic: rcases le_or_gt ω (repr e) with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
inl : ∀ (h : ω ≤ e.repr), ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have inr : ∀ (h : e.repr < ω), ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
Tactic: rcases le_or_gt ω (repr e) with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have inl : ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)
Tactic: grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
inl : ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have h₁ : 0 < ω
Tactic: grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)
have inl : 0 < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
inl : 0 < ω
⊢ ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)
have inl₁ : e.repr * succ b + 1 ≤ e.repr * ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ e.repr * succ b < e.repr * ω
have hbc : succ b < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have inr : ω ^ ω ≤ ω ^ (e.repr * ω)
Tactic: grw [show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : e.repr < ω
inr : ω ^ ω ≤ ω ^ (e.repr * ω)
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
have h₁ : 0 < ω
Tactic: grw [show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
⊢ (k ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑k : Ordinal.{0}))
have No : (a0.oadd n a').NF
Tactic: haveI No : NF (oadd a0 n a') :=
    N0.oadd n (Na'.below_of_lt' <| lt_of_le_of_lt le_self_add h)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr
⊢ (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑0 : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑0 : Ordinal.{0}))
have zero : ∀ (h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr),
  let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr;
  (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑0 : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑0 : Ordinal.{0}))
        (succ (↑0 : Ordinal.{0}))
Tactic: cases m
Cleared hypotheses: m, h, R'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr
zero :
  ∀ (h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr;
    (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑0 : Ordinal.{0}))) ∧
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
            (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
          R' =
        HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑0 : Ordinal.{0}))
          (succ (↑0 : Ordinal.{0}))
⊢ (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑0 : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑0 : Ordinal.{0}))
have zero₁ : ∀ (n_1 : ℕ) (h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr),
  let R' := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) 0 (n_1 + 1)).repr;
  (Ne (α := ℕ) 0 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑0 : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑0 : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑(n_1 + 1) : Ordinal.{0}))
        (succ (↑0 : Ordinal.{0}))
Tactic: cases m
Cleared hypotheses: m, h, R'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
⊢ R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
have pos : ∀ (h : m = 0), R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
pos : ∀ (h : m = 0), R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
⊢ R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
have neg : ∀ (h : ¬m = 0), R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
⊢ (k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑(k + 1) : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑(k + 1) : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑(k + 1) : Ordinal.{0}))
have RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
Tactic: have RR : R' = ω0 ^ (k : Ordinal) * (α' * m) + R := by
    by_cases h : m = 0
    · simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr, mul_zero,
        ONote.opowAux, add_zero]
    · simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux,
        ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
⊢ (k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑(k + 1) : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑(k + 1) : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑(k + 1) : Ordinal.{0}))
have α0 : 0 < α'
Tactic: have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
α0 : 0 < α'
⊢ (k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑(k + 1) : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑(k + 1) : Ordinal.{0}) *
          (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        R' =
      HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
        (succ (↑(k + 1) : Ordinal.{0}))
have ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Tactic: have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.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}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
⊢ R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
have pos : ∀ (k0 : k = 0), R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
Tactic: by_cases k0 : k = 0