-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (hypothesis)
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 (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
      Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        Y)
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
        X)
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)) f ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map
      (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) 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 h₂ : Eq (α :=
  Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
    Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) Y)
  (CategoryStruct.comp (Y :=
    Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
      X)
    (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
    (CategoryTheory.Functor.map
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)) (r • f) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
  (CategoryTheory.Functor.map
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f))
Tactic: have h₂ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) (r • f)