Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
    (-((snd (mappingConeCompTriangle f g).mor₁).comp
                ((↑(fst (f ≫ g))).comp
                  ((inl f).comp
                      (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                    -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                  ⋯)
                ⋯ +
              ((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁)
                    ⋯).comp
                ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                  ⋯)
                ⋯) +
          Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
      n n ⋯

Tactic:
ext_from_iff _ (n + 1) n rfl,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ (inl (mappingConeCompTriangle f g).mor₁).v (n + 1) n ⋯ ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
      (inl (mappingConeCompTriangle f g).mor₁).v (n + 1) n ⋯ ≫
        (-((snd (mappingConeCompTriangle f g).mor₁).comp
                    ((↑(fst (f ≫ g))).comp
                      ((inl f).comp
                          (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                          ⋯ +
                        -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                      ⋯)
                    ⋯ +
                  ((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁)
                        ⋯).comp
                    ((↑(fst (f ≫ g))).comp
                      ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                    ⋯) +
              Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
          n n ⋯ ∧
    (inr (mappingConeCompTriangle f g).mor₁).f n ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
      (inr (mappingConeCompTriangle f g).mor₁).f n ≫
        (-((snd (mappingConeCompTriangle f g).mor₁).comp
                    ((↑(fst (f ≫ g))).comp
                      ((inl f).comp
                          (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁))
                          ⋯ +
                        -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                      ⋯)
                    ⋯ +
                  ((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁)
                        ⋯).comp
                    ((↑(fst (f ≫ g))).comp
                      ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
                    ⋯) +
              Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
          n n ⋯