-- Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
/--
For an additive functor `F : C ⥤ D` between abelian categories, the following are equivalent:
- `F` preserves short exact sequences, i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then
  `0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact.
- `F` preserves exact sequences, i.e. if `A ⟶ B ⟶ C` is exact then `F(A) ⟶ F(B) ⟶ F(C)` is exact.
- `F` preserves homology.
- `F` preserves both finite limits and finite colimits.
-/
lemma exact_tfae : List.TFAE
    [
      ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact,
      ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      PreservesHomology F,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F
    ]

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 4 → 2
| ⟨h1, h2⟩, _, h => h.map F

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
tfae_4_to_2 : PreservesFiniteLimits F ∧ PreservesFiniteColimits F → ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ (ShortComplex.mk 0 S.f ⋯).f = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
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)

Result:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ PreservesColimit (parallelPair f 0) F

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ S.g ≫ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
tfae_4_to_2 : PreservesFiniteLimits F ∧ PreservesFiniteColimits F → ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
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

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ ((ShortComplex.mk S.g 0 ?m.44208).map F).g = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 2 → 1
| hF, S, hS => by
  have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
    hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
  have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
    hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
  exact ⟨hF S hS.exact⟩

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Proof state:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
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

Result:
no goals