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 (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 ⋯

Tactic:
dsimp [hom, inv]

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 (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 ⋯)