awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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} (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)
have h : x =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
        (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
      ((x, y), z)).1
Tactic: with_reducible convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
-- 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
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
⊢ 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)
have h₁ : y =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).2.1
Tactic: with_reducible convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
-- 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
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
h₁ :
  y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1
⊢ 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)
have h₂ : z =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).2.2
Tactic: with_reducible convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k k (Finsupp.{w, u} X.V k)) (tprod (trivial k G k) (linearize k G X))
      (linearize k G X))
    (↑(lid k (linearize k G X)) : ((trivial k G k).tprod (linearize k G X)).IntertwiningMap (linearize k G X))
    (comp (comp (linearizeMap (Iso.hom (λ_ X))) (μ ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) X))
      (rTensor (linearize k G X) (ε k G)))
have h : ∀ (x1 : X.V),
  Eq (α := Finsupp.{w, u} X.V k)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap (ρ := tprod (trivial k G k) (linearize k G X))
                    (↑(lid k (linearize k G X)) :
                      ((trivial k G k).tprod (linearize k G X)).IntertwiningMap (linearize k G X))) :
                k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle x1 :
        (a : k) → X.V →₀ k)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap
                    (comp
                      (comp (linearizeMap (Iso.hom (λ_ X))) (μ ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) X))
                      (rTensor (linearize k G X) (ε k G)))) :
                k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle x1 :
        (a : k) → X.V →₀ k)
      1)
Tactic: ext x1 : 5
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} X.V k) k) (tprod (linearize k G X) (trivial k G k))
      (linearize k G X))
    (↑(rid k (linearize k G X)) : ((linearize k G X).tprod (trivial k G k)).IntertwiningMap (linearize k G X))
    (comp (comp (linearizeMap (Iso.hom (ρ_ X))) (μ X ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))))
      (lTensor (linearize k G X) (ε k G)))
have h : ∀ (x a : X.V),
  Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                        (toLinearMap (ρ := tprod (linearize k G X) (trivial k G k))
                          (↑(rid k (linearize k G X)) :
                            ((linearize k G X).tprod (trivial k G k)).IntertwiningMap (linearize k G X))) ∘ₗ
                      Finsupp.lsingle x :
                    k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                  (a : k) → k →ₗ[k] X.V →₀ k)
                1 :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry
                        (toLinearMap
                          (comp
                            (comp (linearizeMap (Iso.hom (ρ_ X)))
                              (μ X ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))))
                            (lTensor (linearize k G X) (ε k G)))) ∘ₗ
                      Finsupp.lsingle x :
                    k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                  (a : k) → k →ₗ[k] X.V →₀ k)
                1 :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a :
      k)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ Eq (α :=
    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k →ₗ[k]
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
        (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
          (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
        g)
    ((tprod (linearize k G X) (linearize k G Y) :
          (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
        g ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
        (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)))
have h : ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
  Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
            (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
              g) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
    ((((tprod (linearize k G X) (linearize k G Y) :
                (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
              g ∘ₗ
            (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
            (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
              g) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
    ((((tprod (linearize k G X) (linearize k G Y) :
                (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
              g ∘ₗ
            (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
have h : Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
  (Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V)) g) :
              (a : X.V × Y.V) → X.V × Y.V)
            a).1
        1 ⊗ₜ[k]
      Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V)) g) :
              (a : X.V × Y.V) → X.V × Y.V)
            a).2
        1 :
    TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
  (Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : X.V) → X.V) a.1)
        1 ⊗ₜ[k]
      Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V) a.2) 1 :
    TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
Tactic: simp [types_tensorObj_def, linearize_single _,
      finsuppTensorFinsupp'_symm_single_eq_single_one_tmul k]
-- 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
f : X ⟶ Y
⊢ Eq (α :=
    IntertwiningMap (V := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z).V k)
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z))
      (tprod (linearize k G Y) (linearize k G Z)))
    (comp (rTensor (linearize k G Z) (linearizeMap f)) (δ X Z)) (comp (δ Y Z) (linearizeMap (f ▷ Z)))
have h : ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z).V),
  Eq (α := TensorProduct k (Finsupp.{w, u} Y.V k) (Finsupp.{w, u} Z.V k))
    ((toLinearMap (comp (rTensor (linearize k G Z) (linearizeMap f)) (δ X Z)) ∘ₗ Finsupp.lsingle a :
        (a : k) → TensorProduct k (Y.V →₀ k) (Z.V →₀ k))
      1)
    ((toLinearMap (comp (δ Y Z) (linearizeMap (f ▷ Z))) ∘ₗ Finsupp.lsingle a :
        (a : k) → TensorProduct k (Y.V →₀ k) (Z.V →₀ k))
      1)
