Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inl none with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

pp: case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inl (some b') with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inr f with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

Tactic:
<;>

Goal state after:
case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inl none with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inl (some b') with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ (a.oadd m b).FundamentalSequenceProp
    (match Sum.inr f with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))