-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (j : J),
    CategoryStruct.comp (Y :=
        Cocone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
          (buildColimit (c₁ :=
            Cofan.mk (G.obj Q) fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦
              G.map
                (Sigma.ι.{w, v, u} (C := C)
                  (fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j))
            (c₂ := Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)) (G.map s)
            (G.map t) ⋯ ⋯ (Cofork.ofπ (G.map i) ⋯)))
        (NatTrans.app
            (Cocone.ι
              (buildColimit (c₁ :=
                Cofan.mk (G.obj Q) fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦
                  G.map
                    (Sigma.ι.{w, v, u} (C := C)
                      (fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j))
                (c₂ := Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)) (G.map s)
                (G.map t) ⋯ ⋯ (Cofork.ofπ (G.map i) ⋯)))
            j :
          (K ⋙ G).obj j ⟶
            Functor.obj.{w, v₂, w, u₂}
              (Functor.obj (Functor.const J)
                (Cocone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
                  (buildColimit (c₁ :=
                    Cofan.mk (G.obj Q) fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦
                      G.map
                        (Sigma.ι.{w, v, u} (C := C)
                          (fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j))
                    (c₂ := Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)) (G.map s)
                    (G.map t) ⋯ ⋯ (Cofork.ofπ (G.map i) ⋯))))
              j)
        (Iso.hom
          (Iso.refl
            (Cocone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
              (buildColimit (c₁ :=
                Cofan.mk (G.obj Q) fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦
                  G.map
                    (Sigma.ι.{w, v, u} (C := C)
                      (fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j))
                (c₂ := Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)) (G.map s)
                (G.map t) ⋯ ⋯ (Cofork.ofπ (G.map i) ⋯))))) =
      (G.mapCocone (buildColimit s t ⋯ ⋯ (colimit.cocone (parallelPair s t)))).ι.app j
have dsimp : ∀ (j : J),
  (G.map (Sigma.ι K.obj j) ≫ G.map (coequalizer.π s t)) ≫ 𝟙 (G.obj I) =
    G.map (colimit.ι (Discrete.functor K.obj) { as := j } ≫ coequalizer.π s t)
Tactic: dsimp [i]