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 : ℤ
⊢ (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) ⋯

Tactic:
constructor

Goal state after:
case left
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)

case right
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 ℤ)).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) ⋯