no goals
R : Type u_2
inst✝² : Semiring R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_1
inst✝ : Semiring T
f : R →+* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
r : R
⊢ ↑(universalHom f fS hf) (↑numeratorHom r) = ↑f r
simp [numeratorHom_apply, universalHom_apply]