-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.mk : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D] →
            {M : Type u_6} →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : CategoryTheory.HasShift C₁ M] →
                  [inst_5 : CategoryTheory.HasShift C₂ M] →
                    [inst_6 : CategoryTheory.HasShift D M] →
                      {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                        {h : CategoryTheory.CommShift₂Setup D M} →
                          (commShiftObj :
                              autoParam ((X₁ : C₁) → (G.obj X₁).CommShift M)
                                CategoryTheory.Functor.CommShift₂.commShiftObj._autoParam) →
                            autoParam (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁), CategoryTheory.NatTrans.CommShift (G.map f) M)
                                CategoryTheory.Functor.CommShift₂.commShift_map._autoParam →
                              (commShiftFlipObj :
                                  autoParam ((X₂ : C₂) → (G.flip.obj X₂).CommShift M)
                                    CategoryTheory.Functor.CommShift₂.commShiftFlipObj._autoParam) →
                                autoParam
                                    (∀ {X₂ Y₂ : C₂} (g : X₂ ⟶ Y₂), CategoryTheory.NatTrans.CommShift (G.flip.map g) M)
                                    CategoryTheory.Functor.CommShift₂.commShift_flip_map._autoParam →
                                  (∀ (X₁ : C₁) (X₂ : C₂) (m n : M),
                                      CategoryTheory.CategoryStruct.comp
                                          ((CategoryTheory.Functor.commShiftIso
                                                  (G.obj ((CategoryTheory.shiftFunctor C₁ m).obj X₁)) n).hom.app
                                            X₂)
                                          ((CategoryTheory.shiftFunctor D n).map
                                            ((CategoryTheory.Functor.commShiftIso (G.flip.obj X₂) m).hom.app X₁)) =
                                        CategoryTheory.CategoryStruct.comp
                                          ((CategoryTheory.Functor.commShiftIso
                                                  (G.flip.obj ((CategoryTheory.shiftFunctor C₂ n).obj X₂)) m).hom.app
                                            X₁)
                                          (CategoryTheory.CategoryStruct.comp
                                            ((CategoryTheory.shiftFunctor D m).map
                                              ((CategoryTheory.Functor.commShiftIso (G.obj X₁) n).hom.app X₂))
                                            (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.shiftComm ((G.obj X₁).obj X₂) m n).inv
                                              ((↑(h.ε m n)).app
                                                ((CategoryTheory.shiftFunctor D n).obj
                                                  ((CategoryTheory.shiftFunctor D m).obj ((G.obj X₁).obj X₂))))))) →
                                    G.CommShift₂ h