no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_2
M'' : Type ?u.915771
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
s : { x // x ∈ S }
⊢ mk' f m s = 0 ↔ ∃ s', s' • m = 0
simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]