awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
g : G
h :
  ∀ (a : α) (a_1 : G),
    Eq.{v' + 1} (α := V)
      ((((((linearCombination k fun (x : α × G) ↦
                      (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                    (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
                  (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g) ∘ₗ
                lsingle a) ∘ₗ
              lsingle a_1 :
            (a : k) → V)
          1 :
        V)
      (((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
                  (linearCombination k fun (x : α × G) ↦
                      (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                    (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
                lsingle a) ∘ₗ
              lsingle a_1 :
            (a : k) → V)
          1 :
        V)
⊢ Eq (α := (α →₀ G →₀ k) →ₗ[k] V)
    (((linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
        (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
      (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g)
    ((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
      (linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
        (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
g : G
a : α
a_1 : G
⊢ Eq.{v' + 1} (α := V)
    ((((((linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                  (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
                (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)
    (((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
                (linearCombination k fun (x : α × G) ↦
                    (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                  (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
k : Type u
inst_2 : CommSemiring k
inst_3 : Module k V
σ : Representation k G V
α : Type w'
i : α
g : G
r : k
f : α → V
⊢ (σ.freeLift f : (a : α →₀ G →₀ k) → V) (single i (single g r)) =
    HSMul.hSMul (β := V) r ((((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) (f i) : V)

Tactic:
simp [freeLift]

Premises used: Representation.freeLift
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : IntertwiningMap (free k G α) σ
h :
  ∀ (a : α) (a_1 : G),
    Eq.{v' + 1} (α := V)
      (((toLinearMap
                  (σ.freeLift
                    ((fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦
                        ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
                      f)) ∘ₗ
                lsingle a) ∘ₗ
              lsingle a_1 :
            (a : k) → V)
          1 :
        V)
      (((f.toLinearMap ∘ₗ lsingle a) ∘ₗ lsingle a_1 : (a : k) → V) 1 : V)
⊢ σ.freeLift
      ((fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦ ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : IntertwiningMap (free k G α) σ
a : α
a_1 : G
⊢ Eq.{v' + 1} (α := V)
    (((toLinearMap
                (σ.freeLift
                  ((fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦
                      ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
                    f)) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)
    (((f.toLinearMap ∘ₗ lsingle a) ∘ₗ lsingle a_1 : (a : k) → V) 1 : V)

Tactic:
simp [← f.isIntertwining]

Premises used: Representation.IntertwiningMap.isIntertwining
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
⊢ (fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦ ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
      (σ.freeLift f) =
    f

Tactic:
simp [← toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_12 : DecidableEq α
g : G
a : α
x : V
x_1 : W
a_1 : α
⊢ Eq (α := TensorProduct k V W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                            (((↑(TensorProduct.finsuppLeft k k V W α) :
                                  TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
                                TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                              (((σ.finsupp α).tprod ρ :
                                    (a : G) → TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W)
                                  g :
                                TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W)) ∘ₗ
                          lsingle a :
                        V →ₗ[k] W →ₗ[k] α →₀ TensorProduct k V W) :
                      (a : V) → W →ₗ[k] α →₀ TensorProduct k V W)
                    x :
                  W →ₗ[k] α →₀ TensorProduct k V W) :
                (a : W) → α →₀ TensorProduct k V W)
              x_1 :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        a_1 :
      TensorProduct k V W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                            ((((σ.tprod ρ).finsupp α :
                                    (a : G) → (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W)
                                  g :
                                (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                              ((↑(TensorProduct.finsuppLeft k k V W α) :
                                  TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
                                TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W)) ∘ₗ
                          lsingle a :
                        V →ₗ[k] W →ₗ[k] α →₀ TensorProduct k V W) :
                      (a : V) → W →ₗ[k] α →₀ TensorProduct k V W)
                    x :
                  W →ₗ[k] α →₀ TensorProduct k V W) :
                (a : W) → α →₀ TensorProduct k V W)
              x_1 :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        a_1 :
      TensorProduct k V W)

Tactic:
simp [TensorProduct.finsuppLeft_apply_tmul]

Premises used: TensorProduct.finsuppLeft_apply_tmul
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
f : α →₀ V
w : W
⊢ Eq (α := α →₀ TensorProduct k V W)
    ((σ.finsuppTensorLeft ρ α : (a : TensorProduct k (α →₀ V) W) → α →₀ TensorProduct k V W) (f ⊗ₜ[k] w) :
      α →₀ TensorProduct k V W)
    (f.sum fun (i : α) (v : V) ↦ single i (v ⊗ₜ[k] w) : α →₀ TensorProduct k V W)

Tactic:
simp [finsuppTensorLeft, TensorProduct.finsuppLeft_apply_tmul]

Premises used: Representation.finsuppTensorLeft, TensorProduct.finsuppLeft_apply_tmul
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
f : α →₀ V
w : W
i : α
⊢ Eq (α := TensorProduct k V W)
    ((((σ.finsuppTensorLeft ρ α : (a : TensorProduct k (α →₀ V) W) → α →₀ TensorProduct k V W) (f ⊗ₜ[k] w) :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        i :
      TensorProduct k V W)
    ((f : (a : α) → V) i ⊗ₜ[k] w : TensorProduct k V W)

Tactic:
simp +contextual [finsuppTensorLeft_apply_tmul, Finsupp.sum_apply, Finsupp.single_apply]

Premises used: Representation.finsuppTensorLeft_apply_tmul, Finsupp.single_apply, Finsupp.sum_apply
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
i : α
v : V
w : W
⊢ Eq (α := TensorProduct k (α →₀ V) W)
    (((σ.finsuppTensorLeft ρ α).symm : (a : α →₀ TensorProduct k V W) → TensorProduct k (α →₀ V) W)
        (single i (v ⊗ₜ[k] w)) :
      TensorProduct k (α →₀ V) W)
    (single i v ⊗ₜ[k] w : TensorProduct k (α →₀ V) W)

Tactic:
simp [finsuppTensorLeft]

Premises used: Representation.finsuppTensorLeft
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_12 : DecidableEq α
g : G
x : V
a : α
x_1 : W
a_1 : α
⊢ Eq (α := TensorProduct k V W)
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (((↑(TensorProduct.finsuppRight k k V W α) :
                                TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                              TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                            ((σ.tprod (ρ.finsupp α) :
                                  (a : G) → TensorProduct k V (α →₀ W) →ₗ[k] TensorProduct k V (α →₀ W))
                                g :
                              TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] TensorProduct.{u, v', w'} k V (α →₀ W))) :
                        V →ₗ[k] (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                      (a : V) → (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
                    x ∘ₗ
                  lsingle a :
                (a : W) → α →₀ TensorProduct k V W)
              x_1 :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        a_1 :
      TensorProduct k V W)
    ((((((TensorProduct.AlgebraTensorModule.curry
                          ((((σ.tprod ρ).finsupp α :
                                  (a : G) → (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W)
                                g :
                              (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                            ((↑(TensorProduct.finsuppRight k k V W α) :
                                TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                              TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)) :
                        V →ₗ[k] (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                      (a : V) → (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
                    x ∘ₗ
                  lsingle a :
                (a : W) → α →₀ TensorProduct k V W)
              x_1 :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        a_1 :
      TensorProduct k V W)

Tactic:
simp [TensorProduct.finsuppRight_apply_tmul]

Premises used: TensorProduct.finsuppRight_apply_tmul
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
v : V
f : α →₀ W
⊢ Eq (α := α →₀ TensorProduct k V W)
    ((σ.finsuppTensorRight ρ α : (a : TensorProduct k V (α →₀ W)) → α →₀ TensorProduct k V W) (v ⊗ₜ[k] f) :
      α →₀ TensorProduct k V W)
    (f.sum fun (i : α) (w : W) ↦ single i (v ⊗ₜ[k] w) : α →₀ TensorProduct k V W)

Tactic:
simp [finsuppTensorRight, TensorProduct.finsuppRight_apply_tmul]

Premises used: Representation.finsuppTensorRight, TensorProduct.finsuppRight_apply_tmul
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
v : V
f : α →₀ W
i : α
⊢ Eq (α := TensorProduct k V W)
    ((((σ.finsuppTensorRight ρ α : (a : TensorProduct k V (α →₀ W)) → α →₀ TensorProduct k V W) (v ⊗ₜ[k] f) :
            α →₀ TensorProduct k V W) :
          (a : α) → TensorProduct k V W)
        i :
      TensorProduct k V W)
    (v ⊗ₜ[k] (f : (a : α) → W) i : TensorProduct k V W)

Tactic:
simp +contextual [finsuppTensorRight_apply_tmul, Finsupp.sum_apply, Finsupp.single_apply]

Premises used: Representation.finsuppTensorRight_apply_tmul, Finsupp.single_apply, Finsupp.sum_apply
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
W : Type w'
inst_2 : AddCommMonoid W
k : Type u
inst_3 : CommSemiring k
inst_4 : Module k V
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_6 : DecidableEq α
i : α
v : V
w : W
⊢ Eq (α := TensorProduct.{u, v', w'} k V (α →₀ W))
    (((σ.finsuppTensorRight ρ α).symm : (a : α →₀ TensorProduct k V W) → TensorProduct k V (α →₀ W))
        (single i (v ⊗ₜ[k] w)) :
      TensorProduct.{u, v', w'} k V (α →₀ W))
    (v ⊗ₜ[k] single i w : TensorProduct.{u, v', w'} k V (α →₀ W))

Tactic:
simp [finsuppTensorRight]

Premises used: Representation.finsuppTensorRight
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g : G
a :
  ∀ (a : G) (a_1 a_2 : α) (a_3 : G),
    Eq.{u + 1} (α := k)
      (((((((TensorProduct.AlgebraTensorModule.curry
                                  ((↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                          curryLinearEquiv k) :
                                      TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k) ∘ₗ
                                    (tprod (leftRegular k G) (trivial k G (α →₀ k)) :
                                        (a : G) →
                                          TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] TensorProduct k (G →₀ k) (α →₀ k))
                                      g) ∘ₗ
                                lsingle a :
                              k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                            (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                          1 ∘ₗ
                        lsingle a_1 :
                      (a : k) → α →₀ G →₀ k)
                    1 :
                  (a : α) → G →₀ k)
                a_2 :
              G →₀ k) :
            (a : G) → k)
          a_3 :
        k)
      (((((((TensorProduct.AlgebraTensorModule.curry
                                  ((free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g ∘ₗ
                                    (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                          curryLinearEquiv k) :
                                      TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k)) ∘ₗ
                                lsingle a :
                              k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                            (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                          1 ∘ₗ
                        lsingle a_1 :
                      (a : k) → α →₀ G →₀ k)
                    1 :
                  (a : α) → G →₀ k)
                a_2 :
              G →₀ k) :
            (a : G) → k)
          a_3 :
        k)
⊢ (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ curryLinearEquiv k) :
        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k) ∘ₗ
      (tprod (leftRegular k G) (trivial k G (α →₀ k)) :
          (a : G) → TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] TensorProduct k (G →₀ k) (α →₀ k))
        g =
    (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g ∘ₗ
      (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ curryLinearEquiv k) :
        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g a : G
a_1 a_2 : α
a_3 : G
⊢ Eq.{u + 1} (α := k)
    (((((((TensorProduct.AlgebraTensorModule.curry
                                ((↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                        curryLinearEquiv k) :
                                    TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k) ∘ₗ
                                  (tprod (leftRegular k G) (trivial k G (α →₀ k)) :
                                      (a : G) →
                                        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] TensorProduct k (G →₀ k) (α →₀ k))
                                    g) ∘ₗ
                              lsingle a :
                            k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                          (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                        1 ∘ₗ
                      lsingle a_1 :
                    (a : k) → α →₀ G →₀ k)
                  1 :
                (a : α) → G →₀ k)
              a_2 :
            G →₀ k) :
          (a : G) → k)
        a_3 :
      k)
    (((((((TensorProduct.AlgebraTensorModule.curry
                                ((free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g ∘ₗ
                                  (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                        curryLinearEquiv k) :
                                    TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k)) ∘ₗ
                              lsingle a :
                            k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                          (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                        1 ∘ₗ
                      lsingle a_1 :
                    (a : k) → α →₀ G →₀ k)
                  1 :
                (a : α) → G →₀ k)
              a_2 :
            G →₀ k) :
          (a : G) → k)
        a_3 :
      k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
α : Type w'
g : G
i : α
r s : k
⊢ Eq (α := α →₀ G →₀ k)
    ((leftRegularTensorTrivialIsoFree α : (a : TensorProduct k (G →₀ k) (α →₀ k)) → α →₀ G →₀ k)
        (single g r ⊗ₜ[k] single i s) :
      α →₀ G →₀ k)
    (single i (single g (r * s)) : α →₀ G →₀ k)

Tactic:
simp [leftRegularTensorTrivialIsoFree]

Premises used: Representation.leftRegularTensorTrivialIsoFree
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
k : Type u
inst_1 : CommSemiring k
α : Type w'
i : α
g : G
r : k
⊢ Eq (α := TensorProduct k (G →₀ k) (α →₀ k))
    ((Equiv.symm (leftRegularTensorTrivialIsoFree α) : (a : α →₀ G →₀ k) → TensorProduct k (G →₀ k) (α →₀ k))
        (single i (single g r)) :
      TensorProduct k (G →₀ k) (α →₀ k))
    (single g 1 ⊗ₜ[k] single i r : TensorProduct k (G →₀ k) (α →₀ k))

Tactic:
simp [leftRegularTensorTrivialIsoFree, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Representation.leftRegularTensorTrivialIsoFree