R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n + single () 1)) (φ * X) = ↑(MvPowerSeries.coeff R (single () n)) φ
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(coeff R (n + 1)) (φ * X) = ↑(coeff R n) φ
simp only [coeff, Finsupp.single_add]
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n)) φ = ↑(MvPowerSeries.coeff R (single () n)) φ * 1
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n + single () 1)) (φ * X) = ↑(MvPowerSeries.coeff R (single () n)) φ
convert φ.coeff_add_mul_monomial (single () n) (single () 1) _
no goals
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n)) φ = ↑(MvPowerSeries.coeff R (single () n)) φ * 1
rw [mul_one]