-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [toMonoidalRightActionStruct : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            autoParam
                (∀ {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d' g))
                CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def._autoParam →
              autoParam
                  (∀ (c : C) (d : D),
                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                        (CategoryTheory.CategoryStruct.id c) =
                      CategoryTheory.CategoryStruct.id
                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c))
                  CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id._autoParam →
                autoParam
                    (∀ (c : C) (d : D),
                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                          (CategoryTheory.CategoryStruct.id d) c =
                        CategoryTheory.CategoryStruct.id
                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c))
                    CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft._autoParam →
                  autoParam
                      (∀ {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d') (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c''),
                        CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                            (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₁ g₁)
                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₂ g₂))
                      CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp._autoParam →
                    autoParam
                        (∀ {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂ c₄).hom =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁ c₃).hom
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h))
                        CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality._autoParam →
                      autoParam
                          (∀ {d d' : D} (f : d ⟶ d'),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom f =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').hom)
                          CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality._autoParam →
                        autoParam
                            (∀ {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D),
                              CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c) =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c' c).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f) c)
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c''
                                        c).inv))
                            CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight._autoParam →
                          autoParam
                              (∀ (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
                                CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                        c').hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) f)
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                          c'').inv))
                              CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft._autoParam →
                            autoParam
                                (∀ (c₁ c₂ c₃ : C) (d : D),
                                  CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom)
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁
                                            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃)).hom
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c₁)
                                            c₂ c₃).hom) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃).hom
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁
                                            c₂).hom
                                        c₃))
                                CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator._autoParam →
                              autoParam
                                  (∀ (c : C) (d : D),
                                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c).hom
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                              d).hom
                                          c))
                                  CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor._autoParam →
                                autoParam
                                    (∀ (c : C) (d : D),
                                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                                                c)).hom)
                                    CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor._autoParam →
                                  CategoryTheory.MonoidalCategory.MonoidalRightAction C D