no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_2
M'' : Type ?u.688815
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'
a : M
b : { x // x ∈ S }
eq1 : b • m = ↑f a
⊢ ∃ u,
    u • b • (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).fst =
      u • (Exists.choose (_ : ∃ x, x.snd • m = ↑f x.fst)).snd • a
erw [← IsLocalizedModule.eq_iff_exists S f, f.map_smul, f.map_smul, ← (surj' _).choose_spec,
← mul_smul, mul_comm, mul_smul, eq1]