no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F = pushout.inr
convert (whisker_eq Limits.coprod.inl pushout.condition :
  (_ : F.obj _ ⟶  constructCoequalizer _) = _) <;> simp