case mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Injective ↑(lift f hg) → ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y

case mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ (∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y) → Injective ↑(lift f hg)
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Injective ↑(lift f hg) ↔ ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
constructor
case mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
case mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ Injective ↑(lift f hg) → ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
intro H x y
case mp.mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y → ↑g x = ↑g y

case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑g x = ↑g y → ↑(toMap f) x = ↑(toMap f) y
case mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
constructor
no goals
case mp.mp
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑(toMap f) x = ↑(toMap f) y → ↑g x = ↑g y
exact f.eq_of_eq hg
case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑g x = ↑g y
⊢ ↑(toMap f) x = ↑(toMap f) y
case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
⊢ ↑g x = ↑g y → ↑(toMap f) x = ↑(toMap f) y
intro h
case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑(lift f hg) (↑(toMap f) x) = ↑(lift f hg) (↑(toMap f) y)
⊢ ↑(toMap f) x = ↑(toMap f) y
case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑g x = ↑g y
⊢ ↑(toMap f) x = ↑(toMap f) y
rw [← f.lift_eq hg, ← f.lift_eq hg] at h
no goals
case mp.mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : Injective ↑(lift f hg)
x y : M
h : ↑(lift f hg) (↑(toMap f) x) = ↑(lift f hg) (↑(toMap f) y)
⊢ ↑(toMap f) x = ↑(toMap f) y
exact H h
case mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
⊢ z = w
case mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
⊢ (∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y) → Injective ↑(lift f hg)
intro H z w h
case mpr.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝ : M × { x // x ∈ S }
h✝ : z * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
case mpr
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
⊢ z = w
obtain ⟨_, _⟩ := f.surj z
case mpr.intro.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
case mpr.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝ : M × { x // x ∈ S }
h✝ : z * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
obtain ⟨_, _⟩ := f.surj w
case mpr.intro.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ mk' f (sec f z).fst (sec f z).snd = mk' f (sec f w).fst (sec f w).snd
case mpr.intro.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ z = w
rw [← f.mk'_sec z, ← f.mk'_sec w]
no goals
case mpr.intro.intro
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
H : ∀ (x y : M), ↑(toMap f) x = ↑(toMap f) y ↔ ↑g x = ↑g y
z w : N
h : ↑(lift f hg) z = ↑(lift f hg) w
w✝¹ : M × { x // x ∈ S }
h✝¹ : z * ↑(toMap f) ↑w✝¹.snd = ↑(toMap f) w✝¹.fst
w✝ : M × { x // x ∈ S }
h✝ : w * ↑(toMap f) ↑w✝.snd = ↑(toMap f) w✝.fst
⊢ mk' f (sec f z).fst (sec f z).snd = mk' f (sec f w).fst (sec f w).snd
exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)