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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
simp :
  Eq (α :=
    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).1)
        { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
      W)
    ((c₁.ι.app { as := f } ≫ t) ≫ h) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h)
⊢ c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ h =
    c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
⊢ Eq (α :=
    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).1)
        { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
      W)
    ((c₁.ι.app { as := f } ≫ t) ≫ h) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h)

Tactic:
apply eq_whisker (ht f)

Premises used: CategoryTheory.eq_whisker
-- 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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ h =
      c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h

Tactic:
have reassoced_t (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ t ≫ h = c₂.ι.app ⟨f.fst.fst⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (ht f)
-- 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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
reassoced_t :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ h =
      c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (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).1)
        { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (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).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (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).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)

Tactic:
simp [reassoced_s, reassoced_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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s_1 t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s_1 =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s_1 t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
s : Cocone F
j : J
⊢ (buildColimit s_1 t hs ht i).ι.app j ≫
      hi.desc
        (Cofork.ofπ (P := s.1)
          (t₂.desc (Cofan.mk s.1 fun (j : J) ↦ s.ι.app j) :
            c₂.pt ⟶
              Cocone.pt.{w, v, w, u} (J := Discrete J) (F := Discrete.functor F.obj)
                (Cofan.mk s.1 fun (j : J) ↦ s.ι.app j))
          ⋯) =
    s.ι.app j

Tactic:
simp
-- 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
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      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).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
m : (buildColimit s t hs ht i).pt ⟶ q.pt
w : ∀ (j : J), (buildColimit s t hs ht i).ι.app j ≫ m = q.ι.app j
j : Discrete J
⊢ c₂.ι.app j ≫ i.π ≫ m =
    c₂.ι.app j ≫
      i.π ≫
        hi.desc
          (Cofork.ofπ (P := q.1)
            (t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
              c₂.pt ⟶
                Cocone.pt.{w, v, w, u} (J := Discrete J) (F := Discrete.functor F.obj)
                  (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j))
            ⋯)

Tactic:
simpa using w j.1

Premises used: CategoryTheory.Discrete.as
-- 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
F : Functor.{w, v, w, u} J C
inst_3 : HasColimit.{w, w, v, u} (Discrete.functor F.obj)
inst_4 :
  HasColimit.{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).1)
inst_5 : HasCoequalizers.{v, u} C
⊢ ∀ (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)) ↦ F.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} (F := Discrete.functor F.obj) (colimit.cocone (Discrete.functor F.obj)))
      (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Discrete ((p : J × J) × (p.1 ⟶ p.2))))
            (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)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
              (colimit.cocone
                (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                  F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1))))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        (NatTrans.app
          (Cocone.ι
            (colimit.cocone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)))
          { as := f })
        (Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
          F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
            colimit.ι (Discrete.functor F.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }))
      (F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        NatTrans.app (Cocone.ι (colimit.cocone (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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
inst_3 : HasColimit.{w, w, v, u} (Discrete.functor F.obj)
inst_4 :
  HasColimit.{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).1)
inst_5 : HasCoequalizers.{v, u} C
⊢ ∀ (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)) ↦ F.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} (F := Discrete.functor F.obj) (colimit.cocone (Discrete.functor F.obj)))
      (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Discrete ((p : J × J) × (p.1 ⟶ p.2))))
            (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)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
              (colimit.cocone
                (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                  F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1))))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        (NatTrans.app
          (Cocone.ι
            (colimit.cocone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)))
          { as := f })
        (Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
          colimit.ι (Discrete.functor F.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }))
      (NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor F.obj)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })

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 : HasColimit.{w, w, v, u} (Discrete.functor F.obj)
inst_3 :
  HasColimit.{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).1)
inst_4 : HasCoequalizers.{v, u} C
⊢ HasColimit F

Tactic:
HasColimit.mk (colimitCoconeOfCoequalizerAndCoproduct F)

Premises used: CategoryTheory.Limits.colimitCoconeOfCoequalizerAndCoproduct, CategoryTheory.Limits.HasColimit.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 : HasColimitsOfSize.{w, w, v, u} C
F : Functor.{w, v, w, u} J C
⊢ Epi (X := sigmaObj.{w, v, u} fun (j : J) ↦ F.obj j) (Y := colimit F)
    (colimitQuotientCoproduct F : (sigmaObj.{w, v, u} fun (j : J) ↦ F.obj j) ⟶ colimit F)

Tactic:
epi_comp _ _

Premises used: CategoryTheory.epi_comp, CategoryTheory.Limits.colimitQuotientCoproduct
-- 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)),
    NatTrans.app
          (Cocone.ι
            (colimit.cocone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
        s =
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor K.obj)))
          { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).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 : 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)),
    NatTrans.app
          (Cocone.ι
            (colimit.cocone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)))
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
        t =
      NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor K.obj)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }

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 : 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 : IsColimit (G.mapCocone (buildColimit s t ⋯ ⋯ (colimit.cocone (parallelPair s t))))
⊢ PreservesColimit K G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone
        (buildIsColimit s t (by simp [P, s]) (by simp [P, t]) (colimit.isColimit _)
          (colimit.isColimit _) (colimit.isColimit _))

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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 : (j : (p : J × J) × (p.1 ⟶ p.2)) → K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 ⟶ Q
⊢ 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

Tactic:
refine Cofan.mk (G.obj Q) fun j => G.map ?_

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.Cofan.mk, CategoryTheory.Functor.obj