-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
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) ⋯)
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) ⋯)
⊢ 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) ⋯)

Tactic:
ext