no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : FractionRing K[X]
⊢ { toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
simp only [Div.div, HDiv.hDiv,  RatFunc.div]