J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
i j : J
xi : F.obj i
xj : F.obj j
⊢ Quot.mk (Quot.Rel F) { fst := i, snd := xi } = Quot.mk (Quot.Rel F) { fst := j, snd := xj } ↔
    FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
i j : J
xi : F.obj i
xj : F.obj j
⊢ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔
    FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }
change Quot.mk _ _ = Quot.mk _ _ ↔ _
no goals
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
i j : J
xi : F.obj i
xj : F.obj j
⊢ Quot.mk (Quot.Rel F) { fst := i, snd := xi } = Quot.mk (Quot.Rel F) { fst := j, snd := xj } ↔
    FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }
rw [Quot.eq, FilteredColimit.rel_eq_eqvGen_quot_rel]