Theorem: PowerSeries.constantCoeff_subst (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
⊢ (MvPowerSeries.constantCoeff τ S) (subst a f) = ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.constantCoeff τ S) (a ^ d)
Tactic:
simp only [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]
State after:
no goals