-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
neg₄ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
neg₅ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    0
neg₆ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap ((K.shortComplexTruncLE e).f ≫ (K.shortComplexTruncLE e).g) (e.f i)) 0
neg₇ :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap 0 (e.f i)) 0
neg₈ neg₉ :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i)) 0 0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, HomologicalComplex.homologyMap_comp, HomologicalComplex.shortComplexTruncLE, HomologicalComplex.homologyMap_zero, CategoryTheory.ShortComplex.zero, ComplexShape.Embedding.f, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g