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 f).v (n + 2) (n + 1) ⋯ ≫
          (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)).v (n + 1) n ⋯ ≫
            (Cochain.ofHom
                  (desc (map f (f ≫ g) (𝟙 X₁) g ⋯) ((snd f).comp (inl g) inv._proof_5)
                      (desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) inv._proof_5) (inr g) ⋯) ⋯ ≫
                    lift (map f (f ≫ g) (𝟙 X₁) g ⋯) (descCocycle g (Cochain.ofHom (inr f)) 0 hom._proof_6 ⋯)
                      (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) hom._proof_7) ⋯)).v
              n n ⋯ =
        (inl f).v (n + 2) (n + 1) ⋯ ≫
          (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)).v (n + 1) n ⋯ ≫
            (-(((snd (map f (f ≫ g) (𝟙 X₁) g ⋯)).comp
                        ((↑(fst (f ≫ g))).comp
                          ((inl f).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯ ≫ inr (map f (f ≫ g) (𝟙 X₁) g ⋯))) ⋯ +
                            -(Cochain.ofHom (f ≫ inr f)).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯)
                          ⋯)
                        ⋯).v
                    n n ⋯ +
                  (((↑(fst (map f (f ≫ g) (𝟙 X₁) g ⋯))).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯).comp
                        ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) homotopyInvHomId._proof_1)
                          ⋯)
                        ⋯).v
                    n n ⋯) +
              (Cochain.ofHom (𝟙 (mappingCone (map f (f ≫ g) (𝟙 X₁) g ⋯)))).v n n ⋯) ∧
      (inr f).f (n + 1) ≫
          (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)).v (n + 1) n ⋯ ≫
            (Cochain.ofHom
                  (desc (map f (f ≫ g) (𝟙 X₁) g ⋯) ((snd f).comp (inl g) inv._proof_5)
                      (desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) inv._proof_5) (inr g) ⋯) ⋯ ≫
                    lift (map f (f ≫ g) (𝟙 X₁) g ⋯) (descCocycle g (Cochain.ofHom (inr f)) 0 hom._proof_6 ⋯)
                      (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) hom._proof_7) ⋯)).v
              n n ⋯ =
        (inr f).f (n + 1) ≫
          (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)).v (n + 1) n ⋯ ≫
            (-(((snd (map f (f ≫ g) (𝟙 X₁) g ⋯)).comp
                        ((↑(fst (f ≫ g))).comp
                          ((inl f).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯ ≫ inr (map f (f ≫ g) (𝟙 X₁) g ⋯))) ⋯ +
                            -(Cochain.ofHom (f ≫ inr f)).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯)
                          ⋯)
                        ⋯).v
                    n n ⋯ +
                  (((↑(fst (map f (f ≫ g) (𝟙 X₁) g ⋯))).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯).comp
                        ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) homotopyInvHomId._proof_1)
                          ⋯)
                        ⋯).v
                    n n ⋯) +
              (Cochain.ofHom (𝟙 (mappingCone (map f (f ≫ g) (𝟙 X₁) g ⋯)))).v n n ⋯)) ∧
    (inl (f ≫ g)).v (n + 1) n ⋯ ≫
          (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)).f n ≫
            (Cochain.ofHom
                  (desc (map f (f ≫ g) (𝟙 X₁) g ⋯) ((snd f).comp (inl g) inv._proof_5)
                      (desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) inv._proof_5) (inr g) ⋯) ⋯ ≫
                    lift (map f (f ≫ g) (𝟙 X₁) g ⋯) (descCocycle g (Cochain.ofHom (inr f)) 0 hom._proof_6 ⋯)
                      (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) hom._proof_7) ⋯)).v
              n n ⋯ =
        (inl (f ≫ g)).v (n + 1) n ⋯ ≫
          (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)).f n ≫
            (-(((snd (map f (f ≫ g) (𝟙 X₁) g ⋯)).comp
                        ((↑(fst (f ≫ g))).comp
                          ((inl f).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯ ≫ inr (map f (f ≫ g) (𝟙 X₁) g ⋯))) ⋯ +
                            -(Cochain.ofHom (f ≫ inr f)).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯)
                          ⋯)
                        ⋯).v
                    n n ⋯ +
                  (((↑(fst (map f (f ≫ g) (𝟙 X₁) g ⋯))).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯).comp
                        ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) homotopyInvHomId._proof_1)
                          ⋯)
                        ⋯).v
                    n n ⋯) +
              (Cochain.ofHom (𝟙 (mappingCone (map f (f ≫ g) (𝟙 X₁) g ⋯)))).v n n ⋯) ∧
      (inr (f ≫ g)).f n ≫
          (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)).f n ≫
            (Cochain.ofHom
                  (desc (map f (f ≫ g) (𝟙 X₁) g ⋯) ((snd f).comp (inl g) inv._proof_5)
                      (desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) inv._proof_5) (inr g) ⋯) ⋯ ≫
                    lift (map f (f ≫ g) (𝟙 X₁) g ⋯) (descCocycle g (Cochain.ofHom (inr f)) 0 hom._proof_6 ⋯)
                      (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) hom._proof_7) ⋯)).v
              n n ⋯ =
        (inr (f ≫ g)).f n ≫
          (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)).f n ≫
            (-(((snd (map f (f ≫ g) (𝟙 X₁) g ⋯)).comp
                        ((↑(fst (f ≫ g))).comp
                          ((inl f).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯ ≫ inr (map f (f ≫ g) (𝟙 X₁) g ⋯))) ⋯ +
                            -(Cochain.ofHom (f ≫ inr f)).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯)
                          ⋯)
                        ⋯).v
                    n n ⋯ +
                  (((↑(fst (map f (f ≫ g) (𝟙 X₁) g ⋯))).comp (Cochain.ofHom (map f (f ≫ g) (𝟙 X₁) g ⋯)) ⋯).comp
                        ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (map f (f ≫ g) (𝟙 X₁) g ⋯)) homotopyInvHomId._proof_1)
                          ⋯)
                        ⋯).v
                    n n ⋯) +
              (Cochain.ofHom (𝟙 (mappingCone (map f (f ≫ g) (𝟙 X₁) g ⋯)))).v n n ⋯)

Tactic:
simp [ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _
          (add_neg_cancel 1) n (n + 1) n (by lia) (by lia),
        Cochain.comp_v _ _ (show 1 + -2 = -1 by decide) (n + 1) (n + 2) n
          (by lia) (by lia),
        Cochain.comp_v _ _ (show (-1) + -1 = -2 by decide) (n + 2) (n + 1) n
          (by lia) (by lia)]

Goal state after: