awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := V (leftRegular G) × (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V × (Fin n → G))
          f :
        V (leftRegular G) × (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
⊢ ((Fin.consEquiv.{u} (n := n) fun (x : Fin (n + 1)) ↦ G : G × ((i : Fin n) → G) ≃ ((i : Fin (n + 1)) → G)) :
        (a : (leftRegular G).V × (Fin n → G)) → Fin (n + 1) → G)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G (Fin n → G))) :
                  (a : G) → End ((leftRegular G).V × (Fin n → G)))
                ((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).1⁻¹) :
            (a : (leftRegular G).V × (Fin n → G)) → (leftRegular G).V × (Fin n → G))
          (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                    (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                  f).2
              0,
            fun (i : Fin n) ↦
            HMul.hMul (α := G)
              (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).2
                  i.castSucc)⁻¹
              (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                      (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                    f).2
                i.succ)) :
        V (leftRegular G) × (Fin n → G))
      0 =
    (f 0)⁻¹ * f 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
i : Fin n
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := V (leftRegular G) × (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V × (Fin n → G))
          f :
        V (leftRegular G) × (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
⊢ ((Fin.consEquiv.{u} (n := n) fun (x : Fin (n + 1)) ↦ G : G × ((i : Fin n) → G) ≃ ((i : Fin (n + 1)) → G)) :
        (a : (leftRegular G).V × (Fin n → G)) → Fin (n + 1) → G)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G (Fin n → G))) :
                  (a : G) → End ((leftRegular G).V × (Fin n → G)))
                ((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).1⁻¹) :
            (a : (leftRegular G).V × (Fin n → G)) → (leftRegular G).V × (Fin n → G))
          (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                    (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                  f).2
              0,
            fun (i : Fin n) ↦
            HMul.hMul (α := G)
              (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                        (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                      f).2
                  i.castSucc)⁻¹
              (((Equiv.symm (Fin.consEquiv.{u} (n := n + 1) fun (a : Fin (n + 1 + 1)) ↦ G) :
                      (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V × (diagonal G (n + 1)).V)
                    f).2
                i.succ)) :
        V (leftRegular G) × (Fin n → G))
      i.succ =
    (f i.castSucc.succ)⁻¹ * f i.succ.succ

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
f : Fin (n + 1) → G
zero :
  ∀ (f : Fin (HAdd.hAdd (α := ℕ) 0 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G 0))) :
            (a : (diagonal G (0 + 1)).V) → (leftRegular G).V ⊗ (Fin 0 → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin 0 → G))
      ((f 0, fun (i : Fin 0) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin 0) → G))
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (f : Fin (n + 1) → G),
        Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
                (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
              f :
            tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
          ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G)))
    (f : Fin (n + 1 + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
      ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin (n + 1)) → G))
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
          (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
    ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))

Tactic:
induction n with
  | zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
  | succ n hn =>
    refine Prod.ext rfl (funext fun x => ?_)
    induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl

Premises used: Action.diagonalSuccIsoTensorTrivial, funext, CategoryTheory.types_tensorObj_def, Prod.ext, rfl, Fin.elim0
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
g : G
f : Fin 0 → G
zero :
  ∀ (x : Fin 1),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
          (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
        (g, f) x =
      (g • Fin.partialProd f) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
        (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
      (g, f) =
    g • Fin.partialProd f

Tactic:
funext (x : Fin 1)
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
g : G
f : Fin 0 → G
x : Fin 1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
        (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x

Tactic:
simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]

Premises used: Action.diagonalOneIsoLeftRegular, Action.diagonalSuccIsoTensorTrivial, CategoryTheory.types_tensorUnit_def, CategoryTheory.types_tensorObj_def, Subsingleton.elim, OfNat.ofNat, Action.ofMulAction_V
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
succ :
  ∀ (x : Fin (n + 1 + 1)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
        (g, f) x =
      (g • Fin.partialProd f) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) =
    g • Fin.partialProd f

Tactic:
funext x
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    g
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    (g • Fin.partialProd f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
i : Fin (n + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) i.succ =
    (g • Fin.partialProd f) i.succ

Tactic:
simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i

Premises used: Action.diagonalSuccIsoTensorTrivial, HMul.hMul, mul_assoc, CategoryTheory.types_tensorObj_def, congrFun, Fin.partialProd_succ', OfNat.ofNat, Fin.tail, Action.ofMulAction_V
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
          (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
        (g, f) =
      g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
x : Fin (n + 1 + 1)
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) 0 =
    (g • Fin.partialProd f) 0
succ₁ :
  ∀ (i : Fin (n + 1)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
        (g, f) i.succ =
      (g • Fin.partialProd f) i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
        (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
      (g, f) x =
    (g • Fin.partialProd f) x

Tactic:
induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i

Premises used: Action.diagonalSuccIsoTensorTrivial, mul_assoc, CategoryTheory.types_tensorObj_def, Fin.partialProd_succ', Action.ofMulAction_V
-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
G : Type u
inst : Group G
n : ℕ
g : G
f : Fin n → G
zero :
  ∀ (g : G) (f : Fin 0 → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G 0))) :
          (a : (leftRegular G).V ⊗ (Fin 0 → G)) → (diagonal G (0 + 1)).V)
        (g, f) =
      g • Fin.partialProd f
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (g : G) (f : Fin n → G),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
              (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
            (g, f) =
          g • Fin.partialProd f)
    (g : G) (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (leftRegular G).V ⊗ (Fin (n + 1) → G)) → (diagonal G (n + 1 + 1)).V)
        (g, f) =
      g • Fin.partialProd f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.inv (diagonalSuccIsoTensorTrivial G n))) :
        (a : (leftRegular G).V ⊗ (Fin n → G)) → (diagonal G (n + 1)).V)
      (g, f) =
    g • Fin.partialProd f

