-- Mathlib/CategoryTheory/Shift/CommShift.lean
/--
Assume that we have a diagram of categories
```
C₁ ⥤ D₁
‖     ‖
v     v
C₂ ⥤ D₂
‖     ‖
v     v
C₃ ⥤ D₃
```
with functors `F₁₂ : C₁ ⥤ C₂`, `F₂₃ : C₂ ⥤ C₃` and `F₁₃ : C₁ ⥤ C₃` on the first
column that are related by a natural transformation `α : F₁₃ ⟶ F₁₂ ⋙ F₂₃`
and similarly `β : G₁₂ ⋙ G₂₃ ⟶ G₁₃` on the second column. Assume that we have
natural transformations
`e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂` (top square), `e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃` (bottom square),
and `e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃` (outer square), where the horizontal functors
are denoted `L₁`, `L₂` and `L₃`. Assume that `e₁₃` is determined by the other
natural transformations `α`, `e₂₃`, `e₁₂` and `β`. Then, if all these categories
are equipped with a shift by an additive monoid `A`, and all these functors commute with
these shifts, then the natural transformation `e₁₃` of the outer square commutes with the
shift if all `α`, `e₂₃`, `e₁₂` and `β` do. -/
lemma NatTrans.CommShift.verticalComposition {C₁ C₂ C₃ D₁ D₂ D₃ : Type*}
    [Category C₁] [Category C₂] [Category C₃] [Category D₁] [Category D₂] [Category D₃]
    {F₁₂ : C₁ ⥤ C₂} {F₂₃ : C₂ ⥤ C₃} {F₁₃ : C₁ ⥤ C₃} (α : F₁₃ ⟶ F₁₂ ⋙ F₂₃)
    {G₁₂ : D₁ ⥤ D₂} {G₂₃ : D₂ ⥤ D₃} {G₁₃ : D₁ ⥤ D₃} (β : G₁₂ ⋙ G₂₃ ⟶ G₁₃)
    {L₁ : C₁ ⥤ D₁} {L₂ : C₂ ⥤ D₂} {L₃ : C₃ ⥤ D₃}
    (e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂) (e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃) (e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃)
    (A : Type*) [AddMonoid A] [HasShift C₁ A] [HasShift C₂ A] [HasShift C₃ A]
    [HasShift D₁ A] [HasShift D₂ A] [HasShift D₃ A]
    [F₁₂.CommShift A] [F₂₃.CommShift A] [F₁₃.CommShift A] [CommShift α A]
    [G₁₂.CommShift A] [G₂₃.CommShift A] [G₁₃.CommShift A] [CommShift β A]
    [L₁.CommShift A] [L₂.CommShift A] [L₃.CommShift A]
    [CommShift e₁₂ A] [CommShift e₂₃ A]
    (h₁₃ : e₁₃ = CategoryTheory.whiskerRight α L₃ ≫ (Functor.associator _ _ _).hom ≫
      CategoryTheory.whiskerLeft F₁₂ e₂₃ ≫ (Functor.associator _ _ _).inv ≫
        CategoryTheory.whiskerRight e₁₂ G₂₃ ≫ (Functor.associator _ _ _).hom ≫
          CategoryTheory.whiskerLeft L₁ β) : CommShift e₁₃ A

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{u_8, u_1} C₁
inst✝²⁴ : Category.{u_9, u_2} C₂
inst✝²³ : Category.{u_10, u_3} C₃
inst✝²² : Category.{u_11, u_4} D₁
inst✝²¹ : Category.{u_12, u_5} D₂
inst✝²⁰ : Category.{u_13, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
⊢ CommShift
    (CategoryTheory.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        CategoryTheory.whiskerLeft F₁₂ e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫
            CategoryTheory.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ CategoryTheory.whiskerLeft L₁ β)
    A

Tactic:
infer_instance

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{u_8, u_1} C₁
inst✝²⁴ : Category.{u_9, u_2} C₂
inst✝²³ : Category.{u_10, u_3} C₃
inst✝²² : Category.{u_11, u_4} D₁
inst✝²¹ : Category.{u_12, u_5} D₂
inst✝²⁰ : Category.{u_13, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    CategoryTheory.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        CategoryTheory.whiskerLeft F₁₂ e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫
            CategoryTheory.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ CategoryTheory.whiskerLeft L₁ β
⊢ CommShift e₁₃ A

Tactic:
subst h₁₃

Result:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{u_8, u_1} C₁
inst✝²⁴ : Category.{u_9, u_2} C₂
inst✝²³ : Category.{u_10, u_3} C₃
inst✝²² : Category.{u_11, u_4} D₁
inst✝²¹ : Category.{u_12, u_5} D₂
inst✝²⁰ : Category.{u_13, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
⊢ CommShift
    (CategoryTheory.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        CategoryTheory.whiskerLeft F₁₂ e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫
            CategoryTheory.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ CategoryTheory.whiskerLeft L₁ β)
    A