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
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).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).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 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 })

Tactic:
dsimp [P, Q, t, 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).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).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).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).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).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).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:
dsimp
-- 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 : G.map i ≫ G.map s = G.map i ≫ G.map t
⊢ Fork (G.map s) (G.map t)

Tactic:
apply Fork.ofι (G.map i)

Premises used: CategoryTheory.Limits.Fork.ofι, 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
rw : G.map (i ≫ s) = G.map (i ≫ t)
⊢ G.map i ≫ G.map s = G.map i ≫ G.map t

Tactic:
rw [← G.map_comp, ← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : i ≫ s = i ≫ t
⊢ G.map (i ≫ s) = G.map (i ≫ t)

Tactic:
apply congrArg G.map

Premises used: congrArg, 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
⊢ i ≫ s = i ≫ t

Tactic:
equalizer.condition s t

Premises used: CategoryTheory.Limits.equalizer.condition
-- 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
⊢ i ≫ s = i ≫ t

Tactic:
exact equalizer.condition s t

Premises used: CategoryTheory.Limits.equalizer.condition
-- 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
⊢ 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))

Tactic:
apply isLimitOfHasProductOfPreservesLimit

Premises used: CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit
-- 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
⊢ 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))

Tactic:
apply isLimitOfHasProductOfPreservesLimit

Premises used: CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit
-- 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
l : IsLimit (Fork.ofι i ⋯)
w : i ≫ s = i ≫ t
⊢ IsLimit (F := parallelPair (G.map s) (G.map t)) (Fork.ofι (G.map i) ⋯ : Fork (G.map s) (G.map t))

Tactic:
apply isLimitForkMapOfIsLimit

Premises used: CategoryTheory.Limits.isLimitForkMapOfIsLimit
-- 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
refine :
  ∀ (j : J),
    NatTrans.app
        (Cone.π
          (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) ⋯)))
        j =
      Iso.hom
          (Iso.refl
            (Cone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
              (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)))).π.app j
⊢ 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)))

Tactic:
refine Cone.ext (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- 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
j : J
dsimp :
  G.map (equalizer.ι s t) ≫ G.map (Pi.π K.obj j) =
    𝟙 (G.obj (equalizer s t)) ≫ G.map (equalizer.ι s t ≫ limit.π (Discrete.functor K.obj) { as := j : Discrete J })
⊢ NatTrans.app
      (Cone.π
        (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) ⋯)))
      j =
    Iso.hom
        (Iso.refl
          (Cone.pt.{w, v₂, w, u₂} (J := J) (F := K ⋙ G)
            (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)))).π.app j

Tactic:
dsimp [P, Q, I, i]