-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma hasKernel [S.HasRightHomology] [HasCokernel S.f] :
    HasKernel (cokernel.desc S.f S.g S.zero)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ (parallelPair (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)).hom =
    ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp).hom ≫
      (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Tactic:
let e : parallelPair (cokernel.desc S.f S.g S.zero) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) h.hp)
    (Iso.refl _) (coequalizer.hom_ext (by simp)) (by simp)

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
e : parallelPair (cokernel.desc S.f S.g ⋯) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp)
    (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
e : parallelPair (cokernel.desc S.f S.g ⋯) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp)
    (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Tactic:
exact hasLimitOfIso e.symm

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Tactic:
let h := S.rightHomologyData

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ coequalizer.π S.f 0 ≫
      (parallelPair (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.left ≫
        (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)).hom =
    coequalizer.π S.f 0 ≫
      ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp).hom ≫
        (parallelPair h.g' 0).map WalkingParallelPairHom.left

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Tactic:
haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ HasKernel (cokernel.desc S.f S.g ⋯)