Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
          (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
              (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
            (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
              ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl
            (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
                (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
                    (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
                  (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
                    ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).obj₁).hom =
    (Iso.refl
          (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
              (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
                  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
                (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
                  ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).obj₃).hom ≫
      (mappingConeCompTriangleh u₁₂ u₂₃).mor₃

Tactic:
dsimp [mappingConeCompTriangleh]

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X₂) ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (mappingCone.inr u₁₂))) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((quotient C (ComplexShape.up ℤ)).obj (mappingCone u₁₂))) =
    𝟙 ((quotient C (ComplexShape.up ℤ)).obj (mappingCone u₂₃)) ≫
      (quotient C (ComplexShape.up ℤ)).map
          ((mappingCone.triangle u₂₃).mor₃ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr u₁₂)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone u₁₂)