no goals
α : Type u_1
M : Type u_2
N : Type ?u.60317
P : Type ?u.60320
R : Type u_3
S : Type ?u.60326
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
p : α →₀ M
⊢ p ∈ supported M R ↑p.support
rw [Finsupp.mem_supported]