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 : 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 : (p : J × J) × (p.1 ⟶ p.2)
⊢ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 ⟶ Q

Tactic:
apply Sigma.ι _ j

Premises used: CategoryTheory.Limits.Sigma.ι
-- 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
⊢ Cofan.{w, v₂, u₂} (K ⋙ G).obj

Tactic:
exact Cofan.mk _ fun f => G.map (Sigma.ι _ f)

Premises used: CategoryTheory.Limits.Sigma.ι, CategoryTheory.Functor.map, CategoryTheory.Limits.Cofan.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 : 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
⊢ 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))

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 : 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
⊢ 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))

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 : 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
f : (p : J × J) × (p.1 ⟶ p.2)
simp :
  Eq (α := G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map
        (NatTrans.app
          (Cocone.ι
            (Cofan.mk (sigmaObj.{w, v, u} K.obj) 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 }))
          { as := f }) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map
        (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫ Sigma.ι K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
⊢ Eq (α := G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (CategoryStruct.comp (Y :=
        G.obj
          (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))
        (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) f))
        (G.map
          (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 })) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) ≫
        G.map (Sigma.ι K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))

Tactic:
simp only [← G.map_comp, colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc, 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 : 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
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α := G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map
        (NatTrans.app
          (Cocone.ι
            (Cofan.mk (sigmaObj.{w, v, u} K.obj) 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 }))
          { as := f }) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map
        (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫ Sigma.ι K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))

Tactic:
congr
-- 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
f : (p : J × J) × (p.1 ⟶ p.2)
dsimp :
  Eq (α := G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (CategoryStruct.comp (Y :=
        G.obj
          (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))
        (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) f))
        (G.map
          (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 })) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map (Sigma.ι K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
⊢ 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 })

Tactic:
dsimp [P, Q, t, Cofan.mk]

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

Tactic:
simp only [← G.map_comp, colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc, 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 : 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
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α := G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map
        (NatTrans.app
          (Cocone.ι
            (Cofan.mk (sigmaObj.{w, v, u} K.obj) 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 }))
          { as := f }) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))
    (G.map (Sigma.ι K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) :
      G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ⟶ G.obj (sigmaObj.{w, v, u} K.obj))

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 : 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
refine : G.map s ≫ G.map i = G.map t ≫ G.map i
⊢ Cofork (G.map s) (G.map t)

Tactic:
refine Cofork.ofπ (G.map i) ?_

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

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

Tactic:
apply congrArg G.map

Premises used: congrArg, CategoryTheory.Functor.map