-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a functor preserves a certain left homology data of a short complex `S`, then it
preserves the left homology of `S`. -/
lemma PreservesLeftHomologyOf.mk' (h : S.LeftHomologyData) [h.IsPreservedBy F] :
    F.PreservesLeftHomologyOf S where
  isPreservedBy h' :=
    { g := ShortComplex.LeftHomologyData.IsPreservedBy.hg h F
      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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
have := ShortComplex.LeftHomologyData.IsPreservedBy.hf' h 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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ 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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
exact preservesColimit_of_iso_diagram F e

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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
let e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl _) (ShortComplex.cyclesMapIso' (Iso.refl S) h h')
    (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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ 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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.left ≫ (ShortComplex.cyclesMapIso' (Iso.refl S) h h').hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h'.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
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.right ≫ (ShortComplex.cyclesMapIso' (Iso.refl S) h h').hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h'.f' 0).map WalkingParallelPairHom.right

Tactic:
simp

Result:
no goals