case h
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)
j : N →* P
x✝ : N
⊢ ↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y))) x✝ = ↑j x✝
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)
j : N →* P
⊢ lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y)) = j
ext
case h
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)
j : N →* P
x✝ : N
⊢ ↑(MonoidHom.comp j (toMap f)) (sec f x✝).fst = ↑(MonoidHom.comp j (toMap f)) ↑(sec f x✝).snd * ↑j x✝
case h
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)
j : N →* P
x✝ : N
⊢ ↑(lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y))) x✝ = ↑j x✝
rw [lift_spec]
case h
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)
j : N →* P
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd) * ↑j x✝
case h
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)
j : N →* P
x✝ : N
⊢ ↑(MonoidHom.comp j (toMap f)) (sec f x✝).fst = ↑(MonoidHom.comp j (toMap f)) ↑(sec f x✝).snd * ↑j x✝
show j _ = j _ * _
no goals
case h
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)
j : N →* P
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd) * ↑j x✝
erw [← j.map_mul, sec_spec']