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
j : J
⊢ 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 })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasEqualizers.{v, u} C
inst_3 : HasFiniteProducts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape WalkingParallelPair G
inst_5 : PreservesFiniteProducts G
J : Type
inst_6 : SmallCategory J
inst_7 : FinCategory J
⊢ PreservesLimitsOfShape J G

Tactic:
apply preservesLimit_of_preservesEqualizers_and_product

Premises used: CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
⊢ HasFiniteLimits.{v, u} C

Tactic:
@hasFiniteLimits_of_hasEqualizers_and_finite_products C _
    (@hasFiniteProducts_of_has_binary_and_terminal C _
      (hasBinaryProducts_of_hasTerminal_and_pullbacks C) inferInstance)
    (@hasEqualizers_of_hasPullbacks_and_binary_products C _
      (hasBinaryProducts_of_hasTerminal_and_pullbacks C) inferInstance)

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
⊢ HasFiniteLimits.{v, u} C

Tactic:
have : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits.{v, u} C
⊢ PreservesLimitsOfShape (Discrete WalkingPair) G

Tactic:
have : PreservesLimitsOfShape (Discrete WalkingPair) G :=
    preservesBinaryProducts_of_preservesTerminal_and_pullbacks G
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesLimitsOfShape WalkingParallelPair G

Tactic:
have : PreservesLimitsOfShape WalkingParallelPair G :=
    preservesEqualizers_of_preservesPullbacks_and_binaryProducts G
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this_2 : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteProducts G

Tactic:
have : PreservesFiniteProducts G := .of_preserves_binary_and_terminal _
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this_2 : PreservesLimitsOfShape (Discrete WalkingPair) G
this_3 : PreservesLimitsOfShape WalkingParallelPair G
this : PreservesFiniteProducts G
⊢ PreservesFiniteLimits G

Tactic:
preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts G

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasTerminal.{v, u} C
inst_3 : HasPullbacks.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
this_1 : HasFiniteLimits.{v, u} C
this_2 : PreservesLimitsOfShape (Discrete WalkingPair) G
this_3 : PreservesLimitsOfShape WalkingParallelPair G
this : PreservesFiniteProducts G
⊢ PreservesFiniteLimits G

Tactic:
exact preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts G

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts
-- 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
j₁ j₂ : J
f : j₁ ⟶ j₂
dsimp : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π =
    (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ Functor.map (Functor.obj (Functor.const J) i.pt) f

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
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
j₁ j₂ : J
f_1 : j₁ ⟶ j₂
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

Tactic:
simp only [← Category.assoc, eq_whisker (hs f)]

Premises used: CategoryTheory.Category.assoc, 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
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ ∀ (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

Tactic:
have reassoced (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} {h : _ ⟶ W} :
          c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by
            simp only [← Category.assoc, eq_whisker (hs 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
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (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
rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
rw₁ :
  c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
      s ≫ i.π =
    c₂.ι.app { as := j₁ } ≫ i.π
rw₂ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    (c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t ≫ i.π :
      Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
          (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 := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
        i.pt)
    (c₂.ι.app { as := j₁ } ≫ i.π)
rw₃ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    ((c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t) ≫ i.π :
      Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
          (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 := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
        i.pt)
    (c₂.ι.app { as := j₁ } ≫ i.π)
rw₄ rw₅ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    (c₂.ι.app
        {
          as :=
            (Sigma.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2)
                (Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f)).1 } ≫
      i.π)
    (c₂.ι.app { as := j₁ } ≫ i.π)
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt

Tactic:
rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]

Premises used: CategoryTheory.Category.assoc, Prod.mk, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cofork.condition, Sigma.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
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
refine_1 : c₂.pt ⟶ q.1
refine_2 :
  Eq (α := c₁.pt ⟶ q.1) (s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
    (t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
⊢ (buildColimit s t hs ht i).pt ⟶ q.pt

Tactic:
refine hi.desc (Cofork.ofπ ?_ ?_)

Premises used: CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.IsColimit.desc
-- 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
refine_1 : (j : J) → F.obj j ⟶ q.1
⊢ c₂.pt ⟶ q.1

Tactic:
refine t₂.desc (Cofan.mk _ fun j => ?_)

Premises used: CategoryTheory.Limits.IsColimit.desc, 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
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 : J
⊢ F.obj j ⟶ q.1

Tactic:
apply q.ι.app j

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- 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
refine_2 :
  ∀ (j : Discrete ((p : J × J) × (p.1 ⟶ p.2))),
    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) j)
        q.1)
      (c₁.ι.app j ≫ 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) j)
          q.1)
      (c₁.ι.app j ≫ 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) j)
          q.1)
⊢ Eq (α := c₁.pt ⟶ q.1) (s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
    (t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)

Tactic:
apply t₁.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_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
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 f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
simp :
  (c₁.ι.app { as := f } ≫ 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 : Discrete J }) ≫
      h
⊢ 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

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 f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
⊢ (c₁.ι.app { as := f } ≫ 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 : Discrete J }) ≫
      h

Tactic:
apply eq_whisker (hs 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)
⊢ ∀ (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

Tactic:
have reassoced_s (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (hs f)