no goals
J : Type w
C : Type u
inst✝ : Category C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j
cases j <;> aesop_cat