no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F = pullback.snd
convert (eq_whisker pullback.condition Limits.prod.fst :
 (_ : constructEqualizer F ⟶  F.obj WalkingParallelPair.zero) = _) <;> simp