-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem r.isEquiv : IsEquiv _ (r S M) :=
  { refl := fun ⟨m, s⟩ => ⟨1, by rw [one_smul]⟩
    trans := fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨m3, s3⟩ ⟨u1, hu1⟩ ⟨u2, hu2⟩ => by
      use u1 * u2 * s2
      -- Put everything in the same shape, sorting the terms using `simp`
      have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm
      have hu2' := congr_arg ((u1 * s1) • ·) hu2.symm
      simp only [← mul_smul, smul_assoc, mul_assoc, mul_comm, mul_left_comm] at hu1' hu2' ⊢
      rw [hu2', hu1']
    symm := fun ⟨_, _⟩ ⟨_, _⟩ ⟨u, hu⟩ => ⟨u, hu.symm⟩ }

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M × ↥S
m : M
s : ↥S
⊢ 1 • (m, s).2 • (m, s).1 = 1 • (m, s).2 • (m, s).1

Tactic:
rw [one_smul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ r S M (m1, s1) (m3, s3)

Tactic:
use u1 * u2 * s2

Result:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (fun x => (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1) = (fun x => (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1)
hu2' : (fun x => (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1) = (fun x => (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1)
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1

Tactic:
simp only [← mul_smul, smul_assoc, mul_assoc, mul_comm, mul_left_comm] at hu1' hu2' ⊢

Result:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3

Tactic:
rw [hu2', hu1']

Result:
no goals