-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
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
apply :
  Cofan.{w, v₂, u₂} (C := D) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
apply₁ : Cofan.{w, v₂, u₂} (K ⋙ G).obj
apply₂ apply₃ :
  Cocone.pt.{w, v₂, w, u₂} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
      Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
      (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)) ⟶
    Cocone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
      (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f))
apply₄ :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq.{v₂ + 1} (α :=
      Functor.obj.{w, v₂, w, u₂}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        Cocone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
          (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)))
      (NatTrans.app
          (Cocone.ι
            (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)))
          { as := f } ≫
        G.map s)
      ((K ⋙ G).map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        NatTrans.app (Cocone.ι (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)))
          { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
apply₅ :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq.{v₂ + 1} (α :=
      Functor.obj.{w, v₂, w, u₂}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        Cocone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
          (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)))
      (NatTrans.app
          (Cocone.ι
            (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)))
          { as := f } ≫
        G.map t)
      (NatTrans.app (Cocone.ι (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
apply₆ : Cofork (G.map s) (G.map t)
apply₇ :
  IsColimit.{w, v₂, w, u₂} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
    Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
    (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))
apply₈ :
  IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
    (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f))
apply₉ : IsColimit (F := parallelPair (G.map s) (G.map t)) (Cofork.ofπ (G.map i) ⋯ : Cofork (G.map s) (G.map t))
apply₁₀ :
  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)))
⊢ IsColimit (G.mapCocone (buildColimit s t ⋯ ⋯ (colimit.cocone (parallelPair s t))))

Tactic:
apply IsColimit.ofIsoColimit (buildIsColimit _ _ _ _ _ _ _) _

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit