case H₁
a b c : Ordinal
ba : b + a = a
⊢ (a + b) * succ 0 = a * succ 0 + b

case H₂
a b c : Ordinal
ba : b + a = a
⊢ ∀ (o : Ordinal), (a + b) * succ o = a * succ o + b → (a + b) * succ (succ o) = a * succ (succ o) + b

case H₃
a b c : Ordinal
ba : b + a = a
⊢ ∀ (o : Ordinal),
    IsLimit o → (∀ (o' : Ordinal), o' < o → (a + b) * succ o' = a * succ o' + b) → (a + b) * succ o = a * succ o + b
a b c : Ordinal
ba : b + a = a
⊢ (a + b) * succ c = a * succ c + b
apply limitRecOn c
no goals
case H₁
a b c : Ordinal
ba : b + a = a
⊢ (a + b) * succ 0 = a * succ 0 + b
simp only [succ_zero, mul_one]
case H₂
a b c✝ : Ordinal
ba : b + a = a
c : Ordinal
IH : (a + b) * succ c = a * succ c + b
⊢ (a + b) * succ (succ c) = a * succ (succ c) + b
case H₂
a b c : Ordinal
ba : b + a = a
⊢ ∀ (o : Ordinal), (a + b) * succ o = a * succ o + b → (a + b) * succ (succ o) = a * succ (succ o) + b
intro c IH
no goals
case H₂
a b c✝ : Ordinal
ba : b + a = a
c : Ordinal
IH : (a + b) * succ c = a * succ c + b
⊢ (a + b) * succ (succ c) = a * succ (succ c) + b
rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ]
case H₃
a b c✝ : Ordinal
ba : b + a = a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → (a + b) * succ o' = a * succ o' + b
⊢ (a + b) * succ c = a * succ c + b
case H₃
a b c : Ordinal
ba : b + a = a
⊢ ∀ (o : Ordinal),
    IsLimit o → (∀ (o' : Ordinal), o' < o → (a + b) * succ o' = a * succ o' + b) → (a + b) * succ o = a * succ o + b
intro c l IH
no goals
case H₃
a b c✝ : Ordinal
ba : b + a = a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → (a + b) * succ o' = a * succ o' + b
⊢ (a + b) * succ c = a * succ c + b
rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc]