-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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))
⊢ 𝟙 (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)
have 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)))
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]