awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
⊢ Eq (α := F.obj S.X₁ ⟶ F.obj (cokernel S.f)) (F.map S.f ≫ F.map (cokernel.π S.f)) 0

Tactic:
simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
h :
  ∀ (l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)) (hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)),
    Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0

Tactic:
obtain ⟨l, hl⟩ :=
    cokernel.desc' (F.map S.f) (F.map (cokernel.π S.f))
      (by simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero])

Premises used: CategoryTheory.Limits.cokernel.desc', CategoryTheory.Functor.map, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
S : ShortComplex.{v₁, u₁} C
hS : Eq (α := Limits.kernel (F.map S.g) ⟶ cokernel (F.map S.f)) (kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f)) 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
h : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f)) 0
h₁ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l) 0
h₂ : (k ≫ kernel.ι (F.map S.g)) ≫ cokernel.π (F.map S.f) ≫ l = 0
h₃ : k ≫ kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0
h₄ : k ≫ 0 ≫ l = 0
h₅ : Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (k ≫ 0) 0
h₆ h₇ : Eq.{v₂ + 1} (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) 0 0
⊢ Eq (α := F.obj (Limits.kernel S.g) ⟶ F.obj (cokernel S.f)) (F.map (kernel.ι S.g ≫ cokernel.π S.f)) 0

Tactic:
rw [F.map_comp, ← hl, ← hk, Category.assoc, reassoc_of% hS, zero_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
apply : ShortComplex.Exact (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)
⊢ Mono (L.map f)

Tactic:
apply ((Abelian.tfae_mono (L.map f) (L.obj 0)).out 2 0).mp

Premises used: CategoryTheory.Functor.map, List.TFAE.out, Iff.mp, CategoryTheory.Abelian.tfae_mono, OfNat.ofNat, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)

Tactic:
ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))

Premises used: CategoryTheory.ShortComplex.exact_of_iso, List.TFAE.out, Iff.mp, CategoryTheory.Abelian.tfae_mono, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
refine :
  Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 f ⋯) L)
    (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)

Tactic:
refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))

Premises used: CategoryTheory.ShortComplex.exact_of_iso, List.TFAE.out, Iff.mp, CategoryTheory.Abelian.tfae_mono, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Mono f
⊢ Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 f ⋯) L)
    (ShortComplex.mk (X₁ := L.obj 0) 0 (L.map f) ⋯)

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
apply : ShortComplex.Exact (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)
⊢ Epi (L.map f)

Tactic:
apply ((Abelian.tfae_epi (L.map f) (L.obj 0)).out 2 0).mp

Premises used: CategoryTheory.Abelian.tfae_epi, CategoryTheory.Functor.map, List.TFAE.out, Iff.mp, OfNat.ofNat, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)

Tactic:
ShortComplex.exact_of_iso ?_ (hL _ (((tfae_epi f 0).out 0 2).mp hf))

Premises used: CategoryTheory.Abelian.tfae_epi, CategoryTheory.ShortComplex.exact_of_iso, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
refine :
  Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₃ := 0) f 0 ⋯) L)
    (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)

Tactic:
refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_epi f 0).out 0 2).mp hf))

Premises used: CategoryTheory.Abelian.tfae_epi, CategoryTheory.ShortComplex.exact_of_iso, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
hf : Epi f
⊢ Iso (C := ShortComplex.{v₂, u₂} B) (ShortComplex.map (ShortComplex.mk (X₃ := 0) f 0 ⋯) L)
    (ShortComplex.mk (X₃ := L.obj 0) (L.map f) 0 ⋯)

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
⊢ L.PreservesMonomorphisms

Tactic:
have := preservesMonomorphisms_of_map_exact _ hL
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
apply : IsLimit (F := parallelPair f 0 ⋙ L) (L.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
apply : IsLimit (F := parallelPair (L.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) L)
⊢ IsLimit (F := parallelPair f 0 ⋙ L) (L.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))

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

