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:
rw [ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 1) n rfl,
        ext_from_iff _ (n + 2) (n + 1) (by lia)]

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 f).v (n + 2) (n + 1) ⋯ ≫
          (inl (mappingConeCompTriangle f g).mor₁).v (n + 1) n ⋯ ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
        (inl f).v (n + 2) (n + 1) ⋯ ≫
          (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 f).f (n + 1) ≫
          (inl (mappingConeCompTriangle f g).mor₁).v (n + 1) n ⋯ ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
        (inr f).f (n + 1) ≫
          (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 ⋯) ∧
    (inl (f ≫ g)).v (n + 1) n ⋯ ≫
          (inr (mappingConeCompTriangle f g).mor₁).f n ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
        (inl (f ≫ g)).v (n + 1) 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 ⋯ ∧
      (inr (f ≫ g)).f n ≫ (inr (mappingConeCompTriangle f g).mor₁).f n ≫ (Cochain.ofHom (inv f g ≫ hom f g)).v n n ⋯ =
        (inr (f ≫ g)).f 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 ⋯