Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl,
      mapHomologicalComplexXIso_eq φ H (n + 1) (n + 2) (by lia),
      mapHomologicalComplexXIso'_hom, mapHomologicalComplexXIso'_hom]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (H.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
          H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (H.map ((↑(fst φ)).v (n + 1) (n + 2) ⋯) ≫
              (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 2) (n + 1) ⋯ +
            H.map ((snd φ).v (n + 1) (n + 1) ⋯) ≫
              (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f (n + 1)) ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (H.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
          H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
        ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (H.map ((↑(fst φ)).v (n + 1) (n + 2) ⋯) ≫
              (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 2) (n + 1) ⋯ +
            H.map ((snd φ).v (n + 1) (n + 1) ⋯) ≫
              (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f (n + 1)) ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