-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ (mappingConeCompTriangleh f g).mor₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom (Iso.refl (mappingConeCompTriangleh f g).obj₁)) =
    Iso.hom (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)) ≫
      (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₃
have dsimp : Eq (α :=
  Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
  (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (mappingCone f)))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        ((mappingCone.triangle g).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (mappingCone.inr f)))
      (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)) ≫
    CategoryTheory.Functor.map
      (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (𝟙 (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
  (CategoryStruct.comp (Y :=
    Functor.obj (quotient C (ComplexShape.up ℤ))
      (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
        (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)) :
      Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
        Functor.obj (quotient C (ComplexShape.up ℤ))
          (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
            (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f) :
      Functor.obj (quotient C (ComplexShape.up ℤ))
          (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
            (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))) ⟶
        Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
Tactic: dsimp [mappingConeCompTriangleh]