awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : ℕ
h : a'.repr + (↑(m + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(m + 1) : ONote)) (k + 1) (m + 1)).repr
R : Ordinal.{0} := (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

Tactic:
simpa [opowAux] using natCast_lt_omega0 (m + 1)

Premises used: Ordinal.natCast_lt_omega0, HAdd.hAdd, ONote.opowAux, OfNat.ofNat
-- 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
neg : R < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0}))
⊢ R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
rw [opow_mul]

Premises used: Ordinal.opow_mul
-- 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
⊢ R < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0}))

Tactic:
IH.1 k0

Premises used: And.left
-- 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
⊢ R < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0}))

Tactic:
exact IH.1 k0

Premises used: And.left
-- 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})
⊢ R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
have Rl : R < ω ^ (repr a0 * succ ↑k) := by
    by_cases k0 : k = 0
    · simp only [k0, Nat.cast_zero, succ_eq_add_one, _root_.zero_add, mul_one, R]
      refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))
      rcases m with - | m
      · simp [opowAux, omega0_pos]
      · simpa [opowAux] using natCast_lt_omega0 (m + 1)
    · rw [opow_mul]
      exact IH.1 k0
-- 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})
Rl : R < ω ^ (a0.repr * 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}))

Tactic:
⟨fun _ => ?_, ?_⟩

Premises used: And.intro
-- 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
succ : k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑(k + 1) : Ordinal.{0}))
succ₁ :
  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}))
      (Order.succ (↑(k + 1) : Ordinal.{0}))
⊢ (k + 1 ≠ 0 → R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.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}))
        (Order.succ (↑(k + 1) : Ordinal.{0}))

Tactic:
refine ⟨fun _ => ?_, ?_⟩
-- 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
succ :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R <
    ω ^ (a0.repr * Order.succ (↑k.succ : Ordinal.{0}))
⊢ R' < HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (Order.succ (↑(k + 1) : Ordinal.{0}))

Tactic:
rw [RR, ← opow_mul _ _ (succ k.succ)]

Premises used: Ordinal.opow_mul, Order.succ, Nat.cast, Nat.succ
-- 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
⊢ 0 < a0.repr

Tactic:
have e0 := pos_iff_ne_zero.2 e0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
⊢ 0 < a0.repr + a0.repr

Tactic:
have rr0 : 0 < repr a0 + repr a0 := lt_of_lt_of_le e0 le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
succ :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) <
    ω ^ (a0.repr * Order.succ (↑k.succ : Ordinal.{0}))
succ₁ : R < ω ^ (a0.repr * Order.succ (↑k.succ : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R <
    ω ^ (a0.repr * Order.succ (↑k.succ : Ordinal.{0}))

Tactic:
apply isPrincipal_add_omega0_opow

Premises used: Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
succ :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) <
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * (ω ^ a0.repr * ω ^ a0.repr)
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) <
    ω ^ (a0.repr * Order.succ (↑k.succ : Ordinal.{0}))

Tactic:
simp only [Nat.cast_add_one, opow_add_one, opow_mul, opow_succ, mul_assoc]

Premises used: Ordinal.opow_mul, mul_assoc, Ordinal.opow_add_one, Ordinal.opow_succ, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
succ : α' * (↑m : Ordinal.{0}) < ω ^ a0.repr * ω ^ a0.repr
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) <
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * (ω ^ a0.repr * ω ^ a0.repr)

Tactic:
gcongr ?_ * ?_
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
succ : α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)
⊢ α' * (↑m : Ordinal.{0}) < ω ^ a0.repr * ω ^ a0.repr

Tactic:
rw [← Ordinal.opow_add]

Premises used: Ordinal.opow_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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 (Order.succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (Order.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})
Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
succ : ∀ (this : (a0.oadd n a').repr < ω ^ (a0.repr + a0.repr)), α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)
succ₁ : a0.repr < a0.repr + a0.repr
⊢ α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)

Tactic:
have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
this : (a0.oadd n a').repr < ω ^ (a0.repr + a0.repr)
⊢ α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)

Tactic:
mul_lt_omega0_opow rr0 this (natCast_lt_omega0 _)

Premises used: Ordinal.mul_lt_omega0_opow, Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
this : (a0.oadd n a').repr < ω ^ (a0.repr + a0.repr)
⊢ α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)

Tactic:
exact mul_lt_omega0_opow rr0 this (natCast_lt_omega0 _)

Premises used: Ordinal.mul_lt_omega0_opow, Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ a0.repr < a0.repr + a0.repr

Tactic:
simpa using (add_lt_add_iff_left (repr a0)).2 e0

Premises used: Iff.mpr, ONote.repr, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0_1 : 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h_1 : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ R < ω ^ (a0.repr * succ (↑k.succ : Ordinal.{0}))

Tactic:
lt_of_lt_of_le Rl
          (opow_le_opow_right omega0_pos <|
            mul_le_mul_right (succ_le_succ_iff.2 (Nat.cast_le.2 (le_of_lt k.lt_succ_self))) _)

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, Ordinal.omega0_pos, le_of_lt, mul_le_mul_right, Nat.lt_succ_self, Order.succ_le_succ_iff, Nat.cast_le, lt_of_lt_of_le