awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
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:
simp [linearizeMap_single _, δ_apply_single _]

Premises used: Representation.LinearizeMonoidal.δ_apply_single, Representation.linearizeMap_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
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)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
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:
simp [linearizeMap_single _, δ_apply_single _]

Premises used: Representation.LinearizeMonoidal.δ_apply_single, Representation.linearizeMap_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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)
⊢ 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))))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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:
simp [linearizeMap, δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul k]

Premises used: Representation.LinearizeMonoidal.δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Representation.linearizeMap
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
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)
⊢ 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))))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
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:
simp [linearizeMap, δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: Representation.LinearizeMonoidal.δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Representation.linearizeMap
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
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)
⊢ 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))))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
X : Action (Type u) G
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:
simp [linearizeMap_single _, δ_apply_single _]

Premises used: Representation.LinearizeMonoidal.δ_apply_single, Representation.linearizeMap_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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:
simp [δ_apply_single _]

Premises used: Representation.LinearizeMonoidal.δ_apply_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
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:
simp [δ_apply_single _]

Premises used: Representation.LinearizeMonoidal.δ_apply_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
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)
⊢ 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)

Tactic:
ext (x : X) : 2
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
x : X
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)
⊢ 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:
rw [LinearMap.comp_apply, LinearMap.id_comp, Finsupp.lsingle_apply, linearize_single]

Premises used: Representation.linearize_single, LinearMap.comp_apply, LinearMap.id_comp, Finsupp.lsingle_apply
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
x : X
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)
⊢ 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:
simp only [Action.trivial_V, Action.trivial_ρ]

Premises used: Action.trivial_ρ, Action.trivial_V
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
g : G
x : X
⊢ 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:
rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X_1 Y Z : Action (Type w) G
X : Type w
g : G
⊢ Eq (α := Finsupp.{w, u} (Action.V (Action.trivial G X)) k →ₗ[k] X →₀ k)
    ((↑(LinearEquiv.refl k (Finsupp.{w, u} (Action.V (Action.trivial G X)) k)) :
        ((Action.trivial G X).V →₀ k) →ₗ[k] 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)
    ((trivial k G (X →₀ k) : (a : G) → (X →₀ k) →ₗ[k] X →₀ k) g ∘ₗ
      (↑(LinearEquiv.refl k (Finsupp.{w, u} (Action.V (Action.trivial G X)) k)) :
        ((Action.trivial G X).V →₀ k) →ₗ[k] X →₀ k))

Tactic:
simpa using linearizeTrivial_def (k := k) X g

Premises used: Representation.linearizeTrivial_def
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
f : Finsupp.{w, u} (Action.V (Action.trivial G X)) k
⊢ (linearizeTrivialIso k G X : (a : (Action.trivial G X).V →₀ k) → X →₀ k) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Type w
f : X →₀ k
⊢ (Equiv.symm (linearizeTrivialIso k G X) : (a : X →₀ k) → (Action.trivial G X).V →₀ k) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
H : Type w
inst_6 : MulAction G H
g : G
⊢ Eq (α := Finsupp.{w, u} (Action.V (Action.ofMulAction G H)) k →ₗ[k] H →₀ k)
    ((↑(LinearEquiv.refl k (Finsupp.{w, u} (Action.V (Action.ofMulAction G H)) k)) :
        ((Action.ofMulAction G H).V →₀ k) →ₗ[k] H →₀ k) ∘ₗ
      (linearize k G (Action.ofMulAction G H) :
          (a : G) → ((Action.ofMulAction G H).V →₀ k) →ₗ[k] (Action.ofMulAction G H).V →₀ k)
        g)
    ((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g ∘ₗ
      (↑(LinearEquiv.refl k (Finsupp.{w, u} (Action.V (Action.ofMulAction G H)) k)) :
        ((Action.ofMulAction G H).V →₀ k) →ₗ[k] H →₀ k))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
H : Type w
inst_2 : MulAction G H
f : H →₀ k
⊢ (linearizeOfMulActionIso k G H : (a : H →₀ k) → (Action.ofMulAction G H).V →₀ k) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
H : Type w
inst_2 : MulAction G H
f : H →₀ k
⊢ (Equiv.symm (linearizeOfMulActionIso k G H) : (a : H →₀ k) → (Action.ofMulAction G H).V →₀ k) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
⊢ Module.Finite.{u_3, u_2} k (Module.End A V)

Tactic:
have : Module.Finite k (Module.End A V) := .of_injective (LinearMap.restrictScalarsₗ k A V V k) <|
    LinearMap.restrictScalars_injective _
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
this : Module.Finite.{u_3, u_2} k (Module.End A V)
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := k) (β := Module.End A V)
    (⇑(algebraMap k (Module.End A V)) : (a : k) → Module.End A V)

Tactic:
IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

Premises used: IsAlgClosed.algebraMap_bijective_of_isIntegral