no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun n φ) = if m < n then ↑(coeff R m) φ else 0
simp [truncFun, MvPolynomial.coeff_sum]