-- 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 : 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))))
⊢ 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) ⋯)
have 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) sorry)
    (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))))
Tactic: ext