R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
⊢ (if m < n then ↑(coeff R m) (φ + ψ) else 0) =
    (if m < n then ↑(coeff R m) φ else 0) + if m < n then ↑(coeff R m) ψ else 0
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
⊢ Polynomial.coeff (trunc n (φ + ψ)) m = Polynomial.coeff (trunc n φ + trunc n ψ) m
simp only [coeff_trunc, AddMonoidHom.map_add, Polynomial.coeff_add]
case inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
H : m < n
⊢ ↑(coeff R m) (φ + ψ) = ↑(coeff R m) φ + ↑(coeff R m) ψ

case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
⊢ (if m < n then ↑(coeff R m) (φ + ψ) else 0) =
    (if m < n then ↑(coeff R m) φ else 0) + if m < n then ↑(coeff R m) ψ else 0
split_ifs with H
no goals
case inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
H : m < n
⊢ ↑(coeff R m) (φ + ψ) = ↑(coeff R m) φ + ↑(coeff R m) ψ
rfl
no goals
case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
φ ψ : PowerSeries R
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0
rw [zero_add]