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 : 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) * α'
⊢ 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})
have 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})
Tactic: congr 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
α0 : 0 < α'
ω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}) * α' + R) * α'
have αd : ω ∣ α'
Tactic: have αd : ω ∣ α' :=
      dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
-- 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}))
αd : ω ∣ α'
⊢ ¬IsMin α'
have rw : ¬α' = ⊥
Tactic: rw [isMin_iff_eq_bot]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
α0 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * α' =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α'
have α0₁ : ¬IsMin α'
Tactic: have α0 : ¬IsMin α' := by
      rw [isMin_iff_eq_bot]
      exact α0.ne'
-- 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_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 (succ (↑k : Ordinal.{0})) * α' =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * α'
have 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})
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]
-- 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_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 +
      HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0}) =
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
have h₁ : HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr + R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
Tactic: apply @add_of_omega0_opow_le _ (repr a0 * succ ↑k)
-- 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_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}))
⊢ 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})
have h₂ : ω ^ (a0.repr * succ (↑k : 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)
-- 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_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}))
have h₁ : HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
Tactic: refine isPrincipal_add_omega0_opow _ ?_ Rl
-- 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_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 < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
have h₁ : HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr <
  HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr
Tactic: rw [opow_mul, opow_succ]
-- 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_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 <
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr
have h₁ : a'.repr < ω ^ a0.repr
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
IH :
  (k ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑m : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑m : Ordinal.{0})) + R
α0_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ ω ^ (a0.repr * succ (↑k : Ordinal.{0})) ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
have this : HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * 1 ≤
  HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
Tactic: have := mul_le_mul_right (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))
-- 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_1 : 0 < α'
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0})
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
αd : ω ∣ α'
α0 : ¬IsMin α'
this :
  HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * 1 ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
⊢ ω ^ (a0.repr * succ (↑k : Ordinal.{0})) ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
have h₂ : HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0})) ≤
  HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
Tactic: rw [opow_mul]
-- 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}) * α' * (↑m : Ordinal.{0}) + R =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0})
have succ : ∀ (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)
    (Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))),
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑0 : Ordinal.{0}) + R =
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑0 : Ordinal.{0})
Tactic: cases m
Cleared hypotheses: m, h, R', R, IH, RR, Rl
-- 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 (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 :
  ∀ (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 (Order.succ (↑k : Ordinal.{0}))) ∧
          HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
            HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (Order.succ (↑k : Ordinal.{0})))
      (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
      (Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))),
      HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑0 : Ordinal.{0}) + R =
        (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑0 : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑m : Ordinal.{0}) + R =
    (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑m : Ordinal.{0})
have succ₁ : ∀ (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)) (k + 1) (n_1 + 1)).repr;
  let R := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1)).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}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (Order.succ (↑k : Ordinal.{0})))
    (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R)
    (Rl : R < ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0}))),
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' * (↑(n_1 + 1) : Ordinal.{0}) + R =
      (HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R) * (↑(n_1 + 1) : Ordinal.{0})
Tactic: cases m
Cleared hypotheses: m, h, R', R, IH, RR, Rl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
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
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ R = 0
have zero : ∀ (ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0})),
  let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (HAdd.hAdd (α := ℕ) 0 1) 0).repr;
  let R := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) 0 0).repr;
  ∀
    (IH :
      (Ne (α := ℕ) 0 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑0 : Ordinal.{0}))) ∧
        HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * α' + R =
          HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑0 : Ordinal.{0})))
    (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
    (Rl : R < ω ^ (a0.repr * succ (↑0 : Ordinal.{0}))), R = 0
Tactic: cases k
Cleared hypotheses: k, ω00, R', R, IH, RR, Rl