-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a functor preserves a certain right homology data of a short complex `S`, then it
preserves the right homology of `S`. -/
lemma PreservesRightHomologyOf.mk' (h : S.RightHomologyData) [h.IsPreservedBy F] :
    F.PreservesRightHomologyOf S where
  isPreservedBy h' :=
    { f := ShortComplex.RightHomologyData.IsPreservedBy.hf h F
      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
h : S.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)).hom =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 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.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
e : parallelPair h.g' 0 ≅ parallelPair h'.g' 0 :=
  parallelPair.ext (ShortComplex.opcyclesMapIso' (Iso.refl S) h h')
    (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h'.g' 0) F

Tactic:
exact preservesLimit_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.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)).hom =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 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
h : S.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ PreservesLimit (parallelPair h'.g' 0) F

Tactic:
let e : parallelPair h.g' 0 ≅ parallelPair h'.g' 0 :=
  parallelPair.ext (ShortComplex.opcyclesMapIso' (Iso.refl S) h h') (Iso.refl _)
    (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.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
e : parallelPair h.g' 0 ≅ parallelPair h'.g' 0 :=
  parallelPair.ext (ShortComplex.opcyclesMapIso' (Iso.refl S) h h')
    (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h'.g' 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.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
⊢ PreservesLimit (parallelPair h'.g' 0) F

Tactic:
have := ShortComplex.RightHomologyData.IsPreservedBy.hg' 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.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ PreservesLimit (parallelPair h'.g' 0) F