Tactic:
induction n generalizing g with
  | zero =>
    funext (x : Fin 1)
    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]
  | succ n hn =>
    funext x
    induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using congrFun (hn (g * f 0) (Fin.tail f)) i

Premises used: Action.diagonalOneIsoLeftRegular, Action.diagonalSuccIsoTensorTrivial, CategoryTheory.types_tensorUnit_def, mul_assoc, CategoryTheory.types_tensorObj_def, Fin.partialProd_succ', Action.ofMulAction_V
-- 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
g : G
dsimp : 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))
⊢ Eq.{v_2 + 1} (α :=
    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))))
    (CategoryStruct.comp (Y :=
        Action.V.{v_2, u_3, u_2} (G := G) ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)))
        ((ρ ((𝟙_ (Action.{v_2, u_3, u_2} W G)) (𝒞 := instCategory)) : (a : G) → End (𝟙_ (Action W G)).V) g) (ε F) :
      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))))
    (CategoryStruct.comp (Y := Action.V (obj (F.mapAction G) ((𝟙_ (Action.{v_1, u_1, u_2} V G)) (𝒞 := instCategory))))
        (ε F)
        (((ρ (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) :
      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))))

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.LaxMonoidal
g : G
rw :
  Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
    (ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
rw₁ :
  Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F)
    (ε F ≫ 𝟙 (F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))))
rw₂ rw₃ : Eq (α := tensorUnit.{v_2, u_3} W (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_1, u_1} V (𝒞 := inst))) (ε F) (ε F)
⊢ 𝟙 (tensorUnit.{v_2, u_3} W (𝒞 := inst_2)) ≫ ε F = ε F ≫ F.map (𝟙 (tensorUnit.{v_1, u_1} V (𝒞 := inst)))

Tactic:
rw [Category.id_comp, F.map_id, 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.LaxMonoidal
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 (α :=
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) x_1)).V ⟶
      (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) Y x_1)).V)
    (Hom.hom (map (F.mapAction G) x ▷ obj (F.mapAction G) x_1 ≫ { hom := μ F Y.V x_1.V, comm := ⋯ }))
    (Hom.hom ({ hom := μ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) (x ▷ x_1)))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) x_1) ⟶
      obj (F.mapAction G) (tensorObj (𝒞 := instCategory) Y x_1))
    (map (F.mapAction G) x ▷ obj (F.mapAction G) x_1 ≫ { hom := μ F Y.V x_1.V, comm := ⋯ })
    ({ hom := μ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) (x ▷ x_1))

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 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 (α :=
    (tensorObj (𝒞 := instCategory) (obj (F.mapAction G) X) (obj (F.mapAction G) x_1)).V ⟶
      (obj (F.mapAction G) (tensorObj (𝒞 := instCategory) Y x_1)).V)
    (Hom.hom (map (F.mapAction G) x ▷ obj (F.mapAction G) x_1 ≫ { hom := μ F Y.V x_1.V, comm := ⋯ }))
    (Hom.hom ({ hom := μ F X.V x_1.V, comm := ⋯ } ≫ map (F.mapAction G) (x ▷ x_1)))

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 Y x : Action.{v_1, u_1, u_2} V G
x_1 : X ⟶ Y
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 := ⋯ }))
    (Hom.hom ({ hom := μ F x.V X.V, comm := ⋯ } ≫ map (F.mapAction G) (x ◁ x_1)))
⊢ 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))

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 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)).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 := ⋯ }))
    (Hom.hom ({ hom := μ F x.V X.V, comm := ⋯ } ≫ map (F.mapAction G) (x ◁ x_1)))

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 x_1 x_2 : Action.{v_1, u_1, u_2} V G
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 := ⋯ } ▷ 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 := ⋯ }))
⊢ 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 := ⋯ })

Tactic:
ext