Theorem: PolynomialMap.image_eq_coeff_sum' (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι✝ : Type uι
inst✝⁴ : DecidableEq ι✝
inst✝³ : Fintype ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun S (r.sum fun i a => a ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ r.support, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Tactic:
rw [Finsupp.sum, image_eq_coeff_finset_sum]
State after:
no goals