-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem surj₂ (f : LocalizationMap S N) (z w : N) : ∃ z' w' : M, ∃ d : S,
    (z * f.toMap d = f.toMap z') ∧  (w * f.toMap d = f.toMap w')

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'

Tactic:
refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩

Result:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ z * f.toMap ↑(a.2 * b.2) = f.toMap (a.1 * ↑b.2)

case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ w * f.toMap ↑(a.2 * b.2) = f.toMap (↑a.2 * b.1)

Proof state:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ z * f.toMap ↑(a.2 * b.2) = f.toMap (a.1 * ↑b.2)

Tactic:
simp_rw [mul_def, map_mul, ← ha]

Result:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ z * (f.toMap ↑a.2 * f.toMap ↑b.2) = z * f.toMap ↑a.2 * f.toMap ↑b.2

Proof state:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ z * (f.toMap ↑a.2 * f.toMap ↑b.2) = z * f.toMap ↑a.2 * f.toMap ↑b.2

Tactic:
exact (mul_assoc z _ _).symm

Result:
no goals

Proof state:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ w * f.toMap ↑(a.2 * b.2) = f.toMap (↑a.2 * b.1)

Tactic:
simp_rw [mul_def, map_mul, ← hb]

Result:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ w * (f.toMap ↑a.2 * f.toMap ↑b.2) = f.toMap ↑a.2 * (w * f.toMap ↑b.2)

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
⊢ ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'

Tactic:
let ⟨a, ha⟩ := surj f z

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
⊢ ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
⊢ ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'

Tactic:
let ⟨b, hb⟩ := surj f w

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'

Proof state:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f.toMap ↑a.2 = f.toMap a.1
b : M × ↥S
hb : w * f.toMap ↑b.2 = f.toMap b.1
⊢ w * (f.toMap ↑a.2 * f.toMap ↑b.2) = f.toMap ↑a.2 * (w * f.toMap ↑b.2)

Tactic:
exact mul_left_comm w _ _

Result:
no goals