K : Type u
inst✝ : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x } = { toFractionRing := { toFractionRing := x }.toFractionRing }
K : Type u
inst✝ : CommRing K
x y : FractionRing K[X]
xy : { toFractionRing := x }.toFractionRing = { toFractionRing := y }.toFractionRing
⊢ { toFractionRing := x } = { toFractionRing := y }
subst xy
no goals
K : Type u
inst✝ : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x } = { toFractionRing := { toFractionRing := x }.toFractionRing }
rfl