Theorem: PolynomialMap.component_add (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 g : M →ₚ[R] N
⊢ component p (f + g) = component p f + component p g
Tactic:
ext S _ _ sm
State after:
case toFun'.h.h.h.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✝ p : ℕ
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (f + g)).toFun' S sm = (component p f + component p g).toFun' S sm

State before:
case toFun'.h.h.h.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✝ p : ℕ
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (f + g)).toFun' S sm = (component p f + component p g).toFun' S sm
Tactic:
simp only [component, add_def_apply, map_add, Finsupp.coe_add, Pi.add_apply]
State after:
no goals