-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a short complex `S` is such that `S.g = 0` and that the cokernel of `S.f` is preserved
by a functor `F`, then `F` preserves the left homology of `S`. -/
lemma preservesLeftHomology_of_zero_g (hg : S.g = 0)
    [PreservesColimit (parallelPair S.f 0) F] :
    F.PreservesLeftHomologyOf S := ⟨fun h =>
  { g

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.right ≫ (asIso h.i).hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.right

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair 0 0) F

Tactic:
infer_instance

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
rw [hg]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair 0 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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.left ≫ (asIso h.i).hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.left

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
have := h.isIso_i hg

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ PreservesColimit (parallelPair h.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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) (asIso h.i) ⋯ ⋯
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
exact Limits.preservesColimit_of_iso_diagram F e.symm

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
let e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl _) (asIso h.i) (by simp) (by simp)

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) (asIso h.i) ⋯ ⋯
⊢ PreservesColimit (parallelPair h.f' 0) F