no goals
α : Type u_3
β : Type ?u.91934
A : Type ?u.91937
B : Type ?u.91940
M : Type u_2
N : Type ?u.91946
P : Type ?u.91949
R : Type u_1
S : Type ?u.91955
G : Type ?u.91958
M₀ : Type ?u.91961
G₀ : Type ?u.91964
ι : Sort ?u.91967
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
g : α → M
hc : c ≠ 0
x : α
⊢ x ∈ support (c • g) ↔ x ∈ support g
simp only [hc, mem_support, Pi.smul_apply, Ne.def, smul_eq_zero, false_or_iff]