-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
oadd :
  ∀ (e : b.fundamentalSequence = Sum.inl none),
    (a.oadd m b).FundamentalSequenceProp
      (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) 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 (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) 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))
oadd₁ :
  ∀ (b' : ONote) (e : b.fundamentalSequence = Sum.inl (some b')),
    (a.oadd m b).FundamentalSequenceProp
      (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) 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 (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) 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))
oadd₂ :
  ∀ (f : ℕ → ONote) (e : b.fundamentalSequence = Sum.inr f),
    (a.oadd m b).FundamentalSequenceProp
      (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) 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 (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) 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))
⊢ (a.oadd m b).FundamentalSequenceProp
    (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) b.fundamentalSequence 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 (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) 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:
rcases e : b.fundamentalSequence with (⟨_ | b'⟩ | f)

Premises used: ONote.fundamentalSequence