awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact
        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
-- 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}))
rw :
  ω0 ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * α' + R' =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R)
rw₁ :
  ω0 ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R) =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R)
rw₂ :
  ω0 ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R) =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R)
rw₃ rw₄ :
  ω0 ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R) =
    ω0 ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R)
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k.succ : Ordinal.{0}) * α' + R' =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R)

Tactic:
rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]

Premises used: Order.succ_eq_add_one, mul_assoc, Nat.cast_add_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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R) =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0})

Tactic:
?_
-- 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}))
rw :
  (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (α' + (↑m : Ordinal.{0})) =
    HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k.succ : Ordinal.{0}))
rw₁ :
  (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (α' + (↑m : Ordinal.{0})) =
    HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (↑k.succ : Ordinal.{0}) * (α' + (↑m : Ordinal.{0}))
rw₂ :
  (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (α' + (↑m : Ordinal.{0})) =
    (α' + (↑m : Ordinal.{0})) ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * (α' + (↑m : Ordinal.{0}))
rw₃ :
  HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0})) * (α' + (↑m : Ordinal.{0})) =
    (α' + (↑m : Ordinal.{0})) ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * (α' + (↑m : Ordinal.{0}))
rw₄ rw₅ :
  (α' + (↑m : Ordinal.{0})) ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * (α' + (↑m : Ordinal.{0})) =
    (α' + (↑m : Ordinal.{0})) ^ HAdd.hAdd (α := Ordinal.{0}) (↑k : Ordinal.{0}) 1 * (α' + (↑m : Ordinal.{0}))
⊢ (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0}) =
    HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k.succ : Ordinal.{0}))

Tactic:
rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]

Premises used: Order.succ_eq_add_one, And.right, mul_add, 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 : 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 :
  HPow.hPow (β := Ordinal.{0}) ω0 (Order.succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R) =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : 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:
calc
    (ω0 ^ (k.succ : Ordinal)) * α' + R'
    _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := by
        rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
    _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_
    _ = (α' + m) ^ succ (k.succ : Ordinal) := by
        rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]

Premises used: HMul.hMul, Order.succ, Nat.cast, HPow.hPow, HAdd.hAdd, 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 (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 :
  HPow.hPow (β := Ordinal.{0}) ω0 (Order.succ (↑k : Ordinal.{0})) * α' =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α'
succ₁ :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (Order.succ (↑k : Ordinal.{0})) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R) =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α' +
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0})

Tactic:
congr 1
-- 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}))
⊢ ω ∣ ω0

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

Premises used: Iff.mpr, Ordinal.omega0, Ordinal.opow_dvd_opow, Order.one_le_iff_ne_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 : 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}))
⊢ ω ∣ α'

Tactic:
have αd : ω ∣ α' :=
      dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
-- 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}))
αd : ω ∣ α'
rw : ¬α' = ⊥
⊢ ¬IsMin α'

Tactic:
rw [isMin_iff_eq_bot]

Premises used: isMin_iff_eq_bot
-- 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}))
αd : ω ∣ α'
⊢ ¬α' = ⊥

Tactic:
α0.ne'

Premises used: LT.lt.ne'
-- 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}))
αd : ω ∣ α'
⊢ ¬α' = ⊥

Tactic:
exact α0.ne'

Premises used: LT.lt.ne'
-- 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}))
αd : ω ∣ α'
⊢ ¬IsMin α'

Tactic:
have α0 : ¬IsMin α' := by
      rw [isMin_iff_eq_bot]
      exact α0.ne'
-- 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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
rw :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R +
      HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0}) =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α'

Tactic:
rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ,
      add_mul_of_isSuccLimit _ ⟨α0, isSuccPrelimit_iff_omega0_dvd.2 αd⟩, mul_assoc,
      @mul_omega0_dvd n (Nat.cast_pos'.2 n.pos) (natCast_lt_omega0 _) _ αd]

Premises used: Iff.mpr, add_assoc, mul_assoc, Nat.cast, Ordinal.natCast_lt_omega0, HPow.hPow, PNat.pos, Ordinal.isSuccPrelimit_iff_omega0_dvd, And.intro, Ordinal.add_mul_of_isSuccLimit, mul_add, Ordinal.opow_succ, Nat.cast_pos', Ordinal.mul_omega0_dvd
-- 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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
h₁ : HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
h₂ :
  ω ^ (a0.repr * succ (↑k : Ordinal.{0})) ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R +
      HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0}) =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})

Tactic:
apply @add_of_omega0_opow_le _ (repr a0 * succ ↑k)

Premises used: Ordinal.add_of_omega0_opow_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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
isPrincipal_add_omega0_opow _ ?_ Rl

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 : 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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
h₁ : HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
refine isPrincipal_add_omega0_opow _ ?_ Rl

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 : 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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
h₁ :
  HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr <
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))

Tactic:
rw [opow_mul, opow_succ]

Premises used: Ordinal.opow_mul, Ordinal.opow_succ