Tactic: ext
-- 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
f : X ⟶ Y
⊢ Eq (α :=
    IntertwiningMap (V := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z X).V k)
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z X))
      (tprod (linearize k G Z) (linearize k G Y)))
    (comp (lTensor (linearize k G Z) (linearizeMap f)) (δ Z X)) (comp (δ Z Y) (linearizeMap (Z ◁ f)))
have h : ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z X).V),
  Eq (α := TensorProduct k (Finsupp.{w, u} Z.V k) (Finsupp.{w, u} Y.V k))
    ((toLinearMap (comp (lTensor (linearize k G Z) (linearizeMap f)) (δ Z X)) ∘ₗ Finsupp.lsingle a :
        (a : k) → TensorProduct k (Z.V →₀ k) (Y.V →₀ k))
      1)
    ((toLinearMap (comp (δ Z Y) (linearizeMap (Z ◁ f))) ∘ₗ Finsupp.lsingle a :
        (a : k) → TensorProduct k (Z.V →₀ k) (Y.V →₀ k))
      1)
Tactic: ext
-- 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
⊢ Eq (α :=
    IntertwiningMap (V :=
      Finsupp.{w, u}
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z).V
        k)
      (linearize k G
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory)
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z))
      (tprod (linearize k G X) (tprod (linearize k G Y) (linearize k G Z))))
    (comp
      (comp
        (↑(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))))
        (rTensor (linearize k G Z) (δ X Y)))
      (δ (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z))
    (comp
      (comp (lTensor (linearize k G X) (δ Y Z)) (δ X (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)))
      (linearizeMap (Iso.hom (α_ X Y Z))))
