awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
inst_2 : HasLimit.{w, w, v, u} (Discrete.functor F.obj)
inst_3 :
  HasLimit.{w, w, v, u} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (C := C)
    (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
inst_4 : HasEqualizers.{v, u} C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq.{v + 1} (α :=
      Cone.pt.{w, v, w, u} (F := Discrete.functor F.obj) (limit.cone (Discrete.functor F.obj)) ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (CategoryStruct.comp (Y :=
        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)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          (limit.cone
            (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
        (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
          limit.π (Discrete.functor F.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
        (NatTrans.app
          (Cone.π
            (limit.cone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
          { as := f }))
      (NatTrans.app (Cone.π (limit.cone (Discrete.functor F.obj))) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
inst_2 : HasLimit.{w, w, v, u} (Discrete.functor F.obj)
inst_3 :
  HasLimit.{w, w, v, u} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (C := C)
    (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
inst_4 : HasEqualizers.{v, u} C
⊢ HasLimit F

Tactic:
HasLimit.mk (limitConeOfEqualizerAndProduct F)

Premises used: CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.limitConeOfEqualizerAndProduct
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : HasLimitsOfSize.{w, w, v, u} C
F : Functor.{w, v, w, u} J C
⊢ Mono (X := limit F) (Y := piObj.{w, v, u} fun (j : J) ↦ F.obj j)
    (limitSubobjectProduct F : limit F ⟶ piObj.{w, v, u} fun (j : J) ↦ F.obj j)

Tactic:
mono_comp _ _

Premises used: CategoryTheory.mono_comp, CategoryTheory.Limits.limitSubobjectProduct
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{w, v, u} C
inst_2 : HasEqualizers.{v, u} C
⊢ HasLimitsOfSize.{w, w, v, u} C

Tactic:
{ has_limits_of_shape :=
    fun _ _ => { has_limit := fun F => hasLimit_of_equalizer_and_product F } }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.HasLimitsOfSize.mk, CategoryTheory.Limits.hasLimit_of_equalizer_and_product
-- 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
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫
        NatTrans.app
          (Cone.π
            (limit.cone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } =
      NatTrans.app (Cone.π (limit.cone (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))

Tactic:
simp [P, s]
-- 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
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    t ≫
        NatTrans.app
          (Cone.π
            (limit.cone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } =
      NatTrans.app (Cone.π (limit.cone (Discrete.functor K.obj))) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }

Tactic:
simp [P, t]
-- 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 : IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))
⊢ PreservesLimit K G

Tactic:
apply preservesLimit_of_preserves_limit_cone
        (buildIsLimit s t (by simp [P, s]) (by simp [P, t]) (limit.isLimit _)
          (limit.isLimit _) (limit.isLimit _))

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- 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
⊢ Fan.{w, v₂, u₂} (K ⋙ G).obj

Tactic:
exact Fan.mk _ fun j => G.map (Pi.π _ j)

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.Pi.π, CategoryTheory.Functor.map
-- 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
⊢ 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

Tactic:
exact Fan.mk (G.obj Q) fun f => G.map (Pi.π _ f)

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.Pi.π, Sigma.fst, CategoryTheory.Functor.map, Prod.snd, CategoryTheory.Functor.obj
-- 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
⊢ 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))

Tactic:
apply G.map s

Premises used: CategoryTheory.Functor.map
-- 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
⊢ 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))

Tactic:
apply G.map t

Premises used: CategoryTheory.Functor.map
-- 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
f : (p : J × J) × (p.1 ⟶ p.2)
dsimp :
  Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (CategoryStruct.comp (Y :=
        G.obj (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))
        (G.map
          (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))))
        (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.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ≫
        G.map (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).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)))

Tactic:
dsimp [P, Q, s, Fan.mk]

Premises used: CategoryTheory.Limits.Fan.mk
-- 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
f : (p : J × J) × (p.1 ⟶ p.2)
simp :
  Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map
        (NatTrans.app
          (Cone.π
            (Fan.mk (piObj.{w, v, u} K.obj) 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))))
          { as := f }) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 ≫ K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
⊢ Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (CategoryStruct.comp (Y :=
        G.obj (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))
        (G.map
          (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))))
        (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.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ≫
        G.map (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))

Tactic:
simp only [← G.map_comp, limit.lift_π]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limit.lift_π
-- 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
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map
        (NatTrans.app
          (Cone.π
            (Fan.mk (piObj.{w, v, u} K.obj) 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))))
          { as := f }) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 ≫ K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))

Tactic:
congr