-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ Eq (α :=
    Finsupp.{w, u}
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V
      k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (toLinearMap
                              (comp
                                (comp (linearizeMap (Iso.hom (α_ X Y Z)))
                                  (μ (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z))
                                (rTensor (linearize k G Z) (μ X Y))))) ∘ₗ
                        Finsupp.lsingle x :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} Z.V k →ₗ[k]
                            Finsupp.{w, u}
                              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
                                  (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V
                              k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (Z.V →₀ k) →ₗ[k] (X ⊗ Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle y :
              (a : k) → (Z.V →₀ k) →ₗ[k] (X ⊗ Y ⊗ Z).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle z :
        (a : k) → (X ⊗ Y ⊗ Z).V →₀ k)
      1)
    (((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (toLinearMap
                              (comp
                                (comp (μ X (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z))
                                  (lTensor (linearize k G X) (μ Y Z)))
                                (↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z)) :
                                  (((linearize k G X).tprod (linearize k G Y)).tprod (linearize k G Z)).IntertwiningMap
                                    ((linearize k G X).tprod ((linearize k G Y).tprod (linearize k G Z))))))) ∘ₗ
                        Finsupp.lsingle x :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} Z.V k →ₗ[k]
                            Finsupp.{w, u}
                              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
                                  (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V
                              k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (Z.V →₀ k) →ₗ[k] (X ⊗ Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle y :
              (a : k) → (Z.V →₀ k) →ₗ[k] (X ⊗ Y ⊗ Z).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle z :
        (a : k) → (X ⊗ Y ⊗ Z).V →₀ k)
      1)
have h : Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
  ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
      (Finsupp.single ((x, y), z) 1) :
    Finsupp.{w, u} (X.V × Y.V × Z.V) k)
  (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)
Tactic: simp only [Action.tensorObj_V, types_tensorObj_def, comp_toLinearMap, μ_toLinearMap,
    toLinearMap_rTensor, LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
    TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self,
    TensorProduct.curry_apply, LinearEquiv.coe_coe, LinearMap.rTensor_tmul,
    finsuppTensorFinsupp'_single_tmul_single, mul_one, toLinearMap_lTensor, toLinearMap_assoc,
    TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, toLinearMap_apply]