-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        𝟙
            (obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₁ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₂ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₃ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₄ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (𝟙 (obj.{v, v, u, u} (shiftFunctor C p') X))
rw₅ rw₆ :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X) ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)))
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)))
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)

Tactic:
rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp