-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  Eq (α :=
    Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) X) ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) Y))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) X))
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) f) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f))
h₂ :
  Eq (α :=
    Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) X) ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) Y))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) X))
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f)) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (r • f)))
rw :
  CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) X))
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f)) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r
      (CategoryStruct.comp (Y :=
          Functor.obj (quotient C (ComplexShape.up ℤ))
            (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) X))
          (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) f) ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y) :
        Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (Functor.obj (quotient C (ComplexShape.up ℤ)) X) ⟶
          Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (Functor.obj (quotient C (ComplexShape.up ℤ)) Y))
⊢ CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (HSMul.hSMul (β :=
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
        r
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f :
          Functor.obj (quotient C (ComplexShape.up ℤ)) X ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) Y)) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) :
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))

Tactic:
rw [← Functor.map_smul, ← h₁, ← h₂]

Premises used: CategoryTheory.Functor.map_smul