-- 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
⊢ 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))
have 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 := sorry, right_inv := sorry :
                (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 := sorry, right_inv := sorry :
                (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)
Tactic: ext _