-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
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
⊢ 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)
have h : 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 := sorry, right_inv := sorry :
              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 := sorry, right_inv := sorry :
              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 only [tensorObj_V, tensor_ρ]