case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j : J
x : F.obj j
⊢ ↑(colimitEquivQuot F).symm (↑(colimitEquivQuot F) (colimit.ι F j x)) =
    ↑(colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) { fst := j, snd := x })
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j : J
x : F.obj j
⊢ ↑(colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) { fst := j, snd := x }
apply (colimitEquivQuot F).symm.injective
no goals
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j : J
x : F.obj j
⊢ ↑(colimitEquivQuot F).symm (↑(colimitEquivQuot F) (colimit.ι F j x)) =
    ↑(colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) { fst := j, snd := x })
simp