Theorem: PolynomialMap.component_toFun (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✝ p : ℕ
f : M →ₚ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (component p f).toFun S = fun m =>
    ((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) p
Tactic:
sorry
State after:
no goals