-- 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 (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 ⋯
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp [hom, inv]