awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
A : C
hlp : Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (prod.lift (𝟙 A) 0) prod.snd) 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)
    (fun (s : Fork.{v, u} (C := C) (X := Limits.prod.{v, u} A A) prod.snd 0) ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
htt : t = 0
hf :
  Eq (α := Limits.prod.{v, u} A A ⟶ Z) (prod.snd ≫ t)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A)) (cokernel.π (diag A)) 0)
hf₁ :
  Eq.{v + 1} (α := Limits.prod.{v, u} A A ⟶ Z) (prod.snd ≫ 0)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A)) (cokernel.π (diag A)) 0)
hf₂ :
  Eq.{v + 1} (α := Limits.prod.{v, u} A A ⟶ Z) 0
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A)) (cokernel.π (diag A)) 0)
hf₃ hf₄ : Eq.{v + 1} (α := Limits.prod.{v, u} A A ⟶ Z) 0 0
⊢ cokernel.π (diag A) ≫ z =
    CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A)) (cokernel.π (diag A)) 0

Tactic:
rw [← ht, htt, comp_zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
A : C
⊢ IsIso.{v, u} (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} A A) (diag A)) (r A)

Tactic:
isIso_of_mono_of_epi _

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X : C
rw :
  Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) 0 (inv (r X))) 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ X) 0 0
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (diag X : X ⟶ Limits.prod.{v, u} X X)
      (σ : Limits.prod.{v, u} X X ⟶ X))
    0

Tactic:
rw [cokernel.condition_assoc, zero_comp]

Premises used: CategoryTheory.Limits.cokernel.condition_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X : C
rw :
  Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} X X) (diag X))
      (prod.lift (𝟙 X) 0 ≫ cokernel.π (diag X)) (inv (r X)))
    (𝟙 X)
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ : Limits.prod.{v, u} X X ⟶ X))
    (𝟙 X)

Tactic:
rw [← Category.assoc, IsIso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ Limits.prod.{v, u} Y Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0) (prod.map f f)) (f ≫ prod.lift (𝟙 Y) 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X : C
rw :
  Eq.{v + 1} (α := Limits.prod.{v, u} X X ⟶ X)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) (cokernel.π (diag X))
        (Iso.inv (asIso (r X))) :
      Limits.prod.{v, u} X X ⟶ X)
    (σ : Limits.prod.{v, u} X X ⟶ X)
rw₁ rw₂ :
  Eq.{v + 1} (α := Limits.prod.{v, u} X X ⟶ X)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) (cokernel.π (diag X))
        (inv (r X)) :
      Limits.prod.{v, u} X X ⟶ X)
    (σ : Limits.prod.{v, u} X X ⟶ X)
⊢ Eq.{v + 1} (α := Limits.prod.{v, u} X X ⟶ X)
    (CategoryStruct.comp (Y := cokernel.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) (cokernel.π (diag X))
        (Iso.hom (Iso.symm (asIso (r X)))) :
      Limits.prod.{v, u} X X ⟶ X)
    (σ : Limits.prod.{v, u} X X ⟶ X)

Tactic:
rw [Iso.symm_hom, asIso_inv]

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.asIso_inv
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
rw :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (diag Y : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ : Eq (α := X ⟶ Y) (f ≫ 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (diag X)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
    0

Tactic:
rw [prod.diag_map_assoc, diag_σ, comp_zero]

Premises used: CategoryTheory.NonPreadditiveAbelian.diag_σ, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.prod.diag_map_assoc
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
obtain :
  ∀
    (g :
      Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
          (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
        Y)
    (hg :
      Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
            (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
          Limits.prod.{v, u} X X ⟶ Y)),
    Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
          (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
        Limits.prod.{v, u} X X ⟶ Y)
⊢ Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)

Tactic:
obtain ⟨g, hg⟩ :=
    CokernelCofork.IsColimit.desc' isColimitσ (Limits.prod.map f f ≫ σ) (by
      rw [prod.diag_map_assoc, diag_σ, comp_zero])

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc', CategoryTheory.NonPreadditiveAbelian.isColimitσ, CategoryTheory.NonPreadditiveAbelian.σ, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.prod.map
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
hfg : f = g
rw :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y)
    (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
rw₁ : Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y) (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
rw₂ rw₃ : Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
⊢ Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)

Tactic:
rw [← hg, Cofork.π_ofπ, hfg]

Premises used: CategoryTheory.Limits.Cofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
suffices : f = g
⊢ Eq (α := Limits.prod.{v, u} X X ⟶ Y) (σ ≫ f : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)

Tactic:
suffices hfg : f = g by rw [← hg, Cofork.π_ofπ, hfg]
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw : f = f ≫ 𝟙 Y
rw₁ rw₂ : f = f
⊢ f =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)

Tactic:
rw [lift_σ, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NonPreadditiveAbelian.lift_σ
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw rw₁ :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)
⊢ f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y))

Tactic:
rw [lift_map_assoc]

Premises used: CategoryTheory.NonPreadditiveAbelian.lift_map_assoc
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
rw₁ rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)

Tactic:
rw [← hg, CokernelCofork.π_ofπ]

Premises used: CategoryTheory.Limits.CokernelCofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
        (σ : Limits.prod.{v, u} X X ⟶ X) ≫
      g =
    g
rw₁ : 𝟙 X ≫ g = g
rw₂ rw₃ : g = g
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    g

Tactic:
rw [← Category.assoc, lift_σ, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NonPreadditiveAbelian.lift_σ, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
f₁ :
  f =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)
f₂ :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y))
f₃ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
f₄ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    g
⊢ f = g

Tactic:
calc
    f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
    _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
    _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
    _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.NonPreadditiveAbelian.σ, OfNat.ofNat, CategoryTheory.Limits.prod.lift, CategoryTheory.Limits.prod.map
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
⊢ a - b =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a b : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
⊢ a + b = a - -b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ -a = 0 - a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
⊢ a - 0 = a

Tactic:
rw [sub_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : prod.lift a 0
a₂ : (σ : Limits.prod.{v, u} Y Y ⟶ Y)
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a
congr : 0
| prod.lift a 0

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a ≫ 𝟙 Y
| a

Tactic:
rw [← Category.comp_id a]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ Eq (α := X ⟶ Y) 0 (a ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw : a ≫ 0
| 0

Tactic:
rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| 0

Tactic:
case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a ≫ 𝟙 Y
a₂ : (σ : Limits.prod.{v, u} Y Y ⟶ Y)
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)

Tactic:
congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
conv_lhs :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a

Tactic:
conv_lhs =>
    congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
rw₁ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
rw₂ : a ≫ 𝟙 Y = a
rw₃ rw₄ : a = a
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a

Tactic:
rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.prod.comp_lift, CategoryTheory.NonPreadditiveAbelian.lift_σ
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) (𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₃ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) (𝟙 Y) : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₄ : Eq (α := X ⟶ Y) (a ≫ 0) 0
rw₅ rw₆ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ a - a = 0

Tactic:
rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NonPreadditiveAbelian.diag_σ, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.prod.comp_lift, CategoryTheory.NonPreadditiveAbelian.sub_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
simp :
  Eq (α := X ⟶ Limits.prod.{v, u} Y Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (prod.lift (prod.lift a b) (prod.lift c d) :
        X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (σ : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y))
    (prod.lift
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y))
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
⊢ HSub.hSub (α := X ⟶ Limits.prod.{v, u} Y Y) (prod.lift a b) (prod.lift c d) = prod.lift (a - c) (b - d)

Tactic:
simp only [sub_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_def