-- 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:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
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₁₂₃ ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)

Tactic:
subst h₁₂ h₂₃ h₁₂₃

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ 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₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)

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 ≫
      ((shiftMonoidalFunctor C A).obj { as := a₃ }).map
        ((Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }).app 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:
simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map,
  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
⊢ (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)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
rw [← h₁₂, h₁₂₃]

Result:
no goals

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
⊢ 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:
rfl

Result:
no goals

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 ⋯ ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
dsimp [shiftFunctorAdd, shiftFunctor]

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
⊢ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      ((shiftMonoidalFunctor C A).obj { as := a₃ }).map
        ((Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }).app 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:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ 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₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)

Tactic:
ext X

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₃) ⋯ ≪≫
            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