awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯
hS : Exact (S.map F) ∧ Mono (F.map S.f) := ⋯
⊢ Mono (X := X₁ (S.map F)) (ShortComplex.f (S.map F))

Tactic:
have : Mono (S.map F).f := hS.2
-- 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
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := Limits.kernel f) (kernel.ι f) f ⋯
hS : Exact (S.map F) ∧ Mono (F.map S.f) := ⋯
this : Mono (X := X₁ (S.map F)) (ShortComplex.f (S.map F))
⊢ IsLimit (F := parallelPair (F.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) F)

Tactic:
exact hS.1.fIsKernel

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, And.left
-- 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:
tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_
    apply (KernelFork.isLimitMapConeEquiv _ F).2
    let S := ShortComplex.mk _ _ (kernel.condition f)
    let hS := hF S ⟨exact_kernel f, inferInstance⟩
    have : Mono (S.map F).f := hS.2
    exact hS.1.fIsKernel
-- 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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ ⦃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)
tfae_2_to_3 :
  ∀ (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
⊢ PreservesFiniteLimits F

Tactic:
4

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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F

Tactic:
3 → 4

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)
tfae_2_to_3 :
  ∀ (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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F := h
⊢ 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 : 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)
tfae_2_to_3 :
  ∀ (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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F := h
⊢ 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 : 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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F

Tactic:
tfae_have 3 → 4
  | hF => by
    exact preservesFiniteLimits_of_preservesKernels 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 : 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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F
⊢ PreservesFiniteLimits F

Tactic:
4

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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F
⊢ ∀ (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
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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F
⊢ ∀ (a : PreservesFiniteLimits F) (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
4 → 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
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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F
⊢ ∀ (a : PreservesFiniteLimits F) (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
tfae_have 4 → 1
  | ⟨_⟩, S, hS =>
    (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel 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 : 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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F), PreservesFiniteLimits F
tfae_4_to_1 :
  ∀ (a : PreservesFiniteLimits F) (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.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, PreservesFiniteLimits F].TFAE

Tactic:
tfae_finish
-- 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
⊢ PreservesFiniteLimits F ↔ ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)

Tactic:
(Functor.preservesFiniteLimits_tfae F).out 3 0

Premises used: CategoryTheory.Functor.preservesFiniteLimits_tfae, List.TFAE.out, OfNat.ofNat
-- 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) ∧ Epi (F.map S.g)

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 ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)

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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)

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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
⊢ F.PreservesEpimorphisms

Tactic:
have := preservesEpimorphisms_of_preserves_shortExact_right 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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
⊢ Exact (S.map F) ∧ Epi (F.map S.g)

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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
refine : Exact (S.map F)
⊢ Exact (S.map F) ∧ Epi (F.map S.g)

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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
rw :
  F.map (CategoryStruct.comp (Y := T.X₁) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f))) =
    F.map S.f ≫ 𝟙 (F.obj S.X₂)
rw₁ : F.map S.f = F.map S.f ≫ 𝟙 (F.obj S.X₂)
rw₂ rw₃ : F.map S.f = F.map S.f
⊢ CategoryStruct.comp (Y := F.obj (Limits.kernel (Y := cokernel S.f) (cokernel.π S.f)))
      (F.map (Abelian.factorThruImage S.f)) (F.map (kernel.ι (cokernel.π S.f))) =
    F.map S.f ≫ 𝟙 (F.obj S.X₂)

Tactic:
rw [← F.map_comp, Abelian.image.fac, Category.comp_id]

Premises used: CategoryTheory.Abelian.image.fac, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
φ : Quiver.Hom (V := ShortComplex.{v_2, u_2} D) (S.map F) (T.map F) :=
  { τ₁ := F.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (X₂ (S.map F)), τ₃ := 𝟙 (X₃ (S.map F)), comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ Exact (S.map F)

Tactic:
(exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1

Premises used: Iff.mpr, CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.ShortComplex.ShortExact.mk, And.left, Iff.mp
-- 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) ∧ Epi (F.map S.g)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Epi S.g
this : F.PreservesEpimorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }
φ : Quiver.Hom (V := ShortComplex.{v_2, u_2} D) (S.map F) (T.map F) :=
  { τ₁ := F.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (X₂ (S.map F)), τ₃ := 𝟙 (X₃ (S.map F)), comm₁₂ := ⋯,
    comm₂₃ := ⋯ }
⊢ Exact (S.map F)

Tactic:
exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1

Premises used: Iff.mpr, CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.ShortComplex.ShortExact.mk, And.left, Iff.mp
-- 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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)

Tactic:
tfae_have 1 → 2
  | hF, S, ⟨hS, hf⟩ => by
    have := preservesEpimorphisms_of_preserves_shortExact_right F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
    let φ : S.map F ⟶ T.map F :=
      { τ₁ := F.map <| Abelian.factorThruImage S.f
        τ₂ := 𝟙 _
        τ₃ := 𝟙 _
        comm₁₂ := show _ ≫ F.map (kernel.ι _) = F.map _ ≫ 𝟙 _ by
          rw [← F.map_comp, Abelian.image.fac, Category.comp_id] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)

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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)) ⦃X Y : C⦄
    (f : X ⟶ Y), PreservesColimit (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) ∧ Epi (F.map S.g))
    (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact ∧ Epi S.g → Exact (S.map F) ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone