-- 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ (G.mapCone (equalizerCone K)).π.app j = s.π.app j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = s.π.app WalkingParallelPair.zero
h₀ :
  CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (m ≫
        Iso.hom
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.fst (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) =
    CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
      (pullback.fst (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
h₁ :
  CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (m ≫
        Iso.hom
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.snd (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) =
    CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
      (pullback.snd (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
⊢ Eq (α :=
    s.pt ⟶
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
    (m ≫
      Iso.hom
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
    (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)

Tactic:
ext