-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_assoc (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
    (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
    shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃]) ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) _ ≪≫ Functor.associator _ _ _ =
    shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃]) ≪≫
      isoWhiskerLeft _ (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      (Functor.LaxMonoidal.μ (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorObj { as := a₁ } { as := a₂ })
              { as := a₃ }).app
          X ≫
        eqToHom ⋯ ≫
          (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
                  (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
              X ≫
            (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
              (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    (eqToHom ⋯ ≫ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Tactic:
erw [δ_μ_app_assoc, Category.assoc]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    eqToHom ⋯ ≫
      (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X ≫
        (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯).hom.app X) ≫
        𝟙 ((shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X))) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.comp_id]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    ((eqToHom ⋯).app X ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
simp only [eqToHom_app]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (eqToHom ⋯ ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
              (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app
      X =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)).hom.app
      X

Tactic:
dsimp

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯).hom.app X) ≫
        𝟙 ((shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X))) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯).hom.app ((shiftFunctor C a₁).obj X)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
dsimp [shiftFunctorAdd']

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    ((eqToHom ⋯).app X ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)