-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma hasCokernel [S.HasLeftHomology] [HasKernel S.g] :
    HasCokernel (kernel.lift S.g S.f S.zero)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.right ≫
      ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi).hom =
    (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h.f' 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.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Tactic:
haveI : HasColimit (parallelPair h.f' 0) := ⟨⟨⟨_, h.hπ'⟩⟩⟩

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.left ≫
      ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi).hom =
    (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h.f' 0).map WalkingParallelPairHom.left

Tactic:
aesop_cat

Result:
no goals

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

Tactic:
let h := S.leftHomologyData

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Tactic:
let e : parallelPair (kernel.lift S.g S.f S.zero) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl _) (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi)
    (by aesop_cat) (by simp)

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
e : parallelPair (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero))
    ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi) ⋯ ⋯
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
e : parallelPair (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero))
    ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi) ⋯ ⋯
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Tactic:
exact hasColimitOfIso e

Result:
no goals