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 : ℤ
⊢ (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 ⋯ ∧
    (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 ⋯

Tactic:
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 ⋯