awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
e₁ : o₁.split = (ONote.zero, m)
N₁ : ONote.zero.NF
r₁ : o₁.repr = ONote.zero.repr + (↑m : Ordinal.{0})
zero :
  ∀ (e₁ : o₁.split = (ONote.zero, 0)) (r₁ : o₁.repr = ONote.zero.repr + (↑0 : Ordinal.{0})),
    (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
zero₁ :
  ∀ (m : ℕ) (e₁ : o₁.split = (ONote.zero, m + 1)) (r₁ : o₁.repr = ONote.zero.repr + (↑(m + 1) : Ordinal.{0})),
    (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
rcases m with - | m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})
pos : ∀ (h : o₂ = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
neg : ∀ (h : ¬o₂ = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
by_cases h : o₂ = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})
h : o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp [opow_def, opowAux2, e₁, h, r₁]

Premises used: ONote.opowAux2, ONote.opow_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + (↑0 : Ordinal.{0})
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simpa [opow_def, opowAux2, e₁, h, r₁, eqComm] using mt repr_inj.1 h

Premises used: ONote.opowAux2, mt, ONote.repr_inj, Iff.mp, ONote.opow_def, eqComm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : ONote.zero.NF
m : ℕ
e₁ : o₁.split = (ONote.zero, m + 1)
r₁ : o₁.repr = ONote.zero.repr + (↑(m + 1) : Ordinal.{0})
zero : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

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
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ b'.NF

Tactic:
obtain ⟨_, 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
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
⊢ o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})

Tactic:
obtain ⟨_, 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
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
pos : ∀ (h : m = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
neg : ∀ (h : ¬m = 0), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
by_cases h : m = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp [opowAux2, opow_def, e₁, h, r₁, r₂]

Premises used: ONote.opowAux2, ONote.opow_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
neg :
  ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add,
          add_zero]

Premises used: Nat.cast_succ, ONote.opowAux2, zero_add, ONote.repr, ONote.opow_def, add_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
neg :
  ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    ω ^ b'.repr * HPow.hPow (β := Ordinal.{0}) (HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1) (↑k : Ordinal.{0})
neg₁ : 1 < HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1
neg₂ : HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 < ω
⊢ ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 ^ (ω * b'.repr + (↑k : Ordinal.{0}))

Tactic:
rw [opow_add, opow_mul, opow_omega0]

Premises used: Ordinal.opow_mul, Ordinal.opow_omega0, Ordinal.opow_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ ω ^ b'.repr * (↑(↑(m.succPNat ^ k) : ℕ) : Ordinal.{0}) =
    ω ^ b'.repr * HPow.hPow (β := Ordinal.{0}) (HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1) (↑k : Ordinal.{0})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ 1 < HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1

Tactic:
simpa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
neg : ∃ (n : ℕ), Eq (α := Ordinal.{0}) (↑m.succ : Ordinal.{0}) (↑n : Ordinal.{0})
⊢ HAdd.hAdd (α := Ordinal.{0}) (↑m : Ordinal.{0}) 1 < ω

Tactic:
rw [← Nat.cast_succ, lt_omega0]

Premises used: Nat.cast_succ, Ordinal.lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ ∃ (n : ℕ), Eq (α := Ordinal.{0}) (↑m.succ : Ordinal.{0}) (↑n : Ordinal.{0})

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + (↑(m + 1) : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
h : ¬m = 0
⊢ ∃ (n : ℕ), Eq (α := Ordinal.{0}) (↑m.succ : Ordinal.{0}) (↑n : Ordinal.{0})

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
⊢ a0.NF

Tactic:
haveI := N₁.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this : a0.NF
⊢ a'.NF

Tactic:
haveI := N₁.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
⊢ a0.repr ≠ 0

Tactic:
obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)

Premises used: ONote.split_dvd, ONote.NF.of_dvd_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
⊢ ω ∣ a'.repr

Tactic:
obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)

Premises used: ONote.split_dvd, ONote.NF.of_dvd_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
⊢ a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr

Tactic:
have al := split_add_lt e₁
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
⊢ (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})

Tactic:
simp only [ONote.repr_ofNat, ONote.repr_add]

Premises used: ONote.repr_add, ONote.repr_ofNat
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
⊢ (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})

Tactic:
have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
oadd : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

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
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ b'.NF

Tactic:
obtain ⟨_, 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
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
⊢ o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})

Tactic:
obtain ⟨_, 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
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
oadd :
  repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]

Premises used: ONote.opowAux2, ONote.repr, ONote.split_eq_scale_split', ONote.opow_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
oadd :
  ∀ (e₂ : o₂.split' = (b', 0)) (r₂ : o₂.repr = ω * b'.repr + (↑0 : Ordinal.{0})),
    repr
        (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
        | (b, 0) => (a0 * b).oadd 1 0
        | (b, k.succ) =>
          (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
oadd₁ :
  ∀ (k : ℕ) (e₂ : o₂.split' = (b', k + 1)) (r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})),
    repr
        (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
        | (b, 0) => (a0 * b).oadd 1 0
        | (b, k.succ) =>
          (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr

Tactic:
rcases k with - | k
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
e₂ : o₂.split' = (b', 0)
r₂ : o₂.repr = ω * b'.repr + (↑0 : Ordinal.{0})
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr

Tactic:
simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]

Premises used: Ordinal.opow_mul, add_assoc, ONote.repr_opow_aux₁
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((a0 * scale 1 b').opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr

Tactic:
simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc]

Premises used: Ordinal.opow_mul, Ordinal.opow_add, add_assoc, mul_assoc
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ω ^ (a0 * scale 1 b').repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((a0 * scale 1 b').opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))

Tactic:
rw [repr_opow_aux₁ a00 al aa, scale_opowAux]

Premises used: ONote.repr_opow_aux₁, ONote.scale_opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((ω ^ a0.repr) ^ ω) ^ b'.repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ω ^ (a0 * scale 1 b').repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))

Tactic:
simp only [repr_mul, repr_scale, repr, opow_zero, PNat.val_ofNat, Nat.cast_one, mul_one,
        add_zero, opow_one, opow_mul]

Premises used: Ordinal.opow_mul, Ordinal.opow_one, ONote.repr_mul, ONote.repr_scale, PNat.val_ofNat, ONote.repr, Ordinal.opow_zero, mul_one, add_zero, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})))
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((ω ^ a0.repr) ^ ω) ^ b'.repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))

Tactic:
rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]

Premises used: PNat.val, HMul.hMul, Ordinal.omega0, add_assoc, Nat.cast, HPow.hPow, ONote.repr, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
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})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  (ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})))

Tactic:
congr 1