awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
zero :
  NF
    (match (motive := ℕ → ℕ → ONote) k, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
succ :
  ∀ (m : ℕ),
    NF
      (match (motive := ℕ → ℕ → ONote) k, m + 1 with
      | x, 0 => 0
      | 0, m.succ => e.oadd m.succPNat 0
      | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
⊢ NF
    (match (motive := ℕ → ℕ → ONote) k, m with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
cases m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      haveI := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

Premises used: Order.succ, ONote.zero, ONote.NF.oadd_zero, ONote.mulNat_eq_mul, ONote.NF.zero
-- 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₂).NF
⊢ (o₁ ^ o₂).NF

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:
have na := (nf_repr_split e₁).1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
rcases : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF

Tactic:
rcases e₂ : split' o₂ with ⟨b', k⟩

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)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ b'.NF

Tactic:
haveI := (nf_repr_split' e₂).1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
zero : ∀ (e₁ : o₁.split = (ONote.zero, m)) (na : ONote.zero.NF), (o₁ ^ o₂).NF
oadd : ∀ (a0 : ONote) (n : ℕ+) (a' : ONote) (e₁ : o₁.split = (a0.oadd n a', m)) (na : (a0.oadd n a').NF), (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF

Tactic:
obtain - | ⟨a0, n, a'⟩ := a
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
e₁ : o₁.split = (ONote.zero, m)
na : ONote.zero.NF
zero : ∀ (e₁ : o₁.split = (ONote.zero, 0)), (o₁ ^ o₂).NF
zero₁ : ∀ (m : ℕ) (e₁ : o₁.split = (ONote.zero, m + 1)), (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF

Tactic:
rcases m with - | m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
pos : o₂ = 0 → (o₁ ^ o₂).NF
neg : ¬o₂ = 0 → (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF

Tactic:
by_cases o₂ = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : o₂ = 0
pos : NF (if True then 1 else 0)
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]

Premises used: ONote.opowAux2, Pow.pow, HPow.hPow, ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
neg : NF (if False then 1 else 0)
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]

Premises used: ONote.opowAux2, Pow.pow, HPow.hPow, ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : o₂ = 0
⊢ NF (if True then 1 else 0)

Tactic:
decide
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ NF (if False then 1 else 0)

Tactic:
decide
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
pos : m = 0 → (o₁ ^ o₂).NF
neg : ¬m = 0 → (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF

Tactic:
by_cases m = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
pos : NF 1
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, *, zero_def]

Premises used: ONote.opowAux2, Pow.pow, HPow.hPow, ONote.zero_def, ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
⊢ NF 1

Tactic:
decide
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : ¬m = 0
neg : (b'.oadd (Monoid.npow k m.succPNat) 0).NF
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]

Premises used: ONote.opowAux2, Pow.pow, HPow.hPow, ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : ¬m = 0
⊢ (b'.oadd (Monoid.npow k m.succPNat) 0).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
oadd :
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]

Premises used: ONote.opowAux2, Pow.pow, ONote.mulNat_eq_mul, HPow.hPow, ONote.split_eq_scale_split', ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ a0.NF

Tactic:
have := na.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
oadd :
  ∀ (e₂ : o₂.split' = (b', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
oadd₁ :
  ∀ (k : ℕ) (e₂ : o₂.split' = (b', k + 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)

Tactic:
rcases k with - | k
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
oadd :
  ∀ (e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
oadd₁ :
  ∀ (n_1 : ℕ) (e₂ : o₂.split' = (b', n_1 + 1 + 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)

Tactic:
cases k
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)
oadd :
  ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
oadd₁ :
  ∀ (n_1 : ℕ) (e₁ : o₁.split = (a0.oadd n a', n_1 + 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
          (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1))
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)

Tactic:
cases m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n_1 : ℕ
e₂ : o₂.split' = (b', n_1 + 1 + 1)
oadd :
  ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
oadd₁ :
  ∀ (n_2 : ℕ) (e₁ : o₁.split = (a0.oadd n a', n_2 + 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
          (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_2 + 1) : ONote)) k (n_2 + 1))
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)

Tactic:
cases m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)
n_1 : ℕ
e₁ : o₁.split = (a0.oadd n a', n_1 + 1)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
        (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n_1 : ℕ
e₂ : o₂.split' = (b', n_1 + 1 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n_1 : ℕ
e₂ : o₂.split' = (b', n_1 + 1 + 1)
n_2 : ℕ
e₁ : o₁.split = (a0.oadd n a', n_2 + 1)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
        (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_2 + 1) : ONote)) k (n_2 + 1))

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m : ℕ
zero : (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr
succ : ∀ (n : ℕ), (e.opowAux a0 a 0 (n + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n + 1)).repr
⊢ (e.opowAux a0 a 0 m).repr = ω ^ e.repr * (opowAux 0 a0 a 0 m).repr

Tactic:
cases m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
⊢ (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr

Tactic:
simp [opowAux]

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
n : ℕ
⊢ (e.opowAux a0 a 0 (n + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n + 1)).repr

Tactic:
simp [opowAux]

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
pos : ∀ (h : m = 0), (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
neg : ∀ (h : ¬m = 0), (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
by_cases h : m = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
h : m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
simp only [h, opowAux, mulNat_eq_mul, repr_add, repr_scale, repr_mul,
      repr_ofNat, zero_add, mul_add, repr_zero, mul_zero, scale_opowAux e, opow_add, mul_assoc]

Premises used: ONote.zero_add, Ordinal.opow_add, ONote.repr_mul, mul_assoc, ONote.repr_add, ONote.repr_scale, ONote.repr_zero, MulZeroClass.mul_zero, ONote.mulNat_eq_mul, ONote.repr_ofNat, mul_add, ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
h : ¬m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
simp only [h, opowAux, mulNat_eq_mul, repr_add, repr_scale, repr_mul,
      repr_ofNat, zero_add, mul_add, repr_zero, mul_zero, scale_opowAux e, opow_add, mul_assoc]

Premises used: ONote.zero_add, Ordinal.opow_add, ONote.repr_mul, mul_assoc, ONote.repr_add, ONote.repr_scale, ONote.repr_zero, MulZeroClass.mul_zero, ONote.mulNat_eq_mul, ONote.repr_ofNat, mul_add, ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
a' : Ordinal.{0}
e0 : e.repr ≠ 0
h : a' < ω ^ e.repr
aa : a.repr = a'
n : ℕ+
subst : ∀ (h : a.repr < ω ^ e.repr), (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a') ^ ω = (ω ^ e.repr) ^ ω

Tactic:
subst aa
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
⊢ (e.oadd n a).NF

Tactic:
have No := Ne.oadd n (Na.below_of_lt' h)
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
have := omega0_le_oadd e n a
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ (e.oadd n a).repr
⊢ ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr

Tactic:
rw [repr] at this

Premises used: ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
le_antisymm ?_ (opow_le_opow_left _ this)

Premises used: le_antisymm, Ordinal.opow_le_opow_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
refine : (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω ≤ (ω ^ e.repr) ^ ω
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
refine le_antisymm ?_ (opow_le_opow_left _ this)

Premises used: le_antisymm, Ordinal.opow_le_opow_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
apply : ∀ b' < ω, (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b' ≤ (ω ^ e.repr) ^ ω
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ ω ≤ (ω ^ e.repr) ^ ω

Tactic:
apply (opow_le_of_isSuccLimit ((opow_pos _ omega0_pos).trans_le this).ne' isSuccLimit_omega0).2

Premises used: Iff.mpr, Ordinal.isSuccLimit_omega0, Ordinal.omega0_pos, LT.lt.ne', LT.lt.trans_le, Ordinal.opow_pos, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
⊢ (e.oadd n a).repr < ω ^ succ e.repr

Tactic:
have := (No.below_of_lt (lt_succ _)).repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : (e.oadd n a).repr < ω ^ succ e.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr

Tactic:
rw [repr] at this

Premises used: ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
apply : (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω
⊢ (ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
apply (opow_le_opow_left b <| this.le).trans

Premises used: LT.lt.le, LE.le.trans, Ordinal.opow_le_opow_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
rw : ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
⊢ (ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
rw [← opow_mul, ← opow_mul]

Premises used: Ordinal.opow_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
inl : ∀ (h : ω ≤ e.repr), ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
inr : ∀ (h : e.repr < ω), ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
rcases le_or_gt ω (repr e) with h | h

Premises used: Ordinal.omega0, le_or_gt, ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
inl : ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)
h₁ : 0 < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]

Premises used: Order.succ_eq_add_one, Ordinal.one_add_of_omega0_le, Ordinal.add_mul_succ, Order.le_succ
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
inl : 0 < ω
inl₁ : e.repr * succ b + 1 ≤ e.repr * ω
⊢ ω ^ (e.repr * succ b + 1) ≤ ω ^ (e.repr * ω)

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ 0 < ω

Tactic:
omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ 0 < ω

Tactic:
exact omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h_1 : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this_1 : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
hbc : succ b < ω
⊢ e.repr * succ b < e.repr * ω

Tactic:
gcongr