awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'

Tactic:
have fac : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f' := by
    rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
fac : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
epi_of_epi_fac fac

Premises used: CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
fac : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
exact epi_of_epi_fac fac

Premises used: CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
⊢ HasZeroObject.{u_2, u_1} C

Tactic:
have := hS'.hasZeroObject
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this : HasZeroObject.{u_2, u_1} C
⊢ (S.sc hS k ⋯).HasHomology

Tactic:
have := hS'.hasHomology
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
⊢ Mono h.g'

Tactic:
have := h.exact_iff_mono_g'.1 hS'
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
rw : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.p ≫ h.g'
rw₁ : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g
rw₂ : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g
rw₃ rw₄ : S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS k ⋯).g
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'

Tactic:
rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]

Premises used: CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p, CategoryTheory.cancel_epi, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'

Tactic:
have fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = h.g' := by
    rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
mono_of_mono_fac fac

Premises used: CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
exact mono_of_mono_fac fac

Premises used: CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have : Mono (hS.cokerToKer' k hk cc kf hcc hkf) :=
      hS.toIsComplex.mono_cokerToKer' k hk cc kf hcc hkf
    (hS.exact k)
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
this : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have : Epi (hS.cokerToKer' k hk cc kf hcc hkf) :=
    hS.epi_cokerToKer' k hk cc kf hcc hkf (hS.exact (k + 1))
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
this_1 : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
this : Epi (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ (hS.cokerIsoKer' k hk cc kf hcc hkf).inv = 𝟙 cc.pt

Tactic:
(hS.cokerIsoKer' k hk cc kf hcc hkf).hom_inv_id

Premises used: CategoryTheory.ComposableArrows.IsComplex.cokerToKer', CategoryTheory.ComposableArrows.Exact.cokerIsoKer', CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ (hS.cokerIsoKer' k hk cc kf hcc hkf).inv ≫ hS.cokerToKer' k hk cc kf hcc hkf = 𝟙 kf.pt

Tactic:
(hS.cokerIsoKer' k hk cc kf hcc hkf).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ComposableArrows.IsComplex.cokerToKer', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
inst_3 :
  HasCokernel (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
inst_4 :
  HasKernel (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
⊢ Eq (α := S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (CategoryStruct.comp (Y :=
        cokernel (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
          (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩))
        (cokernel.π (S.map' k (k + 1) ⋯ ⋯) :
          S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶
            cokernel (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
              (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩))
        (CategoryStruct.comp (Y :=
            kernel (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
              (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩))
            (Iso.hom (hS.cokerIsoKer k ⋯) :
              cokernel (X := S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1))) (Y := S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)))
                  (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1))) ⟶
                kernel (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
                  (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩))
            (kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯) :
              kernel (X := S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1))) (Y := S.obj (⟨k + 3, ⋯⟩ : Fin (n + 3 + 1)))
                  (S.map' (k + 2) (k + 3) ⋯ ⋯ :
                    S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj (⟨k + 3, ⋯⟩ : Fin (n + 3 + 1))) ⟶
                S.obj ⟨k + 2, ⋯⟩) :
          cokernel (X := S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1))) (Y := S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)))
              (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1))) ⟶
            S.obj ⟨k + 2, ⋯⟩) :
      S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (S.map' (k + 1) (k + 2) ⋯ ⋯ : S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)

Tactic:
hS.toIsComplex.cokerToKer_fac k

Premises used: CategoryTheory.ComposableArrows.IsComplex.cokerToKer', CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.IsComplex.cokerToKer, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
h₁ : (hS.sc k ⋯).HasRightHomology
h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology
⊢ CategoryStruct.comp (Y := (hS.sc k ⋯).opcycles) (hS.sc k ⋯).pOpcycles
      (CategoryStruct.comp (Y := (hS.sc (k + 1) ⋯).cycles)
        (Iso.hom (hS.opcyclesIsoCycles k ⋯) : (hS.sc k ⋯).opcycles ⟶ (hS.sc (k + 1) ⋯).cycles)
        ((hS.sc (k + 1) ⋯).iCycles : (hS.sc (k + 1) ⋯).cycles ⟶ (hS.sc (k + 1) ⋯).X₂)) =
    S.map' (k + 1) (k + 2) ⋯ ⋯

Tactic:
hS.toIsComplex.opcyclesToCycles_fac k hk

Premises used: CategoryTheory.ComposableArrows.IsComplex.cokerToKer', CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles
-- Module: Mathlib.Algebra.Homology.Factorizations.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
hY : IsZero.{v_1, u_1} (L.X n)
⊢ epiWithInjectiveKernel (f.f n) ↔ Injective.{v_1, u_1} (K.X n)

Tactic:
rw [epiWithInjectiveKernel_iff_of_isZero]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff_of_isZero
-- Module: Mathlib.Algebra.Homology.Factorizations.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ IsZero.{v_1, u_1} (L.X n)

Tactic:
(HomologicalComplex.eval _ _ n).map_isZero hL

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Factorizations.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ IsZero.{v_1, u_1} (L.X n)

Tactic:
exact (HomologicalComplex.eval _ _ n).map_isZero hL

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Factorizations.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
h : degreewiseEpiWithInjectiveKernel f
⊢ Epi f

Tactic:
HomologicalComplex.epi_of_epi_f f (fun n ↦ (h n).1)

Premises used: And.left, HomologicalComplex.epi_of_epi_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
F : (cofFib f).FullSubcategory
⊢ Mono F.obj (P := cofFib f).ι

Tactic:
F.property.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.left
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ ∀ (i : ℤ),
    (ComplexShape.up ℤ).Rel i n₁ →
      Eq (α := K.X i ⟶ Injective.under.{v_1, u_1} (opcycles K n₁))
        (K.d i n₁ ≫ pOpcycles K n₁ ≫ Injective.ι (opcycles K n₁)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ : ℤ
⊢ CategoryStruct.comp (Y := mid K L n₁) (ι f n₁) (π K L n₁) = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
inst_3 : Mono f
⊢ Mono (Y := mid K L n₁) (ι f n₁)

Tactic:
mono_of_mono_fac (ι_π f n₁)

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι_π, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ q : ℤ
rw :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mid K L n₁).X q) (w : f ≫ Hom.f (π K L n₁) q = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mid K L n₁).X q, X₃ := L.X q, f := f, g := Hom.f (π K L n₁) q, zero := w :
          ShortComplex.{v_1, u_1} C }.Splitting
