awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
x x_1 x_2 : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) x_1))
          (obj (F.mapAction G) x_2)).V ⟶
      (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x (tensorObj (𝒞 := instCategory) x_1 x_2))).V)
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))
          (obj (F.mapAction G) x_2))
        ({ hom := μ F x.V x_1.V, comm := ⋯ } ▷ obj (F.mapAction G) x_2)
        ({ hom := μ F (tensorObj (𝒞 := instCategory) x x_1).V x_2.V, comm := ⋯ } ≫
          map (F.mapAction G) (Iso.hom (α_ x x_1 x_2)))))
    (Hom.hom
      (Iso.hom (α_ (obj (F.mapAction G) x) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
            (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x_1 x_2)))
          (obj (F.mapAction G) x ◁ { hom := μ F x_1.V x_2.V, comm := ⋯ })
          { hom := μ F x.V (tensorObj (𝒞 := instCategory) x_1 x_2).V, comm := ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
x : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x)).V ⟶
      (obj (F.mapAction G) x).V)
    (Hom.hom (Iso.hom (λ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
          (obj (F.mapAction G) x))
        ({ hom := ε F, comm := ⋯ } ▷ obj (F.mapAction G) x)
        (CategoryStruct.comp (Y :=
          obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
          { hom := μ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
            comm := ⋯ }
          (map (F.mapAction G) (Iso.hom (λ_ x))))))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x) ⟶
      obj (F.mapAction G) x)
    (Iso.hom (λ_ (obj (F.mapAction G) x)))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
        (obj (F.mapAction G) x))
      ({ hom := ε F, comm := ⋯ } ▷ obj (F.mapAction G) x)
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
        { hom := μ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
          comm := ⋯ }
        (map (F.mapAction G) (Iso.hom (λ_ x)))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
x : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x)).V ⟶
      (obj (F.mapAction G) x).V)
    (Hom.hom (Iso.hom (λ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
          (obj (F.mapAction G) x))
        ({ hom := ε F, comm := ⋯ } ▷ obj (F.mapAction G) x)
        (CategoryStruct.comp (Y :=
          obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
          { hom := μ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
            comm := ⋯ }
          (map (F.mapAction G) (Iso.hom (λ_ x))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
x : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))).V ⟶
      (obj (F.mapAction G) x).V)
    (Hom.hom (Iso.hom (ρ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (obj (F.mapAction G) x ◁ { hom := ε F, comm := ⋯ })
        (CategoryStruct.comp (Y :=
          obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
          { hom := μ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
            comm := ⋯ }
          (map (F.mapAction G) (Iso.hom (ρ_ x))))))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) ⟶
      obj (F.mapAction G) x)
    (Iso.hom (ρ_ (obj (F.mapAction G) x)))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
        (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
      (obj (F.mapAction G) x ◁ { hom := ε F, comm := ⋯ })
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        { hom := μ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
          comm := ⋯ }
        (map (F.mapAction G) (Iso.hom (ρ_ x)))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
x : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))).V ⟶
      (obj (F.mapAction G) x).V)
    (Hom.hom (Iso.hom (ρ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (obj (F.mapAction G) x ◁ { hom := ε F, comm := ⋯ })
        (CategoryStruct.comp (Y :=
          obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
          { hom := μ F x.V (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))),
            comm := ⋯ }
          (map (F.mapAction G) (Iso.hom (ρ_ x))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
⊢ Eq (α :=
    Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) ⟶
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
    (Hom.hom (ε (F.mapAction G))) (ε F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.LaxMonoidal
X Y : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) Y)).V ⟶
      (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) X Y)).V)
    (Hom.hom (μ (F.mapAction G) X Y)) (μ F X.V Y.V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
g : G
dsimp : F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
⊢ Eq.{v_2 + 1} (α :=
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
      Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (CategoryStruct.comp (Y := Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (((ρ (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) :
              MonoidHom.{u_2, v_2} G
                (End (Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))) :
            (a : G) → End ((F.mapAction G).obj (𝟙_ (Action V G))).V)
          g)
        (η F) :
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
        Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (CategoryStruct.comp (Y :=
        Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))) (η F)
        ((ρ ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) : (a : G) → End (𝟙_ (Action W G)).V) g) :
      Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
        Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))

Tactic:
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]

Premises used: CategoryTheory.Functor.mapAction, Action.FunctorCategoryEquivalence.inverse
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
g : G
rw : 𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
rw₁ :
  Eq (α := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)) ⟶ tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F)
    (η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)))
rw₂ rw₃ : Eq (α := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)) ⟶ tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (η F)
⊢ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))

Tactic:
rw [map_id, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
x_1 : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) X x_1)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) Y) (obj (F.mapAction G) x_1)).V)
    (Hom.hom ({ hom := δ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) x ▷ obj (F.mapAction G) x_1))
    (Hom.hom (map (F.mapAction G) (x ▷ x_1) ≫ { hom := δ F Y.V x_1.V, comm := ⋯ }))
⊢ Eq (α :=
    obj (F.mapAction G) (tensorObj (𝒞 := instCategory) X x_1) ⟶
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) Y) (obj (F.mapAction G) x_1))
    ({ hom := δ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) x ▷ obj (F.mapAction G) x_1)
    (map (F.mapAction G) (x ▷ x_1) ≫ { hom := δ F Y.V x_1.V, comm := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
x_1 : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) X x_1)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) Y) (obj (F.mapAction G) x_1)).V)
    (Hom.hom ({ hom := δ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) x ▷ obj (F.mapAction G) x_1))
    (Hom.hom (map (F.mapAction G) (x ▷ x_1) ≫ { hom := δ F Y.V x_1.V, comm := ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
X Y x : Action.{v_1, u_1, u_2} V G
x_1 : X ⟶ Y
h :
  Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x X)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) Y)).V)
    (Hom.hom ({ hom := δ F x.V X.V, comm := ⋯ } ≫ obj (F.mapAction G) x ◁ map (F.mapAction G) x_1))
    (Hom.hom (map (F.mapAction G) (x ◁ x_1) ≫ { hom := δ F x.V Y.V, comm := ⋯ }))
