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 → Prop
T : Type u₄
inst✝ : Semiring T
s : A → A → Prop
x y : A
w : s x y
⊢ ↑(mkAlgHom S s) x = ↑(mkAlgHom S s) y
simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]