awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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 x : Action.{v_1, u_1, u_2} V G
x_1 : X ⟶ Y
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) X) ⟶
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x Y))
    (obj (F.mapAction G) x ◁ map (F.mapAction G) x_1 ≫ { hom := μ F x.V Y.V, comm := ⋯ })
    ({ hom := μ F x.V X.V, comm := ⋯ } ≫ map (F.mapAction G) (x ◁ x_1))
have h : Eq (α :=
  (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) (obj (F.mapAction G) X)).V ⟶
    (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x Y)).V)
  (Hom.hom (obj (F.mapAction G) x ◁ map (F.mapAction G) x_1 ≫ { hom := μ F x.V Y.V, comm := sorry }))
  (Hom.hom ({ hom := μ F x.V X.V, comm := sorry } ≫ map (F.mapAction G) (x ◁ x_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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) ⟶
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x (tensorObj (𝒞 := instCategory) x_1 x_2)))
    (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))))
    (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 := ⋯ })
have h : 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 := sorry } ▷ obj (F.mapAction G) x_2)
      ({ hom := μ F (tensorObj (𝒞 := instCategory) x x_1).V x_2.V, comm := sorry } ≫
        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 := sorry })
        { hom := μ F x.V (tensorObj (𝒞 := instCategory) x_1 x_2).V, comm := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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) ⟶
      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)))))
have 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 := sorry } ▷ 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 := sorry }
        (map (F.mapAction G) (Iso.hom (λ_ x))))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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)) ⟶
      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)))))
have 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 := sorry })
      (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 := sorry }
        (map (F.mapAction G) (Iso.hom (ρ_ x))))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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
⊢ 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)))
have dsimp : F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
Tactic: dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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
⊢ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
have rw : 𝟙 (F.obj (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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))
⊢ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
have 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)))
Tactic: rw [map_id, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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)))
⊢ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))) ≫ η F = η F ≫ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
have rw₂ : Eq (α := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst)) ⟶ tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) (η F) (η F)
Tactic: rw [map_id, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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) ⟶
      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 := ⋯ })
have 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 := sorry } ≫ 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 := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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) ⟶
      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 := ⋯ })
have 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 := sorry } ≫ 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 := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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) ⟶
      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 := ⋯ }))
have 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 := sorry }
      ({ hom := δ F x.V x_1.V, comm := sorry } ▷ 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 := sorry }
        (obj (F.mapAction G) x ◁ { hom := δ F x_1.V x_2.V, comm := sorry })))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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 ⟶
      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)))
have 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 := sorry }
        ({ hom := η F, comm := sorry } ▷ obj (F.mapAction G) x))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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 ⟶
      tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (Iso.inv (ρ_ (obj (F.mapAction G) x)))
    (CategoryStruct.comp (Y :=
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
      (map (F.mapAction G) (Iso.inv (ρ_ 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))))
        { 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 := ⋯ }
        (obj (F.mapAction G) x ◁ { hom := η F, comm := ⋯ })))
have h : Eq (α :=
  (obj (F.mapAction G) x).V ⟶
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) x) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))).V)
  (Hom.hom (Iso.inv (ρ_ (obj (F.mapAction G) x))))
  (Hom.hom
    (CategoryStruct.comp (Y :=
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
      (map (F.mapAction G) (Iso.inv (ρ_ 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))))
        { 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 := sorry }
        (obj (F.mapAction G) x ◁ { hom := η F, comm := sorry }))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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.Monoidal
⊢ Eq (α :=
    Quiver.Hom (V := Action.{v_2, u_3, u_2} W G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))
      ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
      (ε (F.mapAction G)) (η (F.mapAction G)))
    (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
have h : Eq (α :=
  Quiver.Hom.{v_2, u_3} (V := W)
    (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
    (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
  (Hom.hom
    (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
      (ε (F.mapAction G)) (η (F.mapAction G))))
  (Hom.hom (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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.Monoidal
⊢ Eq (α :=
    Quiver.Hom.{v_2, u_3} (V := W)
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
      (Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
    (Hom.hom
      (CategoryStruct.comp (Y := obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))
        (ε (F.mapAction G)) (η (F.mapAction G))))
    (Hom.hom (𝟙 ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory))))
have h : CategoryStruct.comp (Y := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (η F) =
  𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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.Monoidal
⊢ CategoryStruct.comp (Y := F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
have h : Eq.{v_2 + 1} (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ tensorUnit.{v_2, u_3} W (𝒞 := inst_2))
  (𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2))) (𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)))
Tactic: rw [ε_η]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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.Monoidal
⊢ Eq (α :=
    Quiver.Hom (V := Action.{v_2, u_3, u_2} W G)
      (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))))
    (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
      (ε (F.mapAction G)))
    (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
have h : Eq (α :=
  Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))) ⟶
    Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
  (Hom.hom
    (CategoryStruct.comp (Y := (𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) (η (F.mapAction G))
      (ε (F.mapAction G))))
  (Hom.hom (𝟙 (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory)))))
Tactic: ext