awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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),
      ∀ (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
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
have refine : IsLimit (F := parallelPair f 0 ⋙ F) (F.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) sorry))
Tactic: refine preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
⊢ IsLimit (F := parallelPair f 0 ⋙ F) (F.mapCone (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯))
have apply : IsLimit (F := parallelPair (F.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) sorry) F)
Tactic: apply (KernelFork.isLimitMapConeEquiv _ F).2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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) := ⋯
⊢ IsLimit (F := parallelPair (F.map f) 0) (KernelFork.map (Fork.ofι (P := Limits.kernel f) (kernel.ι f) ⋯) F)
have this : Mono (X := X₁ (S.map F)) (ShortComplex.f (S.map F))
Tactic: have : Mono (S.map F).f := hS.2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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.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
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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
⊢ [∀ (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
have tfae_3_to_4 : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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),
      ∀ (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
have 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)
Tactic: tfae_have 4 → 1
  | ⟨_⟩, S, hS =>
    (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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
⊢ Exact (S.map F) ∧ Epi (F.map S.g)
have this : F.PreservesEpimorphisms
Tactic: have := preservesEpimorphisms_of_preserves_shortExact_right F hF
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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)
have refine : Exact (S.map F)
Tactic: refine ⟨?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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 := ⋯ }
⊢ 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₂)
have rw : F.map (CategoryStruct.comp (Y := T.X₁) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f))) =
  F.map S.f ≫ 𝟙 (F.obj S.X₂)
Tactic: rw [← F.map_comp, Abelian.image.fac, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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₂)
⊢ 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₂)
have rw₁ : F.map S.f = F.map S.f ≫ 𝟙 (F.obj S.X₂)
Tactic: rw [← F.map_comp, Abelian.image.fac, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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₂)
⊢ 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₂)
have rw₂ : F.map S.f = F.map S.f
Tactic: rw [← F.map_comp, Abelian.image.fac, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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),
      ∀ (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
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
have refine : IsColimit (F := parallelPair f 0 ⋙ F) (F.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) sorry))
Tactic: refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
⊢ IsColimit (F := parallelPair f 0 ⋙ F) (F.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
have apply : IsColimit (F := parallelPair (F.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) sorry) F)
Tactic: apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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) := ⋯
⊢ IsColimit (F := parallelPair (F.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) F)
have this : Epi (X := X₂ (S.map F)) (g (S.map F))
Tactic: have : Epi (S.map F).g := hS.2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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.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
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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
⊢ [∀ (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
have tfae_3_to_4 : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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),
      ∀ (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
have 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)
Tactic: tfae_have 4 → 1
  | ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2
    ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
have refine_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
Tactic: refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
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
⊢ F.PreservesHomology
have refine_2 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
Tactic: refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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
⊢ PreservesLimit (parallelPair f 0) F
have h : ∀ ⦃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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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
⊢ PreservesColimit (parallelPair f 0) F
have h : ∀ ⦃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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
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),
      ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F), F.PreservesHomology,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
have tfae_1_to_3 : ∀ (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