awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₀ :
  Eq (α := X ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
h₁ :
  Eq (α := Y ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr 0)
⊢ Eq (α := biprod.{v, u} X Y ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
    0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₀ :
  Eq (α := X ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (f ≫ biprod.inl)
      (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
h₁ :
  Eq (α := X ⟶ cokernel (f ≫ g))
    (f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
h₂ :
  Eq (α := X ⟶ cokernel (f ≫ g)) (f ≫ g ≫ cokernel.π (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)
h₃ : Eq (α := X ⟶ cokernel (f ≫ g)) (f ≫ g ≫ cokernel.π (f ≫ g)) 0
h₄ : Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) 0
h₅ h₆ : Eq.{v + 1} (α := X ⟶ cokernel (f ≫ g)) 0 0
⊢ Eq (α := X ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl 0)

Tactic:
rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero,
      ← assoc, cokernel.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_desc_assoc, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Limits.biprod.inl_desc
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Y ⟶ cokernel (f ≫ g))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g))
        (biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)))))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono (X := kernel (f ≫ g)) (ι f g)

Tactic:
mono_of_mono_fac (ι_fst f g)

Premises used: CategoryTheory.kernelCokernelCompSequence.ι_fst, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Epi (X := biprod.{v, u} Y Z) (π f g)

Tactic:
epi_of_epi_fac (inr_π f g)

Premises used: CategoryTheory.kernelCokernelCompSequence.inr_π, CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ biprod.{v, u} X Y
hk : k ≫ φ f g = 0
refine_1 : (k ≫ biprod.fst) ≫ f ≫ g = 0
refine_2 : kernel.lift (f ≫ g) (k ≫ biprod.fst) ⋯ ≫ ι f g = k
⊢ { l : A ⟶ kernel (f ≫ g) // l ≫ ι f g = k }

Tactic:
refine ⟨kernel.lift _ (k ≫ biprod.fst) ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ biprod.{v, u} X Y
hk : k ≫ φ f g = 0
refine_1 :
  ∀ (k₁ : A ⟶ X) (k₂ : A ⟶ Y)
    (hk : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ φ f g = 0),
    (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0
⊢ (k ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k

Premises used: CategoryTheory.Limits.biprod.decomp_hom_to, rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
k₂ : A ⟶ Y
hk : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ φ f g = 0
⊢ k₁ ≫ f = k₂ ∧ k₂ ≫ g = 0

Tactic:
simp only [biprod.ext_to_iff, add_comp, assoc, inl_φ, BinaryBicone.inl_fst,
        comp_id, inr_φ_fst, comp_neg, zero_comp, BinaryBicone.inl_snd, comp_zero, φ_snd,
        BinaryBicone.inr_snd_assoc, zero_add, add_neg_eq_zero] at hk

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inl_fst, add_neg_eq_zero, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CategoryTheory.kernelCokernelCompSequence.inl_φ, CategoryTheory.Category.comp_id, zero_add, CategoryTheory.Limits.biprod.ext_to_iff, CategoryTheory.Preadditive.add_comp, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.BinaryBicone.inl_snd, CategoryTheory.Limits.BinaryBicone.inr_snd_assoc, CategoryTheory.kernelCokernelCompSequence.φ_snd, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
k₂ : A ⟶ Y
hk : k₁ ≫ f = k₂ ∧ k₂ ≫ g = 0
refine_1 :
  ∀ (hk : (k₁ ≫ f) ≫ g = 0),
    (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0
⊢ (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
obtain ⟨rfl, hk⟩ := hk

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk : (k₁ ≫ f) ≫ g = 0
⊢ (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ biprod.{v, u} X Y
hk : k ≫ φ f g = 0
refine_2 :
  ∀ (k₁ : A ⟶ X) (k₂ : A ⟶ Y)
    (hk : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ φ f g = 0),
    kernel.lift (f ≫ g) (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ biprod.fst) ⋯ ≫
        ι f g =
      HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr)
⊢ kernel.lift (f ≫ g) (k ≫ biprod.fst) ⋯ ≫ ι f g = k

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k

Premises used: CategoryTheory.Limits.biprod.decomp_hom_to, rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
k₂ : A ⟶ Y
hk_1 : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ φ f g = 0
hk : k₁ ≫ f = k₂ ∧ k₂ ≫ g = 0
refine_2 :
  ∀ (hk : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ φ f g = 0)
    (hk_2 : (k₁ ≫ f) ≫ g = 0),
    kernel.lift (f ≫ g) (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst)
          ⋯ ≫
        ι f g =
      HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr)
⊢ kernel.lift (f ≫ g) (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr) ≫ biprod.fst) ⋯ ≫
      ι f g =
    HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) (k₂ ≫ biprod.inr)

Tactic:
obtain ⟨rfl, hk⟩ := hk

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk_1 : HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ φ f g = 0
hk : (k₁ ≫ f) ≫ g = 0
⊢ kernel.lift (f ≫ g) (HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst)
        ⋯ ≫
      ι f g =
    HAdd.hAdd (α := A ⟶ biprod.{v, u} X Y) (k₁ ≫ biprod.inl) ((k₁ ≫ f) ≫ biprod.inr)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : biprod.{v, u} Y Z ⟶ A
hk : φ f g ≫ k = 0
refine_1 : (f ≫ g) ≫ biprod.inr ≫ k = 0
refine_2 : π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ k) ⋯ = k
⊢ { l : cokernel (f ≫ g) ⟶ A // π f g ≫ l = k }

Tactic:
refine ⟨cokernel.desc _ (biprod.inr ≫ k) ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : biprod.{v, u} Y Z ⟶ A
hk : φ f g ≫ k = 0
refine_1 :
  ∀ (k₁ : Y ⟶ A) (k₂ : Z ⟶ A)
    (hk : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0),
    (f ≫ g) ≫ biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ k = 0

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_from k

Premises used: CategoryTheory.Limits.biprod.decomp_hom_from, rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : Y ⟶ A
k₂ : Z ⟶ A
hk : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0
⊢ f ≫ k₁ = 0 ∧ k₁ = g ≫ k₂

Tactic:
simp only [comp_add, φ_snd_assoc, biprod.ext_from_iff, inl_φ_assoc,
        BinaryBicone.inl_fst_assoc, BinaryBicone.inl_snd_assoc, zero_comp, add_zero, comp_zero,
        inr_φ_fst_assoc, neg_comp, id_comp, BinaryBicone.inr_snd_assoc, neg_add_eq_zero] at hk

Premises used: CategoryTheory.Limits.BinaryBicone.inl_fst_assoc, CategoryTheory.Limits.BinaryBicone.inl_snd_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Limits.zero_comp, CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc, neg_add_eq_zero, add_zero, CategoryTheory.Limits.BinaryBicone.inr_snd_assoc, CategoryTheory.Category.id_comp, CategoryTheory.Limits.biprod.ext_from_iff
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : Y ⟶ A
k₂ : Z ⟶ A
hk : f ≫ k₁ = 0 ∧ k₁ = g ≫ k₂
refine_1 :
  ∀ (hk : f ≫ g ≫ k₂ = 0),
    (f ≫ g) ≫ biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂) = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0

Tactic:
obtain ⟨hk, rfl⟩ := hk

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk : f ≫ g ≫ k₂ = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂) = 0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : biprod.{v, u} Y Z ⟶ A
hk : φ f g ≫ k = 0
refine_2 :
  ∀ (k₁ : Y ⟶ A) (k₂ : Z ⟶ A)
    (hk : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0),
    π f g ≫
        cokernel.desc (f ≫ g) (biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂))
          ⋯ =
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂)
⊢ π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ k) ⋯ = k

