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
⊢ { toQuot := Quot.mk (Rel r) 1 } = RingQuot.one r
rw [one_def]