-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
by a functor `F`, then `F` preserves the right homology of `S`. -/
lemma preservesRightHomology_of_zero_f (hf : S.f = 0)
    [PreservesLimit (parallelPair S.g 0) F] :
    F.PreservesRightHomologyOf S := ⟨fun h =>
  { 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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
let e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (asIso h.p) (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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (asIso h.p) (Iso.refl ((parallelPair S.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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)).hom =
    (asIso h.p).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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
rw [hf]

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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
have := h.isIso_p hf

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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ 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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (asIso h.p) (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
exact Limits.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
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)).hom =
    (asIso h.p).hom ≫ (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp

Result:
no goals