Theorem: PolynomialMap.LocFinsupp_component (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
x✝¹ : CommRing S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (Function.support fun i => ((fun p => component p f) i).toFun' S m).Finite
Tactic:
simp only [support_component', Finset.finite_toSet]
State after:
no goals