-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma map_δ :
    (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
      NatTrans.app ((Functor.mapHomologicalComplex G (ComplexShape.up ℤ)).commShiftIso  1).hom K =
    (mapHomologicalComplexIso φ G).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (G.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        G.map ((snd φ).v n n ⋯) ≫ (inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n

Tactic:
simp only [Functor.mapHomologicalComplex_obj_X, add_comp, assoc, inl_v_triangle_mor₃_f,
  shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv,
  comp_neg, comp_id, inr_f_triangle_mor₃_f, comp_zero, add_zero]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (mapHomologicalComplexXIso φ G n).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n

Tactic:
rw [mapHomologicalComplexXIso_eq φ G n (n+1) rfl, mapHomologicalComplexXIso'_hom]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (G.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        G.map ((snd φ).v n n ⋯) ≫ (inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((-↑(fst φ)).v n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)

Tactic:
simp only [shiftFunctor_obj_X, Cochain.neg_v, shiftFunctorObjXIso,
  HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Functor.map_neg]

Result:
no goals

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
          ((G.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso 1).hom.app K).f
      n =
    ((mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃).f n

Tactic:
dsimp [mapHomologicalComplexIso]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    (mapHomologicalComplexXIso φ G n).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃.f n

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ n + 0 = n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ 0 + 1 = 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ n + 1 = n + 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
      ((G.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso 1).hom.app K =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Tactic:
ext n

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
          ((G.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso 1).hom.app K).f
      n =
    ((mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃).f n

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map (((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v n n ⋯) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)

Tactic:
rw [Cochain.rightShift_v _ 1 0 (by omega) n n (by omega) (n + 1) (by omega)]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((-↑(fst φ)).v n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)