-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem toMap_injective_iff
    {M N : Type*} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : LocalizationMap S N) :
    Injective (LocalizationMap.toMap f) ↔ ∀ ⦃x⦄, x ∈ S → IsLeftRegular x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

Tactic:
constructor <;> intro h

Result:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂
⊢ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
⊢ ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂

Proof state:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
hab : f.toMap a = f.toMap b
⊢ a = b

Tactic:
rw [LocalizationMap.eq_iff_exists] at hab

Result:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
hab : ∃ c, ↑c * a = ↑c * b
⊢ a = b

Proof state:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
⊢ ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂

Tactic:
intro a b hab

Result:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
hab : f.toMap a = f.toMap b
⊢ a = b

Proof state:
case mp.a.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
y z : M
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
x : ↥S
hyz : (fun x_1 => ↑x * x_1) y = (fun x_1 => ↑x * x_1) z
⊢ ∃ c, ↑c * y = ↑c * z

Tactic:
use x

Result:
no goals

Proof state:
case mp.a
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
⊢ ∃ c, ↑c * y = ↑c * z

Tactic:
lift x to S using hx

Result:
case mp.a.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
y z : M
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
x : ↥S
hyz : (fun x_1 => ↑x * x_1) y = (fun x_1 => ↑x * x_1) z
⊢ ∃ c, ↑c * y = ↑c * z

Proof state:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
hab : ∃ c, ↑c * a = ↑c * b
⊢ a = b

Tactic:
obtain ⟨c,hc⟩ := hab

Result:
case mpr.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
c : ↥S
hc : ↑c * a = ↑c * b
⊢ a = b

Proof state:
case mpr.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
a b : M
c : ↥S
hc : ↑c * a = ↑c * b
⊢ a = b

Tactic:
apply (fun x a => h a) c (SetLike.coe_mem c) hc

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ Injective ⇑f.toMap ↔ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

Tactic:
rw [Injective]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

Proof state:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
⊢ y = z

Tactic:
apply (fun y z _ => h) y z x

Result:
case mp.a
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
⊢ ∃ c, ↑c * y = ↑c * z

Proof state:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂
⊢ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

Tactic:
intro x hx y z hyz

Result:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
⊢ y = z

Proof state:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
h : ∀ ⦃a₁ a₂ : M⦄, f.toMap a₁ = f.toMap a₂ → a₁ = a₂
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
⊢ y = z

Tactic:
simp_rw [LocalizationMap.eq_iff_exists] at h

Result:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
hx : x ∈ S
y z : M
hyz : (fun x_1 => x * x_1) y = (fun x_1 => x * x_1) z
h : ∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂
⊢ y = z