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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(lift f hg) 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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
⊢ lift f hg = 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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd * 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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(lift f hg) x✝ = ↑j x✝
rw [lift_spec, ← hj, ← hj, ← j.map_mul]
case h.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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(toMap f) (sec f x✝).fst = ↑(toMap f) ↑(sec f x✝).snd * 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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑j (↑(toMap f) (sec f x✝).fst) = ↑j (↑(toMap f) ↑(sec f x✝).snd * x✝)
apply congr_arg
no goals
case h.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
hj : ∀ (x : M), ↑j (↑(toMap f) x) = ↑g x
x✝ : N
⊢ ↑(toMap f) (sec f x✝).fst = ↑(toMap f) ↑(sec f x✝).snd * x✝
rw [← sec_spec']