-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 : ℤ
⊢ 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 ⋯
have h : (Cochain.v (inl f) (n + 2) (n + 1) sorry ≫
        Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n sorry ≫
          Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n sorry =
      Cochain.v (inl f) (n + 2) (n + 1) sorry ≫
        Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n sorry ≫
          (-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₁))
                            sorry)
                          (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
                        sorry)
                      sorry)
                    (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₁) sorry)
                      (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                        (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
                      sorry) +
                Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
            n n sorry ∧
    HomologicalComplex.Hom.f (inr f) (n + 1) ≫
        Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n sorry ≫
          Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n sorry =
      HomologicalComplex.Hom.f (inr f) (n + 1) ≫
        Cochain.v (inl (mappingConeCompTriangle f g).mor₁) (n + 1) n sorry ≫
          (-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₁))
                            sorry)
                          (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
                        sorry)
                      sorry)
                    (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₁) sorry)
                      (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                        (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
                      sorry) +
                Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
            n n sorry) ∧
  Cochain.v (inl (f ≫ g)) (n + 1) n sorry ≫
        HomologicalComplex.Hom.f (inr (mappingConeCompTriangle f g).mor₁) n ≫
          Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n sorry =
      Cochain.v (inl (f ≫ g)) (n + 1) n sorry ≫
        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₁))
                            sorry)
                          (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
                        sorry)
                      sorry)
                    (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₁) sorry)
                      (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                        (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
                      sorry) +
                Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
            n n sorry ∧
    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 sorry =
      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₁))
                            sorry)
                          (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
                        sorry)
                      sorry)
                    (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₁) sorry)
                      (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                        (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
                      sorry) +
                Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
            n n sorry
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)]