awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
T : C
f g : (F.obj c₁.pt).obj c₂.pt ⟶ T
h :
  (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ f =
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ g
⊢ f = g

Tactic:
Cofork.IsColimit.hom_ext (mapIsColimit _ hc₂ (F.obj c₁.pt))
    (Cofork.IsColimit.hom_ext (mapIsColimit _ hc₁ (F.flip.obj Y₂)) h)

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Functor.flip, CategoryTheory.Limits.CokernelCofork.mapIsColimit, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
⊢ CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inl
      (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s) =
    CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inl 0

Tactic:
have := coprod.inl ≫= s.condition
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
this :
  CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inl
      (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s) =
    CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inl 0
⊢ (F.map f₁).app Y₂ ≫ Cofork.π s = 0

Tactic:
rw [coprod.inl_desc_assoc, comp_zero] at this

Premises used: CategoryTheory.Limits.coprod.inl_desc_assoc, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
this : (F.map f₁).app Y₂ ≫ Cofork.π s = 0
rwa rwa₁ rwa₂ rwa₃ : (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0
⊢ (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
rwa [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
obtain :
  ∀ (l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt)
    (hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s),
    ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt),
      (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s
⊢ ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt),
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s

Tactic:
obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' (mapIsColimit _ hc₁ (F.flip.obj Y₂)) s.π (by
    have := coprod.inl ≫= s.condition
    rw [coprod.inl_desc_assoc, comp_zero] at this
    rwa [zero_comp])

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.Cofork.IsColimit.desc', CategoryTheory.Limits.CokernelCofork.mapIsColimit, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
⊢ CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inr
      (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s) =
    CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inr 0

Tactic:
have := coprod.inr ≫= s.condition
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this :
  CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inr
      (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s) =
    CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inr 0
⊢ (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = 0

Tactic:
rw [coprod.inr_desc_assoc, ← dsimp% hl, NatTrans.naturality_assoc, comp_zero] at this

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.coprod.inr_desc_assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = 0
apply :
  Cofork.π (c₁.map (F.flip.obj X₂)) ≫ (F.obj c₁.pt).map f₂ ≫ l =
    CategoryStruct.comp (Y := Cocone.pt (F := parallelPair ((F.flip.obj X₂).map f₁) 0) (c₁.map (F.flip.obj X₂)))
      (Cofork.π (c₁.map (F.flip.obj X₂))) (0 ≫ l)
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l

Tactic:
apply Cofork.IsColimit.hom_ext (mapIsColimit _ hc₁ (F.flip.obj X₂))

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.Functor.flip, CategoryTheory.Limits.CokernelCofork.mapIsColimit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = 0
rwa :
  Eq (α := (F.flip.obj X₂).obj Y₁ ⟶ s.pt) (Cofork.π (c₁.map (F.flip.obj X₂)) ≫ (F.obj c₁.pt).map f₂ ≫ l)
    (CategoryStruct.comp (Y := Cocone.pt (F := parallelPair ((F.flip.obj X₂).map f₁) 0) (c₁.map (F.flip.obj X₂)))
      (Cofork.π (c₁.map (F.flip.obj X₂))) 0)
rwa₁ rwa₂ rwa₃ rwa₄ :
  Eq (α := (F.flip.obj X₂).obj Y₁ ⟶ s.pt) (Cofork.π (c₁.map (F.flip.obj X₂)) ≫ (F.obj c₁.pt).map f₂ ≫ l) 0
⊢ Cofork.π (c₁.map (F.flip.obj X₂)) ≫ (F.obj c₁.pt).map f₂ ≫ l =
    CategoryStruct.comp (Y := Cocone.pt (F := parallelPair ((F.flip.obj X₂).map f₁) 0) (c₁.map (F.flip.obj X₂)))
      (Cofork.π (c₁.map (F.flip.obj X₂))) (0 ≫ l)

Tactic:
rwa [zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
obtain :
  ∀ (l' : Cocone.pt (F := parallelPair ((F.obj c₁.pt).map f₂) 0) (c₂.map (F.obj c₁.pt)) ⟶ s.pt)
    (hl' : Cofork.π (c₂.map (F.obj c₁.pt)) ≫ l' = l),
    ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt),
      (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s
⊢ ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt),
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s

Tactic:
obtain ⟨l', hl'⟩ := Cofork.IsColimit.desc' (mapIsColimit _ hc₂ (F.obj c₁.pt)) l (by
    have := coprod.inr ≫= s.condition
    rw [coprod.inr_desc_assoc, ← dsimp% hl, NatTrans.naturality_assoc, comp_zero] at this
    apply Cofork.IsColimit.hom_ext (mapIsColimit _ hc₁ (F.flip.obj X₂))
    rwa [zero_comp, comp_zero])

Premises used: CategoryTheory.Limits.Cofork.IsColimit.desc', CategoryTheory.Limits.CokernelCofork.mapIsColimit, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  CokernelCofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : Cocone.pt (F := parallelPair ((F.flip.obj Y₂).map f₁) 0) (c₁.map (F.flip.obj Y₂)) ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
l' : Cocone.pt (F := parallelPair ((F.obj c₁.pt).map f₂) 0) (c₂.map (F.obj c₁.pt)) ⟶ s.pt
hl' : Cofork.π (c₂.map (F.obj c₁.pt)) ≫ l' = l
⊢ ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt),
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s

Tactic:
exact ⟨l', by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  Cofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F :=
        parallelPair (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
          (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0)
        (c₁.mapBifunctor c₂ F))
      (Cofork.π (c₁.mapBifunctor c₂ F))
      ((fun
            (s :
              Cofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
                (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0) ↦
          ⋯.choose (p := fun (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt) ↦
            (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = s.π))
        s) =
    s.π

Tactic:
simpa using (exists_desc hc₁ hc₂ F s).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  Cofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m :
  Cocone.pt (F :=
      parallelPair (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
        (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0)
      (c₁.mapBifunctor c₂ F) ⟶
    s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
dsimp :
  (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫
      (F.obj c₁.pt).map (Cofork.π c₂) ≫
        ⋯.choose (p := fun (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt) ↦
          (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = s.π)
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫
      (F.obj c₁.pt).map (Cofork.π c₂) ≫
        (fun
              (s :
                Cofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
                  (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0) ↦
            ⋯.choose (p := fun (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt) ↦
              (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = s.π))
          s

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
Goal:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C
inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms
inst_7 : F.PreservesZeroMorphisms
inst_8 : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst_9 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst_10 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst_11 : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s :
  Cofork (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m :
  Cocone.pt (F :=
      parallelPair (X := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂))
        (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0)
      (c₁.mapBifunctor c₂ F) ⟶
    s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
rw : (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m = s.π
rw₁ :
  (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    ((F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂)) ≫ m
rw₂ rw₃ :
  (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫
      (F.obj c₁.pt).map (Cofork.π c₂) ≫
        ⋯.choose (p := fun (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt) ↦
          (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = s.π)

Tactic:
rw [(exists_desc hc₁ hc₂ F s).choose_spec, ← dsimp% hm, Category.assoc]

Premises used: CategoryTheory.Category.assoc, Exists.choose_spec, CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
⊢ CreatesLimitsOfShape (Discrete x) F.op

Tactic:
apply +allowSynthFailures createsLimitsOfShapeOp

Premises used: CategoryTheory.Limits.createsLimitsOfShapeOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesFiniteCoproducts F
x : Type
x_1 : Fintype x
⊢ CreatesColimitsOfShape (Discrete x)ᵒᵖ F

Tactic:
exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm, CategoryTheory.createsColimitsOfShapeOfEquiv