-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
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)))
⊢ 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)))
have 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))
Tactic: rw [← Functor.map_smul, ← h₁, ← h₂]