no goals
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows
apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)