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

Proof state:
case e_a
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
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)

Tactic:
rw [← cancel_mono ((shiftFunctorAdd' C p' p 0 hp).inv.app X), Iso.hom_inv_id_app,
  Category.assoc, Category.assoc, Category.assoc, Category.assoc,
  ← shiftFunctorAdd'_assoc_inv_app p' m n n' p 0
    (by rw [← add_left_inj n, hn, add_assoc, h, hp]) h (by rw [add_assoc, h, hp]),
  ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc,
  Category.assoc, Category.assoc,
  shiftFunctorAdd'_assoc_inv_app n' m' m p' 0 n' _ _
    (by rw [add_assoc, hm, add_zero]), Iso.hom_inv_id_app_assoc,
  ← shiftFunctorAdd'_add_zero_hom_app, Iso.hom_inv_id_app,
  Functor.map_id, Category.id_comp, Iso.hom_inv_id_app]

Result:
no goals

Proof state:
case e_a
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
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C m ⋙ shiftFunctor C n).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)

Tactic:
dsimp

Result:
case e_a
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
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj 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
⊢ p' + m = n'

Tactic:
rw [← add_left_inj n, hn, add_assoc, h, hp]

Result:
no goals