-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = (f : (a : M) → M') a
rw :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M') (b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) : M')
    ((f : (a : M) → M') (⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a) : M')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) :
      M')
    ((f : (a : M) → M') (⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a) : M')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) :
      M')
    ((f : (a : M) → M')
        ((↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R) • a) :
      M')
rw₃ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 : M') =
    (f : (a : M) → M') ((↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R) • a)
rw₄ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 : M') =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₅ :
  (↑b : R) • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₆ :
  b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₇ :
  b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2
      ((f : (a : M) → M') a : M')
⊢ ∃ (u : ↥S),
    u • b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 =
      u • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a
have rw₈ : (b * sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2) • m =
  HSMul.hSMul (β := M') sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2
    ((f : (a : M) → M') a : M')
Tactic: rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
        f.map_smul, ← (surj _ _ _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def,
        ← mul_smul, mul_comm, mul_smul, eq1]