Theorem: PolynomialMap.LocFinsupp_component_eq (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯ =
    (Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))
Tactic:
ext n
State after:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯) n =
    ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) n

State before:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯) n =
    ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) n
Tactic:
simp only [component, Finsupp.ofSupportFinite_coe]
State after:
no goals