-- 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
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = s.ι.app WalkingParallelPair.one
h₀ :
  CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.hom
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
        m) =
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
⊢ Eq (α :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ⟶
      s.pt)
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m)
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
have h₁ : CategoryStruct.comp (Y :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.inr (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m) =
  CategoryStruct.comp (Y :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.inr (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) sorry)
Tactic: ext