R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () 1 + single () n)) (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, add_comm n 1]
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n)) φ = 1 * ↑(MvPowerSeries.coeff R (single () n)) φ
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () 1 + single () n)) (X * φ) = ↑(MvPowerSeries.coeff R (single () n)) φ
convert φ.coeff_add_monomial_mul (single () 1) (single () n) _
no goals
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ ↑(MvPowerSeries.coeff R (single () n)) φ = 1 * ↑(MvPowerSeries.coeff R (single () n)) φ
rw [one_mul]