no goals
α : Type u_3
β : Type ?u.619677
γ : Type ?u.619680
ι : Type ?u.619683
M : Type u_2
M' : Type ?u.619689
N : Type ?u.619692
P : Type ?u.619695
G : Type ?u.619698
H : Type ?u.619701
R : Type u_1
S : Type ?u.619707
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
b : R
hb : b ≠ 0
g : α →₀ M
a : α
⊢ a ∈ (b • g).support ↔ a ∈ g.support
simp [Finsupp.smul_apply, hb]