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) ∧ 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
refine : IsColimit (F := parallelPair f 0 ⋙ F) (F.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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
apply : IsColimit (F := parallelPair (F.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) F)
⊢ IsColimit (F := parallelPair f 0 ⋙ F) (F.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))

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

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.invFun
-- 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
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
hS : Exact (S.map F) ∧ Epi (F.map S.g) := ⋯
⊢ Epi (X := X₂ (S.map F)) (g (S.map F))

Tactic:
have : Epi (S.map F).g := 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) ∧ 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
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
hS : Exact (S.map F) ∧ Epi (F.map S.g) := ⋯
this : Epi (X := X₂ (S.map F)) (g (S.map F))
⊢ IsColimit (F := parallelPair (F.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) F)

Tactic:
exact hS.1.gIsCokernel

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, 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) ∧ 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:
tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
    apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
    let S := ShortComplex.mk _ _ (cokernel.condition f)
    let hS := hF S ⟨exact_cokernel f, inferInstance⟩
    have : Epi (S.map F).g := hS.2
    exact hS.1.gIsCokernel
-- 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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ ⦃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)
tfae_2_to_3 :
  ∀ (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
⊢ PreservesFiniteColimits 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) ∧ 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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits 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) ∧ 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)
tfae_2_to_3 :
  ∀ (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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F := h
⊢ 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 : 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)
tfae_2_to_3 :
  ∀ (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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F := h
⊢ 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
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)
tfae_2_to_3 :
  ∀ (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
⊢ ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits F

Tactic:
tfae_have 3 → 4
  | hF => by
    exact preservesFiniteColimits_of_preservesCokernels 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) ∧ 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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits F
⊢ PreservesFiniteColimits 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) ∧ 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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits F
⊢ ∀ (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
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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits F
⊢ ∀ (a : PreservesFiniteColimits F) (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Epi (F.map S.g)

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

Tactic:
tfae_have 4 → 1
  | ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2
    ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel 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) ∧ 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)
tfae_2_to_3 :
  ∀ (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
tfae_3_to_4 : ∀ (a : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F), PreservesFiniteColimits F
tfae_4_to_1 :
  ∀ (a : PreservesFiniteColimits F) (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.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, PreservesFiniteColimits 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
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map 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
⊢ F.PreservesHomology

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
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology

Tactic:
1 → 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
h : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h
⊢ F.PreservesHomology

Tactic:
⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩

Premises used: CategoryTheory.Functor.PreservesHomology.mk
-- 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
h : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h
refine_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
refine_2 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ F.PreservesHomology

Tactic:
refine ⟨fun {X Y} f ↦ ?_, fun {X Y} 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
h : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F

Tactic:
have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_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
h_1 : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h_1
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
h 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
h_1 : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h_1
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
exact h 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
h : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F

Tactic:
have h := (preservesFiniteColimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).epi_g)
-- 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
h_1 : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h_1
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
h 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
h_1 : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F) := h_1
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
exact h 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
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology

Tactic:
tfae_have 1 → 3
  | hF => by
    refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
    · have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_f)
      exact h f
    · have h := (preservesFiniteColimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).epi_g)
      exact h 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_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map 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_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map 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_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)

Tactic:
2 → 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_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Eq (α :=
    X₁ (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 S.f ⋯) F) ⟶
      X₂ (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 S.f ⋯) F))
    (f (ShortComplex.map (ShortComplex.mk (X₁ := 0) 0 S.f ⋯) F)) 0

Tactic:
simp