⊢ epiWithInjectiveKernel (X := (mid K L n₁).X q) (Hom.f (π K L n₁) q)

Tactic:
rw [Abelian.epiWithInjectiveKernel_iff]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ q : ℤ
⊢ Eq (α := (S K n₁).X q ⟶ L.X q) (CategoryStruct.comp (Y := (mid K L n₁).X q) (Hom.f biprod.inl q) (Hom.f (π K L n₁) q))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ q : ℤ
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mid K L n₁).X q) (w : f ≫ Hom.f (π K L n₁) q = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mid K L n₁).X q, X₃ := L.X q, f := f, g := Hom.f (π K L n₁) q, zero := w :
          ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
exact ⟨(S K n₁).X q, inferInstance, (biprod.inl : _ ⟶ mid K L n₁).f q, by simp,
    ⟨{ r := (biprod.fst : mid K L n₁ ⟶ _).f q, s := (biprod.inr : _ ⟶ mid K L n₁).f q }⟩⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
⊢ CategoryStruct.comp (Y := (mid K L n₁).X i) (Hom.f biprod.inr i) (Hom.f (π K L n₁) i) = 𝟙 (L.X i)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
refine : Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i = 𝟙 ((mid K L n₁).X i)
⊢ IsIso (X := (mid K L n₁).X i) (Hom.f (π K L n₁) i)

Tactic:
refine ⟨(biprod.inr : _ ⟶ mid K L n₁).f i, ?_, by simp⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
rw :
  Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i) ∧
    Eq (α := (mid K L n₁).X i ⟶ L.X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
⊢ Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i = 𝟙 ((mid K L n₁).X i)

Tactic:
rw [biprodX_ext_to_iff]

Premises used: HomologicalComplex.biprodX_ext_to_iff