no goals
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
x y : R
w : r x y
⊢ ↑(mkRingHom r) x = ↑(mkRingHom r) y
simp [mkRingHom_def, Quot.sound (Rel.of w)]