-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) (a + b)) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D (a + b)) ((lift r F hF).obj ((functor r).obj X)))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF (a + b))) ((functor r).obj X))
    (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
      ((functor r).obj X))
have w : Eq (α :=
  (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) (a + b)) ((functor r).obj X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor D (a + b)) ((lift r F hF).obj ((functor r).obj X)))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorAdd (Quotient r) a b)) ((functor r).obj X)) ≫
    CategoryStruct.comp (Y :=
      (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) b) ((shiftFunctor C a ⋙ functor r).obj X)))
      ((lift r F hF).map
        (Functor.map (shiftFunctor (Quotient r) b) (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 := (F ⋙ shiftFunctor D b).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) 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))))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorAdd (Quotient r) a b)) ((functor r).obj X)) ≫
    CategoryStruct.comp (Y :=
      (lift r F hF ⋙ shiftFunctor D b).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) a) ((functor r).obj X)))
      (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF b))
        (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) a) ((functor r).obj X)))
      (Functor.map (shiftFunctor D b)
          (CategoryStruct.comp (Y := (lift r F hF).obj ((shiftFunctor C a ⋙ functor r).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)) ((lift r F hF).obj ((functor r).obj X))))
Tactic: rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_add, F.commShiftIso_add,
      Functor.CommShift.isoAdd_hom_app, Functor.CommShift.isoAdd_hom_app,
      Functor.CommShift.isoAdd_inv_app, Functor.map_comp, Functor.map_comp,
      Functor.map_comp, assoc, assoc, assoc, LiftCommShift.iso_hom_app, lift_map_functor_map]