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_3
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 i
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_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
i : ℕ
⊢ (i ∈ Function.support fun i => ((fun p => component p f) i).toFun S m) ↔
    i ∈ ↑((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_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
i : ℕ
⊢ (i ∈ Function.support fun i => ((fun p => component p f) i).toFun S m) ↔
    i ∈ ↑((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
rw [Function.mem_support, ne_eq, Finset.mem_coe, Finsupp.mem_support_iff, not_iff_not,
  component_toFun]
State after:
no goals