no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : Quot.Rel F x y
f : x.fst ⟶ y.fst
h : y.snd = F.map f x.snd
⊢ F.map f x.snd = F.map (𝟙 y.fst) y.snd
rw [← h, FunctorToTypes.map_id_apply]