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