-- 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 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{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 := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
apply : Fan.{w, v₂, u₂} (K ⋙ G).obj
apply₁ :
  Fan.{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).2
apply₂ apply₃ :
  Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
      (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
    Cone.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).2)
      (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
        G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
apply₄ :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
          (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
        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).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (G.map s ≫
        NatTrans.app
          (Cone.π
            (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
              G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)))
          { as := f })
      (NatTrans.app (Cone.π (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)))
          { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
        (K ⋙ G).map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)))
apply₅ :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
          (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
        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).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (G.map t ≫
        NatTrans.app
          (Cone.π
            (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
              G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)))
          { as := f })
      (NatTrans.app (Cone.π (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
apply₆ : Fork (G.map s) (G.map t)
apply₇ :
  IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
    (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j))
apply₈ :
  IsLimit.{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).2)
    (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
      G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
apply₉ : IsLimit (F := parallelPair (G.map s) (G.map t)) (Fork.ofι (G.map i) ⋯ : Fork (G.map s) (G.map t))
apply₁₀ :
  buildLimit (c₁ := Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) (c₂ :=
      Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
        G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
      (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯) ≅
    G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))

Tactic:
apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _

Premises used: CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit, CategoryTheory.Limits.IsLimit.ofIsoLimit