awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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 : HasBinaryCoproduct.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
h₁ :
  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₂) ≫
        (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂)) =
    CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inl 0
⊢ Eq (α := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂) ⟶ (F.obj c₁.pt).obj c₂.pt)
    (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫
      (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂))
    0
have h₂ : 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₂) ≫
      (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂)) =
  CategoryStruct.comp (Y := coprod.{v_3, u_3} ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)) coprod.inr 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (hypothesis)
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₂))
⊢ (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s
have 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
Tactic: have := coprod.inl ≫= s.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (hypothesis)
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.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s
have this₁ : (F.map f₁).app Y₂ ≫ Cofork.π s = 0
Tactic: rw [coprod.inl_desc_assoc, comp_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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
⊢ (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s
have rwa : (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0
Tactic: rwa [zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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 : (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
have 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
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])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (hypothesis)
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
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l
have 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
Tactic: have := coprod.inr ≫= s.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (hypothesis)
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.obj c₁.pt).map f₂ ≫ l = 0 ≫ l
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l
have 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)
Tactic: apply Cofork.IsColimit.hom_ext (mapIsColimit _ hc₁ (F.flip.obj X₂))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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
⊢ 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)
have 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)
Tactic: rwa [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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)
⊢ 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)
have 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
Tactic: rwa [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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 : (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
have 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
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])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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.π
⊢ (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.π)
have rw : (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m = s.π
Tactic: rw [(exists_desc hc₁ hc₂ F s).choose_spec, ← dsimp% hm, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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.π
⊢ (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.π)
have 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
Tactic: rw [(exists_desc hc₁ hc₂ F s).choose_spec, ← dsimp% hm, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel (goal)
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
⊢ (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.π)
have 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
Tactic: rw [(exists_desc hc₁ hc₂ F s).choose_spec, ← dsimp% hm, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
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
⊢ CreatesLimitsOfShape (Discrete x) F.op
have inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsLimitsOfShapeOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites (goal)
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
⊢ CreatesLimitsOfShape (Discrete x) F.leftOp
have inst : CreatesColimitsOfShape (Discrete x)ᵒᵖ F
Tactic: apply +allowSynthFailures createsLimitsOfShapeLeftOp