-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc]
lemma mappingConeCompTriangle_mor₃_naturality {Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂)
    (g' : Y₂ ⟶ Y₃) (φ : mk₂ f g ⟶ mk₂ f' g') :
    map g g' (φ.app 1) (φ.app 2) (naturality' φ 1 2) ≫ (mappingConeCompTriangle f' g').mor₃ =
      (mappingConeCompTriangle f g).mor₃ ≫
        (map f f' (φ.app 0) (φ.app 1) (naturality' φ 0 1))⟦1⟧'

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃).f n =
    ((mappingConeCompTriangle f g).mor₃ ≫
          (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)).f
      n

Tactic:
dsimp [map]

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (desc g ((Cochain.ofHom (φ.app 1)).comp (inl g') map.proof_4) (φ.app 2 ≫ inr g') ⋯).f n ≫
      (triangle g').mor₃.f n ≫ (inr f').f (n + 1) =
    ((triangle g).mor₃.f n ≫ (inr f).f (n + 1)) ≫
      (desc f ((Cochain.ofHom (φ.app 0)).comp (inl f') map.proof_4) (φ.app 1 ≫ inr f') ⋯).f (n + 1)

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (desc g ((Cochain.ofHom (φ.app 1)).comp (inl g') map.proof_4) (φ.app 2 ≫ inr g') ⋯).f n ≫
      (triangle g').mor₃.f n ≫ (inr f').f (n + 1) =
    ((triangle g).mor₃.f n ≫ (inr f).f (n + 1)) ≫
      (desc f ((Cochain.ofHom (φ.app 0)).comp (inl f') map.proof_4) (φ.app 1 ≫ inr f') ⋯).f (n + 1)

Tactic:
simp only [Int.reduceNeg, Fin.isValue, assoc, inr_f_desc_f, HomologicalComplex.comp_f,
  ext_from_iff _ (n + 1) _ rfl, inl_v_desc_f_assoc, Cochain.zero_cochain_comp_v, Cochain.ofHom_v,
  inl_v_triangle_mor₃_f_assoc, triangle_obj₁, shiftFunctor_obj_X', shiftFunctor_obj_X,
  shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, Preadditive.neg_comp,
  id_comp, Preadditive.comp_neg, inr_f_desc_f_assoc, inr_f_triangle_mor₃_f_assoc, zero_comp,
  comp_zero, and_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
⊢ map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃ =
    (mappingConeCompTriangle f g).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃).f n =
    ((mappingConeCompTriangle f g).mor₃ ≫
          (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)).f
      n