no goals
R : Type u_3
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_1
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
j k : S → P
hj1 : j 1 = 1
hk1 : k 1 = 1
hjm : ∀ (a b : S), j (a * b) = j a * j b
hkm : ∀ (a b : S), k (a * b) = k a * k b
h : ∀ (a : R), j (↑(algebraMap R S) a) = k (↑(algebraMap R S) a)
j' : S →* P := { toOneHom := { toFun := j, map_one' := hj1 }, map_mul' := hjm }
k' : S →* P := { toOneHom := { toFun := k, map_one' := hk1 }, map_mul' := hkm }
this : j' = k'
⊢ j'.toFun = k'.toFun
rw [this]