-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
h₀ :
  pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    CategoryStruct.comp (Y :=
      pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) :
        F.obj WalkingParallelPair.one ⟶
          pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ :
        pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ⟶
          c.pt)
⊢ m = pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯
have h₁ : pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
    m =
  CategoryStruct.comp (Y :=
    pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
    (pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) :
      F.obj WalkingParallelPair.one ⟶
        pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
    (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) sorry :
      pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ⟶
        c.pt)
Tactic: apply pushout.hom_ext