Theorem: PolynomialMap.support_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
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (Function.support fun i => ((fun p => component p f) i).toFun' S m) =
    ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
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 : ℕ
⊢ (n ∈ Function.support fun i => ((fun p => component p f) i).toFun' S m) ↔
    n ∈ ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support

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 : ℕ
⊢ (n ∈ Function.support fun i => ((fun p => component p f) i).toFun' S m) ↔
    n ∈ ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
simp only [component, Finsupp.fun_support_eq, Finset.mem_coe, Finsupp.mem_support_iff, ne_eq]
State after:
no goals