awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 b < ω

Tactic:
isSuccLimit_omega0.succ_lt l

Premises used: Ordinal.isSuccLimit_omega0, Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 b < ω

Tactic:
exact isSuccLimit_omega0.succ_lt l

Premises used: Ordinal.isSuccLimit_omega0, Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * ω

Tactic:
exact succ_le_iff.2 <| by gcongr; exact isSuccLimit_omega0.succ_lt l

Premises used: Iff.mpr, Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * ω)
h₁ : 0 < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
grw [show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l]

Premises used: Ordinal.isSuccLimit_omega0, Ordinal.isPrincipal_mul_omega0, Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * ω)

Tactic:
simpa using mul_le_mul_left (one_le_iff_ne_zero.2 e0) ω

Premises used: Iff.mpr, Ordinal.omega0, Order.one_le_iff_ne_zero, mul_le_mul_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < ω
⊢ 0 < ω

Tactic:
omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < ω
⊢ 0 < ω

Tactic:
exact omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ (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)
-- Module: Mathlib.SetTheory.Ordinal.Notation
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}))
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}))
⊢ (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}))

Tactic:
cases m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (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:
simp [R', opowAux]

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
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)) 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:
simp [R', opowAux]

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 : ℕ
IH :
  let R' := (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}))
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
⊢ (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}))

Tactic:
change (k ≠ 0 → R < (ω0 ^ succ (k : Ordinal))) ∧ (ω0 ^ (k : Ordinal)) * α' + R
    = (α' + m) ^ (succ ↑k : Ordinal) at IH

Premises used: Order.succ, Nat.cast, HPow.hPow, HAdd.hAdd
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
neg : ∀ (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

Tactic:
by_cases h : m = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h_1 : 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}))
h : m = 0
⊢ R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R

Tactic:
simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr, mul_zero,
        ONote.opowAux, add_zero]

Premises used: ONote.ofNat, MulZeroClass.mul_zero, ONote.repr, Nat.cast_zero, ONote.opowAux, add_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h_1 : 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}))
h : ¬m = 0
⊢ R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R

Tactic:
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]

Premises used: Ordinal.opow_mul, ONote.zero_add, ONote.repr_mul, ONote.repr_add, ONote.repr_scale, ONote.mulNat_eq_mul, ONote.repr, ONote.repr_ofNat, ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
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

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]
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < α'

Tactic:
simpa [lt_def, repr] using oadd_pos a0 n a'

Premises used: ONote.lt_def, ONote.repr, ONote.oadd_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < α'

Tactic:
have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 < α'
⊢ 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})

Tactic:
have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
pos : ∀ (k0 : k = 0), R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
neg : ∀ (k0 : ¬k = 0), R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
by_cases k0 : k = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
k0 : k = 0
pos : (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr < ω ^ a0.repr
⊢ R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
simp only [k0, Nat.cast_zero, succ_eq_add_one, _root_.zero_add, mul_one, R]

Premises used: Order.succ_eq_add_one, zero_add, Nat.cast_zero, mul_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
k0 : k = 0
⊢ (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr < ω ^ a0.repr

Tactic:
lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, Ordinal.omega0_pos, Order.one_le_iff_ne_zero, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
k0 : k = 0
pos : (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr < HPow.hPow (β := Ordinal.{0}) ω 1
⊢ (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr < ω ^ a0.repr

Tactic:
refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, Ordinal.omega0_pos, Order.one_le_iff_ne_zero, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
k0 : k = 0
pos :
  ∀ (h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (k + 1) 0).repr;
    let R := (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),
      (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr < HPow.hPow (β := Ordinal.{0}) ω 1
pos₁ :
  ∀ (m : ℕ) (h : a'.repr + (↑(m + 1) : Ordinal.{0}) < ω ^ a0.repr),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑(m + 1) : ONote)) (k + 1) (m + 1)).repr;
    let R := (opowAux 0 a0 (a0.oadd n a' * (↑(m + 1) : ONote)) k (m + 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}) (α' + (↑(m + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0})))
      (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(m + 1) : Ordinal.{0})) + R),
      (opowAux 0 a0 (a0.oadd n a' * (↑(m + 1) : ONote)) 0 (m + 1)).repr < HPow.hPow (β := Ordinal.{0}) ω 1
⊢ (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) 0 m).repr < HPow.hPow (β := Ordinal.{0}) ω 1

Tactic:
rcases m with - | m
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})
k0 : k = 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
⊢ (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr < HPow.hPow (β := Ordinal.{0}) ω 1

Tactic:
simp [opowAux, omega0_pos]

Premises used: Ordinal.omega0_pos, ONote.opowAux