awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
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
⊢ α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)
have succ : ∀ (this : (a0.oadd n a').repr < ω ^ (a0.repr + a0.repr)), α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)
Tactic: have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
-- 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_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)
⊢ α' * (↑m : Ordinal.{0}) < ω ^ (a0.repr + a0.repr)
have succ₁ : a0.repr < a0.repr + a0.repr
Tactic: have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
-- 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})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ 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)
have 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)
Tactic: rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
-- 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})
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)
⊢ 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)
have 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)
Tactic: rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
-- 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})
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)
⊢ 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)
have 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)
Tactic: rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
-- 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})
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)
⊢ 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)
have 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)
Tactic: rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one]
-- 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})
Rl : R < ω ^ (a0.repr * succ (↑k : 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}))
have 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}))
Tactic: rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
-- 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})
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}))
⊢ (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}))
have 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}))
Tactic: rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
-- 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})
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}))
⊢ (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}))
have 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}))
Tactic: rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
-- 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})
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}))
⊢ (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}))
have 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}))
Tactic: rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
-- 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})
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}))
⊢ (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}))
have 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}))
Tactic: rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]
-- 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})
Rl : R < ω ^ (a0.repr * succ (↑k : 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 succ : 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: 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]
-- 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})
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})
have succ : HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' =
  (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α'
Tactic: congr 1