Premises used: CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
dsimp : Mono (X := L.obj (Limits.kernel f)) (L.map (kernel.ι f))
⊢ Mono (X := ShortComplex.X₁ (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
    (ShortComplex.f (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono (X := L.obj (Limits.kernel f)) (L.map (kernel.ι f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono (X := ShortComplex.X₁ (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
    (ShortComplex.f (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))

Tactic:
have : Mono ((ShortComplex.mk _ _ (kernel.condition f)).map L).f := by
      dsimp
      infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this :
  Mono (X := ShortComplex.X₁ (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
    (ShortComplex.f (ShortComplex.map (ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯) L))
⊢ IsLimit (F := parallelPair (L.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) L)

Tactic:
exact (hL (ShortComplex.mk _ _ (kernel.condition f))
      (ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel f))).fIsKernel

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, CategoryTheory.ShortComplex.mk, CategoryTheory.Limits.kernel.condition, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
⊢ L.PreservesEpimorphisms

Tactic:
have := preservesEpimorphisms_of_map_exact _ hL
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
apply : IsColimit (F := parallelPair f 0 ⋙ L) (L.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
apply : IsColimit (F := parallelPair (L.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L)
⊢ IsColimit (F := parallelPair f 0 ⋙ L) (L.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))

Tactic:
apply (CokernelCofork.isColimitMapCoconeEquiv _ L).2

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
dsimp : Epi (Y := L.obj (cokernel f)) (L.map (cokernel.π f))
⊢ Epi (X := ShortComplex.X₂ (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
    (ShortComplex.g (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ Epi (Y := L.obj (cokernel f)) (L.map (cokernel.π f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ Epi (X := ShortComplex.X₂ (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
    (ShortComplex.g (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))

Tactic:
have : Epi ((ShortComplex.mk _ _ (cokernel.condition f)).map L).g := by
      dsimp
      infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
X Y : A
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this :
  Epi (X := ShortComplex.X₂ (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
    (ShortComplex.g (ShortComplex.map (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯) L))
⊢ IsColimit (F := parallelPair (L.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L)

Tactic:
exact (hL (ShortComplex.mk _ _ (cokernel.condition f))
      (ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel f))).gIsCokernel

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, CategoryTheory.ShortComplex.mk, CategoryTheory.Limits.cokernel.condition, CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
hL : ∀ (S : ShortComplex.{v₁, u₁} A), S.Exact → ShortComplex.Exact (S.map L)
⊢ L.PreservesHomology

Tactic:
apply preservesHomology_of_map_exact

Premises used: CategoryTheory.Functor.preservesHomology_of_map_exact
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
dsimp :
  𝟙 (L.obj S.X₂) ≫ L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
⊢ 𝟙
        (ShortComplex.X₂
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)) ≫
      ShortComplex.g (S.map L) =
    ShortComplex.g
        ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
              ShortComplex.{v₁, u₁} A }.map
          L) ≫
      L.map (Abelian.factorThruCoimage S.g)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
rw :
  L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))
rw₁ :
  L.map S.g =
    L.map (CategoryStruct.comp (Y := Abelian.coimage S.g) (cokernel.π (kernel.ι S.g)) (Abelian.factorThruCoimage S.g))
rw₂ rw₃ : L.map S.g = L.map S.g
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g =
    CategoryStruct.comp (Y := L.obj (Abelian.coimage S.g)) (L.map (cokernel.π (kernel.ι S.g)))
      (L.map (Abelian.factorThruCoimage S.g))

Tactic:
rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesMonomorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B)
  ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L)
  (S.map L) :=
  {
    τ₁ :=
      𝟙
        (ShortComplex.X₁
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₂ :=
      𝟙
        (ShortComplex.X₂
          ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
                ShortComplex.{v₁, u₁} A }.map
            L)),
    τ₃ := L.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯, comm₂₃ := ⋯ }
hL :
  ShortComplex.Exact
    ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ :
          ShortComplex.{v₁, u₁} A }.map
      L)
⊢ ShortComplex.Exact (S.map L)

Tactic:
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).1

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, Iff.mp