awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.f ≫ (𝟙 S.X₂ - r ≫ S.f) = 0

Tactic:
simp [reassoc_of% f_r]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₅ : S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
rw₆ : S.g - 0 = S.g ≫ 𝟙 S.X₃
rw₇ : S.g = S.g ≫ 𝟙 S.X₃
rw₈ rw₉ : S.g = S.g
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃

Tactic:
rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]

Premises used: CategoryTheory.Category.assoc, sub_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Exact.g_desc_assoc, CategoryTheory.ShortComplex.zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
⊢ ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F

Tactic:
have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesKernel F f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ HasBinaryBiproducts.{v_1, u_1} C

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : HasBinaryBiproducts.{v_1, u_1} C
⊢ HasEqualizers.{v_1, u_1} C

Tactic:
have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
⊢ IsZero.{v_2, u_2} (F.obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
⊢ HasZeroObject.{v_2, u_2} D

Tactic:
have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this_3 : HasEqualizers.{v_1, u_1} C
this : HasZeroObject.{v_2, u_2} D
⊢ PreservesFiniteLimits F

Tactic:
preservesFiniteLimits_of_preservesKernels F

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this_3 : HasEqualizers.{v_1, u_1} C
this : HasZeroObject.{v_2, u_2} D
⊢ PreservesFiniteLimits F

Tactic:
exact preservesFiniteLimits_of_preservesKernels F

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
⊢ ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F

Tactic:
have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesCokernel F f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ HasBinaryBiproducts.{v_1, u_1} C

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryCoproducts
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this : HasBinaryBiproducts.{v_1, u_1} C
⊢ HasCoequalizers.{v_1, u_1} C

Tactic:
have : HasCoequalizers C := Preadditive.hasCoequalizers_of_hasCokernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
⊢ IsZero.{v_2, u_2} (F.obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
⊢ HasZeroObject.{v_2, u_2} D

Tactic:
have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this_3 : HasCoequalizers.{v_1, u_1} C
this : HasZeroObject.{v_2, u_2} D
⊢ PreservesFiniteColimits F

Tactic:
preservesFiniteColimits_of_preservesCokernels F

Premises used: CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this_3 : HasCoequalizers.{v_1, u_1} C
this : HasZeroObject.{v_2, u_2} D
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCokernels F

Premises used: CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
⊢ F.PreservesMonomorphisms

Tactic:
have := preservesMonomorphisms_of_preserves_shortExact_left F hF
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
⊢ Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
⟨?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
refine : Exact (S.map F)
⊢ Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
refine ⟨?_, inferInstance⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
rw :
  F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
rw₁ :
  F.map S.g =
    F.map
      (CategoryStruct.comp (Y := cokernel (X := Limits.kernel S.g) (kernel.ι S.g)) (cokernel.π (kernel.ι S.g))
        (Abelian.factorThruCoimage S.g))
rw₂ rw₃ : F.map S.g = F.map S.g
⊢ 𝟙 (F.obj T.X₂) ≫ F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))

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

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
φ : Quiver.Hom (V := ShortComplex.{v_2, u_2} D) (T.map F) (S.map F) :=
  { τ₁ := 𝟙 (X₁ (T.map F)), τ₂ := 𝟙 (X₂ (T.map F)), τ₃ := F.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ Exact (S.map F)

Tactic:
(exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.ShortExact.mk, And.left, Iff.mp, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
φ : Quiver.Hom (V := ShortComplex.{v_2, u_2} D) (T.map F) (S.map F) :=
  { τ₁ := 𝟙 (X₁ (T.map F)), τ₂ := 𝟙 (X₂ (T.map F)), τ₃ := F.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ Exact (S.map F)

Tactic:
exact (exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.ShortExact.mk, And.left, Iff.mp, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
tfae_have 1 → 2
  | hF, S, ⟨hS, hf⟩ => by
    have := preservesMonomorphisms_of_preserves_shortExact_left F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero)
    let φ : T.map F ⟶ S.map F :=
      { τ₁ := 𝟙 _
        τ₂ := 𝟙 _
        τ₃ := F.map <| Abelian.factorThruCoimage S.g
        comm₂₃ := show 𝟙 _ ≫ F.map _ = F.map (cokernel.π _) ≫ _ by
          rw [Category.id_comp, ← F.map_comp, cokernel.π_desc] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)) ⦃X Y : C⦄
    (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
refine : IsLimit (F := parallelPair f 0 ⋙ F) (F.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
refine preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_2 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Mono S.f → Exact (S.map F) ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
apply : IsLimit (F := parallelPair (F.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) F)
⊢ IsLimit (F := parallelPair f 0 ⋙ F) (F.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))

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

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