-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 m : ℤ
hnm : n + 1 = m
⊢ HAdd.hAdd (α :=
        X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n ⟶
          H.obj ((mappingCone φ).X 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 m ⋯ ≫
          H.map (Cochain.v (inl φ) m n ⋯))
        (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n ⋯ ≫
          H.map (Hom.f (inr φ) n)) ≫
      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 m ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n ⋯)
        (H.map (Cochain.v (snd φ) n n ⋯) ≫
          Hom.f (inr (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)
have simp : HAdd.hAdd (α :=
      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)
      (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 m sorry ≫
        Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n sorry)
      (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n sorry ≫
        CategoryStruct.comp (Y := H.obj (F.X m)) (H.map 0)
          (Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n sorry)) +
    HAdd.hAdd (α :=
      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)
      (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 m sorry ≫
        CategoryStruct.comp (Y := H.obj (G.X n)) (H.map 0)
          (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n))
      (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n sorry ≫
        Hom.f (inr (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)
Tactic: simp only [Functor.mapHomologicalComplex_obj_X, comp_add, add_comp, assoc,
      ← H.map_comp_assoc, inl_v_fst_v, CategoryTheory.Functor.map_id, id_comp, inr_f_fst_v,
      inl_v_snd_v, inr_f_snd_v]