⊢ Eq (α :=
    obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x X) ⟶
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) Y))
    ({ hom := δ F x.V X.V, comm := ⋯ } ≫ obj (F.mapAction G) x ◁ map (F.mapAction G) x_1)
    (map (F.mapAction G) (x ◁ x_1) ≫ { hom := δ F x.V Y.V, comm := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
X Y x : Action.{v_1, u_1, u_2} V G
x_1 : X ⟶ Y
⊢ Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x X)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) Y)).V)
    (Hom.hom ({ hom := δ F x.V X.V, comm := ⋯ } ≫ obj (F.mapAction G) x ◁ map (F.mapAction G) x_1))
    (Hom.hom (map (F.mapAction G) (x ◁ x_1) ≫ { hom := δ F x.V Y.V, comm := ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x x_1 x_2 : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x x_1) x_2)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2))).V)
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))
          (obj (F.mapAction G) x_2))
        { hom := δ F (tensorObj (𝒞 := instCategory) x x_1).V x_2.V, comm := ⋯ }
        ({ hom := δ F x.V x_1.V, comm := ⋯ } ▷ obj (F.mapAction G) x_2 ≫
          Iso.hom (α_ (obj (F.mapAction G) x) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2)))))
    (Hom.hom
      (map (F.mapAction G) (Iso.hom (α_ x x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
            (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x_1 x_2)))
          { hom := δ F x.V (tensorObj (𝒞 := instCategory) x_1 x_2).V, comm := ⋯ }
          (obj (F.mapAction G) x ◁ { hom := δ F x_1.V x_2.V, comm := ⋯ })))
⊢ Eq (α :=
    obj (F.mapAction G) (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x x_1) x_2) ⟶
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
        (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2)))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))
        (obj (F.mapAction G) x_2))
      { hom := δ F (tensorObj (𝒞 := instCategory) x x_1).V x_2.V, comm := ⋯ }
      ({ hom := δ F x.V x_1.V, comm := ⋯ } ▷ obj (F.mapAction G) x_2 ≫
        Iso.hom (α_ (obj (F.mapAction G) x) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2))))
    (map (F.mapAction G) (Iso.hom (α_ x x_1 x_2)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x_1 x_2)))
        { hom := δ F x.V (tensorObj (𝒞 := instCategory) x_1 x_2).V, comm := ⋯ }
        (obj (F.mapAction G) x ◁ { hom := δ F x_1.V x_2.V, comm := ⋯ }))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x x_1 x_2 : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x x_1) x_2)).V ⟶
      (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
          (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2))).V)
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x x_1))
          (obj (F.mapAction G) x_2))
        { hom := δ F (tensorObj (𝒞 := instCategory) x x_1).V x_2.V, comm := ⋯ }
        ({ hom := δ F x.V x_1.V, comm := ⋯ } ▷ obj (F.mapAction G) x_2 ≫
          Iso.hom (α_ (obj (F.mapAction G) x) (obj (F.mapAction G) x_1) (obj (F.mapAction G) x_2)))))
    (Hom.hom
      (map (F.mapAction G) (Iso.hom (α_ x x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x)
            (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x_1 x_2)))
          { hom := δ F x.V (tensorObj (𝒞 := instCategory) x_1 x_2).V, comm := ⋯ }
          (obj (F.mapAction G) x ◁ { hom := δ F x_1.V x_2.V, comm := ⋯ })))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x : Action.{v_1, u_1, u_2} V G
h :
  Eq (α :=
    (obj (F.mapAction G) x).V ⟶
      (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x)).V)
    (Hom.hom (Iso.inv (λ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
        (map (F.mapAction G) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
            (obj (F.mapAction G) x))
          { hom := δ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
            comm := ⋯ }
          ({ hom := η F, comm := ⋯ } ▷ obj (F.mapAction G) x))))
⊢ Eq (α :=
    obj (F.mapAction G) x ⟶
      tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x))
    (Iso.inv (λ_ (obj (F.mapAction G) x)))
    (CategoryStruct.comp (Y :=
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
      (map (F.mapAction G) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
          (obj (F.mapAction G) x))
        { hom := δ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
          comm := ⋯ }
        ({ hom := η F, comm := ⋯ } ▷ obj (F.mapAction G) x)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
W : Type u_3
inst_2 : Category.{v_2, u_3} W
inst_3 : MonoidalCategory.{v_1, u_1} V
inst_4 : MonoidalCategory.{v_2, u_3} W
F : Functor.{v_1, v_2, u_1, u_3} V W
inst_5 : F.OplaxMonoidal
x : Action.{v_1, u_1, u_2} V G
⊢ Eq (α :=
    (obj (F.mapAction G) x).V ⟶
      (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (obj (F.mapAction G) x)).V)
    (Hom.hom (Iso.inv (λ_ (obj (F.mapAction G) x))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        obj (F.mapAction G) (tensorObj (𝒞 := instCategory) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)) x))
        (map (F.mapAction G) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
            (obj (F.mapAction G) x))
          { hom := δ F (Action.V.{v_1, u_1, u_2} (G := G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) x.V,
            comm := ⋯ }
          ({ hom := η F, comm := ⋯ } ▷ obj (F.mapAction G) x))))

Tactic:
simp