Tactic:
obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_from k

Premises used: CategoryTheory.Limits.biprod.decomp_hom_from, rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : Y ⟶ A
k₂ : Z ⟶ A
hk_1 : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂) = 0
hk : f ≫ k₁ = 0 ∧ k₁ = g ≫ k₂
refine_2 :
  ∀ (hk : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂) = 0)
    (hk_2 : f ≫ g ≫ k₂ = 0),
    π f g ≫
        cokernel.desc (f ≫ g)
          (biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂)) ⋯ =
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂)
⊢ π f g ≫
      cokernel.desc (f ≫ g) (biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂))
        ⋯ =
    HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ k₁) (biprod.snd ≫ k₂)

Tactic:
obtain ⟨hk, rfl⟩ := hk

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk_1 : φ f g ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂) = 0
hk : f ≫ g ≫ k₂ = 0
⊢ π f g ≫
      cokernel.desc (f ≫ g)
        (biprod.inr ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂)) ⋯ =
    HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ A) (biprod.fst ≫ g ≫ k₂) (biprod.snd ≫ k₂)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 𝟙 X ≫ f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ≫ 𝟙 Z = f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := kernel f ⟶ kernel g)
    (CategoryStruct.comp (Y := kernel (f ≫ g)) (kernel.map f (f ≫ g) (𝟙 X) g ⋯) (kernel.map (f ≫ g) g f (𝟙 Z) ⋯)) 0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl biprod.snd) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v + 1} (α := Y ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.snd) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := cokernel f ⟶ cokernel g)
    (CategoryStruct.comp (Y := cokernel (f ≫ g)) (cokernel.map f (f ≫ g) (𝟙 X) g ⋯) (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯))
    0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
h₂ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₂)
    (Functor.mapCone ShortComplex.π₂
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
h₃ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₃)
    (Functor.mapCone ShortComplex.π₃
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
⊢ IsLimit (C := ShortComplex.{v, u} C)
    (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
apply ShortComplex.isLimitOfIsLimitπ

Premises used: CategoryTheory.ShortComplex.isLimitOfIsLimitπ
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ :
  IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₁ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₁)
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

Premises used: CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₂ :
  IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₂)
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₂)
    (Functor.mapCone ShortComplex.π₂
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

Premises used: CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₃ :
  IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₃)
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₃)
    (Functor.mapCone ShortComplex.π₃
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

Premises used: CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, Equiv.invFun