-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
rw :
  Eq (α :=
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 2))
      (CategoryStruct.comp (Y :=
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
          (Iso.hom (mapHomologicalComplexXIso φ H n) :
            X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
              X
                (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                  (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                n)
          (-Cochain.v
                  (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
                    Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
                  n (n + 1) ⋯ ≫
                d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 1) (n + 2) :
            X
                (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                  (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                n ⟶
              X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 2)) :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
          X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 2))
      (d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
          CategoryStruct.comp (Y :=
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              (n + 1))
            (Iso.hom (mapHomologicalComplexXIso φ H (n + 1)) :
              X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) (n + 1) ⟶
                X
                  (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                  (n + 1))
            (Cochain.v
                (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
                  Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
                (n + 1) (n + 2) ⋯ :
              X
                  (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                  (n + 1) ⟶
                X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 2)) :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
          X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F) (n + 2)) ∧
    Eq (α :=
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) (n + 1))
      (Iso.hom (mapHomologicalComplexXIso φ H n) ≫
          HAdd.hAdd (α :=
            X
                (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                  (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                n ⟶
              X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) (n + 1))
            (Cochain.v
                (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
                  Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
                n (n + 1) ⋯ ≫
              Hom.f (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ) (n + 1))
            (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n ⋯ ≫
              d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n (n + 1)) :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
          X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) (n + 1))
      (d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
          CategoryStruct.comp (Y :=
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              (n + 1))
            (Iso.hom (mapHomologicalComplexXIso φ H (n + 1)) :
              X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) (n + 1) ⟶
                X
                  (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                  (n + 1))
            (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1)
                (n + 1) ⋯ :
              X
                  (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                  (n + 1) ⟶
                X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) (n + 1)) :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
          X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) (n + 1))
⊢ Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        (n + 1))
    (CategoryStruct.comp (Y :=
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
        (Iso.hom (mapHomologicalComplexXIso φ H n) :
          X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              n)
        (d
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n (n + 1) :
          X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              n ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              (n + 1)) :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          (n + 1))
    (d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
        Iso.hom (mapHomologicalComplexXIso φ H (n + 1)) :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          (n + 1))

Tactic:
rw [ext_to_iff _ _ (n + 2) (by lia), assoc, assoc, d_fst_v _ _ _ _ rfl,
      assoc, assoc, d_snd_v _ _ _ rfl]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.d_snd_v, CochainComplex.mappingCone.ext_to_iff, HAdd.hAdd, OfNat.ofNat, rfl, CochainComplex.mappingCone.d_fst_v