have h : ∀
  (a :
    (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z).V),
  Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (TensorProduct k (Finsupp.{w, u} Y.V k) (Finsupp.{w, u} Z.V k)))
    ((toLinearMap
            (comp
              (comp
                (↑(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))))
                (rTensor (linearize k G Z) (δ X Y)))
              (δ (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) Z)) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (TensorProduct k (Y.V →₀ k) (Z.V →₀ k)))
      1)
    ((toLinearMap
            (comp
              (comp (lTensor (linearize k G X) (δ Y Z))
                (δ X (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)))
              (linearizeMap (Iso.hom (α_ X Y Z)))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (TensorProduct k (Y.V →₀ k) (Z.V →₀ k)))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
⊢ Eq (α :=
    IntertwiningMap (V := X.V →₀ k) (W := TensorProduct k k (X.V →₀ k)) (linearize k G X)
      (tprod (trivial k G k) (linearize k G X)))
    (↑(Equiv.symm (lid k (linearize k G X))) :
      (linearize k G X).IntertwiningMap ((trivial k G k).tprod (linearize k G X)))
    (comp (comp (rTensor (linearize k G X) (η k G)) (δ ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) X))
      (linearizeMap (Iso.inv (λ_ X))))
have h : ∀ (a : X.V),
  Eq (α := TensorProduct k k (X.V →₀ k))
    ((toLinearMap (ρ := linearize k G X)
            (↑(Equiv.symm (lid k (linearize k G X))) :
              (linearize k G X).IntertwiningMap ((trivial k G k).tprod (linearize k G X))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k k (X.V →₀ k))
      1)
    ((toLinearMap
            (comp (comp (rTensor (linearize k G X) (η k G)) (δ ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) X))
              (linearizeMap (Iso.inv (λ_ X)))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k k (X.V →₀ k))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
⊢ Eq (α :=
    IntertwiningMap (V := X.V →₀ k) (W := TensorProduct k (X.V →₀ k) k) (linearize k G X)
      (tprod (linearize k G X) (trivial k G k)))
    (↑(Equiv.symm (rid k (linearize k G X))) :
      (linearize k G X).IntertwiningMap ((linearize k G X).tprod (trivial k G k)))
    (comp (comp (lTensor (linearize k G X) (η k G)) (δ X ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
      (linearizeMap (Iso.inv (ρ_ X))))
have h : ∀ (a : X.V),
  Eq (α := TensorProduct k (X.V →₀ k) k)
    ((toLinearMap (ρ := linearize k G X)
            (↑(Equiv.symm (rid k (linearize k G X))) :
              (linearize k G X).IntertwiningMap ((linearize k G X).tprod (trivial k G k))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) k)
      1)
    ((toLinearMap
            (comp (comp (lTensor (linearize k G X) (η k G)) (δ X ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
              (linearizeMap (Iso.inv (ρ_ X)))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) k)
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
⊢ Eq (α :=
    IntertwiningMap (V := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y))
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y)))
    (comp (μ X Y) (δ X Y))
    (IntertwiningMap.id (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y)))
have h : ∀ (a a_1 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
  Eq.{u + 1} (α := k)
    (((toLinearMap (comp (μ X Y) (δ X Y)) ∘ₗ Finsupp.lsingle a : (a : k) → (X ⊗ Y).V →₀ k) 1 : (a : (X ⊗ Y).V) → k)
        a_1 :
      k)
    (((toLinearMap (ρ := linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y))
                  (IntertwiningMap.id
                    (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y))) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_1 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
      (tprod (linearize k G X) (linearize k G Y)) (tprod (linearize k G X) (linearize k G Y)))
    (comp (δ X Y) (μ X Y)) (IntertwiningMap.id (tprod (linearize k G X) (linearize k G Y)))
have h : ∀ (a : X.V) (a_1 : Y.V),
  Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (δ X Y) (μ X Y))) ∘ₗ Finsupp.lsingle a :
                k →ₗ[k] Finsupp.{w, u} Y.V k →ₗ[k] TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k)) :
              (a : k) → (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (toLinearMap (ρ := tprod (linearize k G X) (linearize k G Y))
                      (IntertwiningMap.id (tprod (linearize k G X) (linearize k G Y)))) ∘ₗ
                  Finsupp.lsingle a :
                k →ₗ[k] Finsupp.{w, u} Y.V k →ₗ[k] TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k)) :
              (a : k) → (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
⊢ Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k →ₗ[k] Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
    ((linearize k G (Action.trivial G X) : (a : G) → ((Action.trivial G X).V →₀ k) →ₗ[k] (Action.trivial G X).V →₀ k)
        g :
      Finsupp.{w, u} (Action.V (Action.trivial G X)) k →ₗ[k] Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
    (LinearMap.id :
      Finsupp.{w, u} (Action.V (Action.trivial G X)) k →ₗ[k] Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
have h : ∀ (x : X),
  Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
    (((linearize k G (Action.trivial G X) : (a : G) → ((Action.trivial G X).V →₀ k) →ₗ[k] (Action.trivial G X).V →₀ k)
            g ∘ₗ
          Finsupp.lsingle x :
        (a : k) → (Action.trivial G X).V →₀ k)
      1)
    ((LinearMap.id ∘ₗ Finsupp.lsingle x : (a : k) → (Action.trivial G X).V →₀ k) 1)
Tactic: ext (x : X) : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
x : X
⊢ Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
    (((linearize k G (Action.trivial G X) : (a : G) → ((Action.trivial G X).V →₀ k) →ₗ[k] (Action.trivial G X).V →₀ k)
            g ∘ₗ
          Finsupp.lsingle x :
        (a : k) → (Action.trivial G X).V →₀ k)
      1)
    ((LinearMap.id ∘ₗ Finsupp.lsingle x : (a : k) → (Action.trivial G X).V →₀ k) 1)
have h : Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
  (Finsupp.single
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (((Action.ρ (Action.trivial G X) : MonoidHom.{v, w} G (End (Action.V (Action.trivial G X)))) :
                (a : G) → End (Action.trivial G X).V)
              g) :
          (a : (fun (X : Type w) ↦ X) (Action.trivial G X).V) → (fun (X : Type w) ↦ X) (Action.trivial G X).V)
        x)
      1 :
    Finsupp.{w, u} ((fun (X : Type w) ↦ X) (Action.V (Action.trivial G X))) k)
  (Finsupp.single x 1 : Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
Tactic: rw [LinearMap.comp_apply, LinearMap.id_comp, Finsupp.lsingle_apply, linearize_single]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
x : X
⊢ Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
    (Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (((Action.ρ (Action.trivial G X) : MonoidHom.{v, w} G (End (Action.V (Action.trivial G X)))) :
                  (a : G) → End (Action.trivial G X).V)
                g) :
            (a : (fun (X : Type w) ↦ X) (Action.trivial G X).V) → (fun (X : Type w) ↦ X) (Action.trivial G X).V)
          x)
        1 :
      Finsupp.{w, u} ((fun (X : Type w) ↦ X) (Action.V (Action.trivial G X))) k)
    (Finsupp.single x 1 : Finsupp.{w, u} (Action.V (Action.trivial G X)) k)
have h : Eq (α := X →₀ k)
  (Finsupp.single
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (((1 : MonoidHom.{v, w} G (End X)) : (a : G) → End X) g) :
          (a : X) → X)
        x)
      1 :
    X →₀ k)
  (Finsupp.single x 1 : X →₀ k)
Tactic: simp only [Action.trivial_V, Action.trivial_ρ]