M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
⊢ ↑(toMap f) x = ↑(toMap f) y
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) (↑c * x) = ↑(toMap f) (↑c * y)
⊢ ↑(toMap f) x = ↑(toMap f) y
rw [f.toMap.map_mul, f.toMap.map_mul] at h
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
u : ((fun x => N) ↑c)ˣ
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
⊢ ↑(toMap f) x = ↑(toMap f) y
cases' f.map_units c with u hu
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
u : ((fun x => N) ↑c)ˣ
h : ↑u * ↑(toMap f) x = ↑u * ↑(toMap f) y
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) ↑c * ↑(toMap f) x = ↑(toMap f) ↑c * ↑(toMap f) y
u : ((fun x => N) ↑c)ˣ
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
rw [← hu] at h
no goals
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.626659
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
u : ((fun x => N) ↑c)ˣ
h : ↑u * ↑(toMap f) x = ↑u * ↑(toMap f) y
hu : ↑u = ↑(toMap f) ↑c
⊢ ↑(toMap f) x = ↑(toMap f) y
exact (Units.mul_right_inj u).1 h