-- 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 : ℤ
left :
  HAdd.hAdd (α :=
        H.obj ((mappingCone φ).X n) ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n (n + 1) ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
        (H.map (Cochain.v (snd φ) n n ⋯) ≫
          Hom.f (inr (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)) =
    d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
      HAdd.hAdd (α :=
          H.obj ((mappingCone φ).X (n + 1)) ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              (n + 1))
          (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) (n + 1) (n + 2) ⋯) ≫
            Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 2) (n + 1)
              ⋯)
          (H.map (Cochain.v (snd φ) (n + 1) (n + 1) ⋯) ≫
            Hom.f (inr (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) ⋯
right :
  HAdd.hAdd (α :=
        H.obj ((mappingCone φ).X n) ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n (n + 1) ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
        (H.map (Cochain.v (snd φ) n n ⋯) ≫
          Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) 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)) =
    d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
      HAdd.hAdd (α :=
          H.obj ((mappingCone φ).X (n + 1)) ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              (n + 1))
          (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) (n + 1) (n + 2) ⋯) ≫
            Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 2) (n + 1)
              ⋯)
          (H.map (Cochain.v (snd φ) (n + 1) (n + 1) ⋯) ≫
            Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1)) ≫
        Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) (n + 1) ⋯
⊢ HAdd.hAdd (α :=
          H.obj ((mappingCone φ).X n) ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              n)
          (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n (n + 1) ⋯) ≫
            Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
          (H.map (Cochain.v (snd φ) n n ⋯) ≫
            Hom.f (inr (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)) =
      d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
        HAdd.hAdd (α :=
            H.obj ((mappingCone φ).X (n + 1)) ⟶
              X
                (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                  (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                (n + 1))
            (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) (n + 1) (n + 2) ⋯) ≫
              Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 2)
                (n + 1) ⋯)
            (H.map (Cochain.v (snd φ) (n + 1) (n + 1) ⋯) ≫
              Hom.f (inr (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) ⋯ ∧
    HAdd.hAdd (α :=
          H.obj ((mappingCone φ).X n) ⟶
            X
              (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
              n)
          (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n (n + 1) ⋯) ≫
            Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
          (H.map (Cochain.v (snd φ) n n ⋯) ≫
            Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) 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)) =
      d (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n (n + 1) ≫
        HAdd.hAdd (α :=
            H.obj ((mappingCone φ).X (n + 1)) ⟶
              X
                (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
                  (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
                (n + 1))
            (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) (n + 1) (n + 2) ⋯) ≫
              Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 2)
                (n + 1) ⋯)
            (H.map (Cochain.v (snd φ) (n + 1) (n + 1) ⋯) ≫
              Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1)) ≫
          Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) (n + 1) ⋯

Tactic:
constructor