-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_injective_of_injective (hg : Injective g) (k : LocalizationMap (S.map g) Q) :
    Injective (map f (apply_coe_mem_map g S) k) := fun z w hizw ↦ by
  set i := map f (apply_coe_mem_map g S) k
  have ifkg (a : M) : i (f.toMap a) = k.toMap (g a) := map_eq f (apply_coe_mem_map g S) a
  let ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
  have : k.toMap (g z') = k.toMap (g w')

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
⊢ z = w

Tactic:
obtain ⟨⟨_, c, hc, rfl⟩, eq⟩ := k.exists_of_eq _ _ this

Result:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : ↑⟨g c, ⋯⟩ * g z' = ↑⟨g c, ⋯⟩ * g w'
⊢ z = w

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
⊢ z = w

Tactic:
have : k.toMap (g z') = k.toMap (g w') := by
  rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
⊢ z = w

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
⊢ z = w

Tactic:
have ifkg (a : M) : i (f.toMap a) = k.toMap (g a) := map_eq f (apply_coe_mem_map g S) a

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
⊢ z = w

Proof state:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : c * z' = c * w'
⊢ ∃ c, ↑c * z' = ↑c * w'

Tactic:
exact ⟨⟨c, hc⟩, eq⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
⊢ z = w

Tactic:
let ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
⊢ z = w

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
⊢ k.toMap (g z') = k.toMap (g w')

Tactic:
rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
hizw : (f.map ⋯ k) z = (f.map ⋯ k) w
⊢ z = w

Tactic:
set i := map f (apply_coe_mem_map g S) k

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
⊢ z = w

Proof state:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : ↑⟨g c, ⋯⟩ * g z' = ↑⟨g c, ⋯⟩ * g w'
⊢ z = w

Tactic:
simp_rw [← map_mul, hg.eq_iff] at eq

Result:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : c * z' = c * w'
⊢ z = w