-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
h :
  (Cochain.v (inl f) (n + 2) (n + 1) ⋯ ≫
          Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n ⋯ ≫
            Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
        Cochain.v (inl f) (n + 2) (n + 1) ⋯ ≫
          Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n ⋯ ≫
            (-HAdd.hAdd (α :=
                      Cochain (mappingCone (mappingConeCompTriangle f g).mor₁)
                        (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
                      (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                            (Cochain.comp (inl f)
                              (Cochain.ofHom
                                ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                              ⋯)
                            (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                          ⋯)
                        ⋯)
                      (Cochain.comp
                        (Cochain.comp
                          (↑(fst (mappingConeCompTriangle f g).mor₁) :
                            Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁
                              1)
                          (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                        ⋯) +
                  Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
              n n ⋯ ∧
      HomologicalComplex.Hom.f (inr f) (n + 1) ≫
          Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n ⋯ ≫
            Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
        HomologicalComplex.Hom.f (inr f) (n + 1) ≫
          Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n ⋯ ≫
            (-HAdd.hAdd (α :=
                      Cochain (mappingCone (mappingConeCompTriangle f g).mor₁)
                        (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
                      (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                            (Cochain.comp (inl f)
                              (Cochain.ofHom
                                ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                              ⋯)
                            (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                          ⋯)
                        ⋯)
                      (Cochain.comp
                        (Cochain.comp
                          (↑(fst (mappingConeCompTriangle f g).mor₁) :
                            Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁
                              1)
                          (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                        ⋯) +
                  Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
              n n ⋯) ∧
    Cochain.v (inl (f ≫ g)) (n + 1) n ⋯ ≫
          HomologicalComplex.Hom.f (inr (mappingConeCompTriangle f g).mor₁) n ≫
            Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
        Cochain.v (inl (f ≫ g)) (n + 1) n ⋯ ≫
          HomologicalComplex.Hom.f (inr (mappingConeCompTriangle f g).mor₁) n ≫
            (-HAdd.hAdd (α :=
                      Cochain (mappingCone (mappingConeCompTriangle f g).mor₁)
                        (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
                      (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                            (Cochain.comp (inl f)
                              (Cochain.ofHom
                                ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                              ⋯)
                            (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                          ⋯)
                        ⋯)
                      (Cochain.comp
                        (Cochain.comp
                          (↑(fst (mappingConeCompTriangle f g).mor₁) :
                            Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁
                              1)
                          (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                        ⋯) +
                  Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
              n n ⋯ ∧
      HomologicalComplex.Hom.f (inr (f ≫ g)) n ≫
          HomologicalComplex.Hom.f (inr (mappingConeCompTriangle f g).mor₁) n ≫
            Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
        HomologicalComplex.Hom.f (inr (f ≫ g)) n ≫
          HomologicalComplex.Hom.f (inr (mappingConeCompTriangle f g).mor₁) n ≫
            (-HAdd.hAdd (α :=
                      Cochain (mappingCone (mappingConeCompTriangle f g).mor₁)
                        (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
                      (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                            (Cochain.comp (inl f)
                              (Cochain.ofHom
                                ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                              ⋯)
                            (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                          ⋯)
                        ⋯)
                      (Cochain.comp
                        (Cochain.comp
                          (↑(fst (mappingConeCompTriangle f g).mor₁) :
                            Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁
                              1)
                          (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
                        (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                          (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                        ⋯) +
                  Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
              n n ⋯
⊢ Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
    (-HAdd.hAdd (α :=
              Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingCone (mappingConeCompTriangle f g).mor₁)
                0)
              (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                  (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                    (Cochain.comp (inl f)
                      (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯)
                    (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                  ⋯)
                ⋯)
              (Cochain.comp
                (Cochain.comp
                  (↑(fst (mappingConeCompTriangle f g).mor₁) :
                    Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁ 1)
                  (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
                (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                  (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                ⋯) +
          Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
      n n ⋯

Tactic:
rw [ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 1) n rfl,
        ext_from_iff _ (n + 2) (n + 1) (by lia)]

Premises used: CochainComplex.mappingCone.ext_from_iff, HAdd.hAdd, OfNat.ofNat, rfl