-- Module: Mathlib.CategoryTheory.Action.Monoidal
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
X : Action (Type u) G
x : G
x_1 : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V
h :
  Eq (α := X.V)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V) x_1.2 :
      X.V)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((1 : (a : G) → End X.V) x) : (a : X.V) → X.V)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V)
            x_1.2 :
          X.V) :
      X.V)
⊢ Eq (α := tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V)
          ((ρ (leftRegular G) : (a : G) → End (leftRegular G).V) x ⊗ₘ (X.ρ : (a : G) → End X.V) x)
          (Iso.hom
            (Equiv.toIso
              {
                toFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                        (a : X.V) → X.V)
                      g.2),
                invFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V))) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                        (a : X.V) → X.V)
                      g.2),
                left_inv := ⋯, right_inv := ⋯ :
                tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V ≃
                  tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)) }))))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)))
          (Iso.hom
            (Equiv.toIso
              {
                toFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                        (a : X.V) → X.V)
                      g.2),
                invFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V))) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                        (a : X.V) → X.V)
                      g.2),
                left_inv := ⋯, right_inv := ⋯ :
                tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V ≃
                  tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)) }))
          ((ρ (leftRegular G) : (a : G) → End (leftRegular G).V) x ⊗ₘ
            (ρ (trivial G X.V) : (a : G) → End (trivial G X.V).V) x)))
      x_1)

Tactic:
simp [types_tensorObj_def]

Premises used: CategoryTheory.types_tensorObj_def