-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma smul_eq_iff_of_mem
    (r : R) (hr : r ∈ S) (x y : LocalizedModule S M) :
    r • x = y ↔ x = Localization.mk 1 ⟨r, hr⟩ • y

Proof state:
case h.h.mpr.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
refine ⟨a, ha, ?_⟩

Result:
case h.h.mpr.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • s • n

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
fconstructor

Result:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n

Proof state:
case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
rintro ⟨a, ha, eq1⟩

Result:
case h.h.mpr.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ ∃ a ∈ S, a • t • r • m = a • s • n

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ ∃ u, u • (⟨r, hr⟩ * t) • m = u • s • n

Tactic:
simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]

Result:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Proof state:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
rintro ⟨a, ha, eq1⟩

Result:
case h.h.mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Proof state:
case h.h.mpr.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • s • n

Tactic:
rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]

Result:
no goals

Proof state:
case h.h.mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
refine ⟨a, ha, ?_⟩

Result:
case h.h.mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • (⟨r, hr⟩ * t) • m = a • s • n

Proof state:
case h.h.mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]

Result:
no goals

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ r • mk m s = mk n t ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • mk n t

Tactic:
rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]

Result:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ ∃ u, u • (⟨r, hr⟩ * t) • m = u • s • n