-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.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] →
          [toMonoidalLeftActionStruct : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            autoParam
                (∀ {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d'),
                  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)
                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c' g))
                CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def._autoParam →
              autoParam
                  (∀ (c : C) (d : D),
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                        (CategoryTheory.CategoryStruct.id d) =
                      CategoryTheory.CategoryStruct.id
                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))
                  CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id._autoParam →
                autoParam
                    (∀ (c : C) (d : D),
                      CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                          (CategoryTheory.CategoryStruct.id c) d =
                        CategoryTheory.CategoryStruct.id
                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))
                    CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft._autoParam →
                  autoParam
                      (∀ {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c') (f₂ : c' ⟶ c'') (g₁ : d ⟶ d') (g₂ : d' ⟶ d''),
                        CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
                            (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₁ g₁)
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₂ g₂))
                      CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp._autoParam →
                    autoParam
                        (∀ {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).hom =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).hom
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h)))
                        CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality._autoParam →
                      autoParam
                          (∀ {d d' : D} (f : d ⟶ d'),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom f =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d').hom)
                          CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality._autoParam →
                        autoParam
                            (∀ (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
                              CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) d =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c''
                                        d).inv))
                            CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft._autoParam →
                          autoParam
                              (∀ {c c' : C} (c'' : C) (f : c ⟶ c') (d : D),
                                CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c'') d =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c''
                                        d).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c'' d))
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c' c''
                                          d).inv))
                              CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft._autoParam →
                            autoParam
                                (∀ (c₁ c₂ c₃ : C) (d : D),
                                  CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom d)
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁
                                            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃) d).hom
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c₁
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₃
                                              d).hom)) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
                                          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃ d).hom
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₂
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₃
                                            d)).hom)
                                CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom._autoParam →
                              autoParam
                                  (∀ (c : C) (d : D),
                                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom d =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
                                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c d).hom
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c
                                              d)).hom)
                                  CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom._autoParam →
                                autoParam
                                    (∀ (c : C) (d : D),
                                      CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom d =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c
                                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d).hom
                                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                                d).hom))
                                    CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom._autoParam →
                                  CategoryTheory.MonoidalCategory.MonoidalLeftAction C D