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 : 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₁ : a'.repr < ω ^ a0.repr
⊢ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * a'.repr <
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr

Tactic:
gcongr
-- 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 α'
⊢ a'.repr < ω ^ a0.repr

Tactic:
No.snd'.repr_lt

Premises used: ONote.NF.snd', ONote.NFBelow.repr_lt
-- 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 α'
⊢ a'.repr < ω ^ a0.repr

Tactic:
exact No.snd'.repr_lt

Premises used: ONote.NF.snd', ONote.NFBelow.repr_lt
-- 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 (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))
-- 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 α'
this :
  HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * 1 ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})
h₂ :
  HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0})) ≤
    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})

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_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})
⊢ HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (succ (↑k : Ordinal.{0})) ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑k : Ordinal.{0})) * (↑(↑n : ℕ) : Ordinal.{0})

Tactic:
simpa
-- 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 :
  ∀ (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})
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})
⊢ 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:
cases m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
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 (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}))
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 (Order.succ (↑0 : Ordinal.{0}))) ∧
          HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * α' + R =
            HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (Order.succ (↑0 : Ordinal.{0})))
      (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
      (Rl : R < ω ^ (a0.repr * Order.succ (↑0 : Ordinal.{0}))), R = 0
succ :
  ∀ (n_1 : ℕ) (ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0})),
    let R' := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1 + 1) 0).repr;
    let R := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1) 0).repr;
    ∀
      (IH :
        (n_1 + 1 ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (Order.succ (↑(n_1 + 1) : Ordinal.{0}))) ∧
          HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * α' + R =
            HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (Order.succ (↑(n_1 + 1) : Ordinal.{0})))
      (RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R)
      (Rl : R < ω ^ (a0.repr * Order.succ (↑(n_1 + 1) : Ordinal.{0}))), R = 0
⊢ R = 0

Tactic:
cases k
-- 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
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑0 : Ordinal.{0})
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (HAdd.hAdd (α := ℕ) 0 1) 0).repr
R : Ordinal.{0} := (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:
simp [R, opowAux]

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr
α0 : 0 < α'
h : a'.repr + (↑0 : Ordinal.{0}) < ω ^ a0.repr
n_1 : ℕ
ω00 : 0 < HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0})
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑0 : ONote)) (n_1 + 1) 0).repr
IH :
  (n_1 + 1 ≠ 0 → R < HPow.hPow (β := Ordinal.{0}) ω0 (succ (↑(n_1 + 1) : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑0 : Ordinal.{0})) (succ (↑(n_1 + 1) : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑(n_1 + 1) : Ordinal.{0}) * (α' * (↑0 : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑(n_1 + 1) : Ordinal.{0}))
⊢ R = 0

Tactic:
simp [R, opowAux]

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

Tactic:
have : R = 0 := by cases k <;> simp [R, opowAux]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
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}))
this : R = 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:
simp [this]
-- 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})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (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}))
succ :
  R + HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' = HPow.hPow (β := Ordinal.{0}) ω0 (↑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:
rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]

Premises used: Order.succ_eq_add_one, Ordinal.add_mul_succ, Nat.cast_add_one
-- 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})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (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}))
succ : ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0})) ≤ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
⊢ R + HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'

Tactic:
apply add_of_omega0_opow_le Rl

Premises used: Ordinal.add_of_omega0_opow_le
-- 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})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (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}))
succ :
  HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'
⊢ ω ^ (a0.repr * Order.succ (↑k : Ordinal.{0})) ≤ HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'

Tactic:
rw [opow_mul, opow_succ]

Premises used: Ordinal.opow_mul, Ordinal.opow_succ
-- 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})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (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}))
succ : ω ^ a0.repr ≤ α'
⊢ HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * ω ^ a0.repr ≤
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α'

Tactic:
gcongr
-- 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})
n_1 : ℕ
h : a'.repr + (↑(n_1 + 1) : Ordinal.{0}) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) (k + 1) (n_1 + 1)).repr
R : Ordinal.{0} := (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 (succ (↑k : Ordinal.{0}))) ∧
    HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * α' + R =
      HPow.hPow (β := Ordinal.{0}) (α' + (↑(n_1 + 1) : Ordinal.{0})) (succ (↑k : Ordinal.{0}))
RR : R' = HPow.hPow (β := Ordinal.{0}) ω0 (↑k : Ordinal.{0}) * (α' * (↑(n_1 + 1) : Ordinal.{0})) + R
Rl : R < ω ^ (a0.repr * succ (↑k : Ordinal.{0}))
⊢ ω ^ a0.repr ≤ α'

Tactic:
simpa [repr] using omega0_le_oadd a0 n a'

Premises used: ONote.omega0_le_oadd, ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
rcases : ∀ (a : ONote) (m : ℕ) (e₁ : o₁.split = (a, m)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
rcases e₁ : split o₁ with ⟨a, m⟩

Premises used: ONote.split
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
⊢ a.NF

Tactic:
obtain ⟨N₁, r₁⟩ := nf_repr_split e₁

Premises used: ONote.nf_repr_split
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
N₁ : a.NF
⊢ o₁.repr = a.repr + (↑m : Ordinal.{0})

Tactic:
obtain ⟨N₁, r₁⟩ := nf_repr_split e₁

Premises used: ONote.nf_repr_split
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
N₁ : a.NF
r₁ : o₁.repr = a.repr + (↑m : Ordinal.{0})
zero :
  ∀ (e₁ : o₁.split = (ONote.zero, m)) (N₁ : ONote.zero.NF) (r₁ : o₁.repr = ONote.zero.repr + (↑m : Ordinal.{0})),
    (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
oadd :
  ∀ (a0 : ONote) (n : ℕ+) (a' : ONote) (e₁ : o₁.split = (a0.oadd n a', m)) (N₁ : (a0.oadd n a').NF)
    (r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
obtain - | ⟨a0, n, a'⟩ := a