M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_1
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑g (sec f (↑(toMap f) x)).fst = ↑g (↑(sec f (↑(toMap f) x)).snd * x)
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_1
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑(lift f hg) (↑(toMap f) x) = ↑g x
rw [lift_spec, ← g.map_mul]
no goals
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_1
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑g (sec f (↑(toMap f) x)).fst = ↑g (↑(sec f (↑(toMap f) x)).snd * x)
exact f.eq_of_eq hg (by rw [sec_spec', f.toMap.map_mul])
no goals
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_1
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x : M
⊢ ↑(toMap f) (sec f (↑(toMap f) x)).fst = ↑(toMap f) (↑(sec f (↑(toMap f) x)).snd * x)
rw [sec_spec', f.toMap.map_mul]