-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
w :
  Eq (α :=
    ((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X ⟶
      (F ⋙ shiftFunctor D (a + b)).obj X)
    (CategoryStruct.comp (Y :=
      ((functor r ⋙ shiftFunctor (Quotient r) a) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X)
      ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
      (CategoryStruct.comp (Y := (((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b) ⋙ lift r F hF).obj X)
        ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
          (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
        ((lift r F hF).map
            (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) b))
              (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
            F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
              CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F ⋙ shiftFunctor D b).obj X)
                (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
                (Functor.map (shiftFunctor D b) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF b)) ((shiftFunctor C a ⋙ functor r).obj X) ≫
      CategoryStruct.comp (Y := (lift r F hF ⋙ shiftFunctor D b).obj ((functor r ⋙ shiftFunctor (Quotient r) a).obj X))
        ((lift r F hF ⋙ shiftFunctor D b).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
        (Functor.map (shiftFunctor D b)
            (CategoryStruct.comp (Y := ((shiftFunctor C a ⋙ functor r) ⋙ lift r F hF).obj X)
              ((lift r F hF).map (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
              (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) ((functor r ⋙ lift r F hF).obj X)))
⊢ Eq (α :=
    ((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X ⟶
      (F ⋙ shiftFunctor D (a + b)).obj X)
    (CategoryStruct.comp (Y :=
      ((functor r ⋙ shiftFunctor (Quotient r) a) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X)
      ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
      (CategoryStruct.comp (Y := (((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b) ⋙ lift r F hF).obj X)
        ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
          (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
        ((lift r F hF).map
            (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) b))
              (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
            F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
              CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F ⋙ shiftFunctor D b).obj X)
                (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
                (Functor.map (shiftFunctor D b) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
    (CategoryStruct.comp (Y :=
      ((functor r ⋙ shiftFunctor (Quotient r) a) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X)
      ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
      (CategoryStruct.comp (Y := ((functor r ⋙ shiftFunctor (Quotient r) a) ⋙ lift r F hF ⋙ shiftFunctor D b).obj X)
        (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF b)) ((functor r ⋙ shiftFunctor (Quotient r) a).obj X))
        (Functor.map (shiftFunctor D b)
            (CategoryStruct.comp (Y := ((shiftFunctor C a ⋙ functor r) ⋙ lift r F hF).obj X)
              ((lift r F hF).map (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
              (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) ((functor r ⋙ lift r F hF).obj X))))

Tactic:
rw [(LiftCommShift.iso F r hF b).hom.naturality_assoc (((functor r).commShiftIso a).hom.app X)]

Premises used: CategoryTheory.Quotient.LiftCommShift.iso, CategoryTheory.Quotient.functor, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc