-- 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
h :
  ∀ (x_1 : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V),
    Eq (α := Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategory) (leftRegular G) X).V)
            (((tensorObj (𝒞 := instCategory) (leftRegular G) X).ρ : (a : G) → End (leftRegular G ⊗ X).V) x)
            (Iso.hom
              (Equiv.toIso
                {
                  toFun := fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
                    (g.1,
                      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                          (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                        g.2),
                  invFun := fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
                    (g.1,
                      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                          (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                        g.2),
                  left_inv := ⋯, right_inv := ⋯ :
                  (tensorObj (𝒞 := instCategory) (leftRegular G) X).V ≃
                    Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)) }))))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)))
            (Iso.hom
              (Equiv.toIso
                {
                  toFun := fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
                    (g.1,
                      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                          (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                        g.2),
                  invFun := fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
                    (g.1,
                      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                          (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                        g.2),
                  left_inv := ⋯, right_inv := ⋯ :
                  (tensorObj (𝒞 := instCategory) (leftRegular G) X).V ≃
                    Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)) }))
            ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)) :
                (a : G) → End (leftRegular G ⊗ trivial G X.V).V)
              x)))
        x_1)
⊢ Eq.{u + 1} (α :=
    (tensorObj (𝒞 := instCategory) (leftRegular G) X).V ⟶
      Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)))
    (CategoryStruct.comp (Y := (tensorObj (𝒞 := instCategory) (leftRegular G) X).V)
      (((tensorObj (𝒞 := instCategory) (leftRegular G) X).ρ : (a : G) → End (leftRegular G ⊗ X).V) x)
      (Iso.hom
        (Equiv.toIso
          {
            toFun := fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
              (g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2),
            invFun := fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
              (g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2),
            left_inv := ⋯, right_inv := ⋯ })))
    (CategoryStruct.comp (Y := Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)))
      (Iso.hom
        (Equiv.toIso
          {
            toFun := fun (g : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V) ↦
              (g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2),
            invFun := fun (g : Action.V (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V))) ↦
              (g.1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                    (a : (fun (X : Type u) ↦ X) X.V) → (fun (X : Type u) ↦ X) X.V)
                  g.2),
            left_inv := ⋯, right_inv := ⋯ }))
      ((ρ (tensorObj (𝒞 := instCategory) (leftRegular G) (trivial G X.V)) :
          (a : G) → End (leftRegular G ⊗ trivial G X.V).V)
        x))

Tactic:
ext _