-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫
          (homologyFunctorFactors C (up ℤ) n₁).inv.app _

Proof state:
case a.w.h.op.h.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (((HomologicalComplex.homologyFunctor C (up ℤ) 0).shift n₁).obj S.X₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Tactic:
dsimp [homologyFunctor_shift]

Result:
case a.w.h.op.h.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Proof state:
case a.w.h.op.h.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀
⊢ (yoneda.map
          ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
            (homologyFunctor C (up ℤ) 0).homologySequenceδ
                (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                  ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
                n₀ n₁ h ≫
              (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
      (Opposite.op A) x =
    (yoneda.map
          (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
            hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
      (Opposite.op A) x

Tactic:
erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]

Result:
case a.w.h.op.h.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀
⊢ (yoneda.map
          ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
            (homologyFunctorFactors C (up ℤ) n₀).hom.app (triangle S.f).obj₃ ≫
              (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
                (homologyFunctorFactors C (up ℤ) n₁).inv.app (triangle S.f).obj₁ ≫
                  (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
      (Opposite.op A) x =
    (yoneda.map
          (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
            hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
      (Opposite.op A) x

Proof state:
case a.w.h.op.h.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫
      (mappingCone S.f).homologyπ n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
  inl_v_descShortComplex_f, comp_zero, zero_add]

Result:
case a.w.h.op.h.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫
      (mappingCone S.f).homologyπ n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h