-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorCompIsoId_add'_hom_app :
    (shiftFunctorCompIsoId C p' p hp).hom.app X =
      ((shiftFunctorAdd' C n' m' p'
          (by rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn])).hom.app X)⟦p⟧' ≫
      (shiftFunctorAdd' C m n p h).hom.app (X⟦n'⟧⟦m'⟧) ≫
      (shiftFunctorCompIsoId C m' m hm).hom.app (X⟦n'⟧)⟦n⟧' ≫
      (shiftFunctorCompIsoId C n' n hn).hom.app X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' = p'

Tactic:
rw [← add_left_inj p, hp, ← h, add_assoc,
← add_assoc m', hm, zero_add, hn]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift 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
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map (𝟙 ((shiftFunctor C m).obj ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)))) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app 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]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift 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
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map (𝟙 ((shiftFunctor C m' ⋙ shiftFunctor C m).obj ((shiftFunctor C n').obj X))) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift 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
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map (𝟙 ((shiftFunctor C m).obj ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)))) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift 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
⊢ (shiftFunctorCompIsoId C p' p hp).hom.app X =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorCompIsoId C n' n hn).hom.app X

Tactic:
rw [← cancel_mono ((shiftFunctorCompIsoId C p' p hp).inv.app X), Iso.hom_inv_id_app,
  shiftFunctorCompIsoId_add'_inv_app m n p m' n' p' hm hn hp h,
  Category.assoc, Category.assoc, Category.assoc, Iso.hom_inv_id_app_assoc,
  ← Functor.map_comp_assoc, Iso.hom_inv_id_app]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift 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
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map (𝟙 ((shiftFunctor C m' ⋙ shiftFunctor C m).obj ((shiftFunctor C n').obj X))) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)