Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ.zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

pp: case oadd.succ.zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF

pp: case oadd.succ.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

pp: case oadd.succ.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝¹ : ℕ
e₂ : o₂.split' = (b', n✝¹ + 1 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', n✝¹ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF

Tactic:
<;>

Goal state after:
case oadd.succ.zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

case oadd.succ.zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF

case oadd.succ.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

case oadd.succ.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝¹ : ℕ
e₂ : o₂.split' = (b', n✝¹ + 1 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', n✝¹ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF