awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
simp :
  Eq (α := V ⊗[k] W)
    (∑ x_1 ∈ r.support,
      HSMul.hSMul (α := k) (β := V ⊗[k] W) ((r : (a : G) → k) x_1 : k)
        ((((ρV : (a : G) → V →ₗ[k] V) x_1 : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : V ⊗[k] W))
    (∑ a ∈ r.support,
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) ((r : (a : G) → k) a : k)
          ((((ρV : (a : G) → V →ₗ[k] V) a : V →ₗ[k] V) : (a : V) → V) x : V) ⊗ₜ[k]
        y)
⊢ Eq (α := V ⊗[k] W)
    (Finsupp.sum r fun (i : G) (d : k) ↦
      HSMul.hSMul (β := V ⊗[k] W) d ((((ρV : (a : G) → V →ₗ[k] V) i : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : V ⊗[k] W))
    ((Finsupp.sum r fun (i : G) (d : k) ↦
        HSMul.hSMul (β := V) d ((((ρV : (a : G) → V →ₗ[k] V) i : V →ₗ[k] V) : (a : V) → V) x : V)) ⊗ₜ[k]
      y)

Tactic:
simp only [Finsupp.sum, TensorProduct.sum_tmul]

Premises used: Finsupp.sum, TensorProduct.sum_tmul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
⊢ Eq (α := V ⊗[k] W)
    (∑ x_1 ∈ r.support,
      HSMul.hSMul (α := k) (β := V ⊗[k] W) ((r : (a : G) → k) x_1 : k)
        ((((ρV : (a : G) → V →ₗ[k] V) x_1 : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : V ⊗[k] W))
    (∑ a ∈ r.support,
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) ((r : (a : G) → k) a : k)
          ((((ρV : (a : G) → V →ₗ[k] V) a : V →ₗ[k] V) : (a : V) → V) x : V) ⊗ₜ[k]
        y)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρW : Representation k G W
r : k[G]
x : V
y : W
change :
  Eq (α := V ⊗[k] W)
    ((((asAlgebraHom (1 ⊗ ρW) : (a : k[G]) → End k (V ⊗[k] W)) r : End k (V ⊗[k] W)) : (a : V ⊗[k] W) → V ⊗[k] W)
        (have this : asModule (V := V ⊗[k] W) (1 ⊗ ρW) := x ⊗ₜ[k] y;
        this) :
      V ⊗[k] W)
    (x ⊗ₜ[k]
        (((ρW.asAlgebraHom : (a : k[G]) → End k W) r : End k W) : (a : W) → W)
          (have this := y;
          this) :
      V ⊗[k] W)
⊢ HSMul.hSMul (β := asModule (V := V ⊗[k] W) (1 ⊗ ρW)) r
      (have this : asModule (V := V ⊗[k] W) (1 ⊗ ρW) := x ⊗ₜ[k] y;
      this) =
    x ⊗ₜ[k]
      HSMul.hSMul (β := ρW.asModule) r
        (have this := y;
        this)

Tactic:
change asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _

Premises used: Representation.asAlgebraHom, Representation.tprod, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρW : Representation k G W
r : k[G]
x : V
y : W
simp :
  Eq (α := V ⊗[k] W)
    (Finsupp.sum r fun (i : G) (d : k) ↦
      HSMul.hSMul (β := V ⊗[k] W) d (x ⊗ₜ[k] (((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : V ⊗[k] W))
    (x ⊗ₜ[k]
      Finsupp.sum r fun (i : G) (d : k) ↦
        HSMul.hSMul (β := W) d ((((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : W))
⊢ Eq (α := V ⊗[k] W)
    ((((asAlgebraHom (1 ⊗ ρW) : (a : k[G]) → End k (V ⊗[k] W)) r : End k (V ⊗[k] W)) : (a : V ⊗[k] W) → V ⊗[k] W)
        (have this : asModule (V := V ⊗[k] W) (1 ⊗ ρW) := x ⊗ₜ[k] y;
        this) :
      V ⊗[k] W)
    (x ⊗ₜ[k]
        (((ρW.asAlgebraHom : (a : k[G]) → End k W) r : End k W) : (a : W) → W)
          (have this := y;
          this) :
      V ⊗[k] W)

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
    LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, Module.End.one_apply]

Premises used: Representation.asAlgebraHom_def, LinearMap.smul_apply, Representation.tprod_apply, Module.End.one_apply, LinearMap.finsupp_sum_apply, MonoidAlgebra.lift_apply, TensorProduct.map_tmul, MonoidHom.one_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρW : Representation k G W
r : k[G]
x : V
y : W
⊢ Eq (α := V ⊗[k] W)
    (Finsupp.sum r fun (i : G) (d : k) ↦
      HSMul.hSMul (β := V ⊗[k] W) d (x ⊗ₜ[k] (((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : V ⊗[k] W))
    (x ⊗ₜ[k]
      Finsupp.sum r fun (i : G) (d : k) ↦
        HSMul.hSMul (β := W) d ((((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : W))

Tactic:
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]

Premises used: Finsupp.sum, TensorProduct.tmul_smul, TensorProduct.tmul_sum
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : V →ₗ[k] W
simp_rw :
  (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ
      HAdd.hAdd (α := V →ₗ[k] W) (f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) (f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) =
    HAdd.hAdd (α := V →ₗ[k] W) ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
⊢ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (f₁ + f₂) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HAdd.hAdd (α := V →ₗ[k] W) ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)

Tactic:
simp_rw [add_comp, comp_add]

Premises used: LinearMap.add_comp, LinearMap.comp_add
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : V →ₗ[k] W
simp_rw :
  (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (β := V →ₗ[k] W) r ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
simp_rw₁ :
  (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ HSMul.hSMul (β := V →ₗ[k] W) r (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) =
    HSMul.hSMul (β := V →ₗ[k] W) r ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
⊢ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (α := k) (β := V →ₗ[k] W) ((RingHom.id k : (a : k) → k) r : k)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)

Tactic:
simp_rw [RingHom.id_apply, smul_comp, comp_smul]

Premises used: LinearMap.smul_comp, RingHom.id_apply, LinearMap.comp_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
x : V →ₗ[k] W
⊢ Eq (α := V →ₗ[k] W)
    (({ toFun := fun (f : V →ₗ[k] W) ↦ (ρW : (a : G) → W →ₗ[k] W) 1 ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : V →ₗ[k] W) → V →ₗ[k] W)
        x :
      V →ₗ[k] W)
    ((1 : (a : V →ₗ[k] W) → V →ₗ[k] W) x : V →ₗ[k] W)

Tactic:
simp [Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x : V →ₗ[k] W
⊢ Eq (α := V →ₗ[k] W)
    (({ toFun := fun (f : V →ₗ[k] W) ↦ (ρW : (a : G) → W →ₗ[k] W) (g * h) ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : V →ₗ[k] W) → V →ₗ[k] W)
        x :
      V →ₗ[k] W)
    ((HMul.hMul (α := (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W)
            { toFun := fun (f : V →ₗ[k] W) ↦ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹,
              map_add' := ⋯, map_smul' := ⋯ : (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W }
            { toFun := fun (f : V →ₗ[k] W) ↦ (ρW : (a : G) → W →ₗ[k] W) h ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹,
              map_add' := ⋯, map_smul' := ⋯ : (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W } :
          (a : V →ₗ[k] W) → V →ₗ[k] W)
        x :
      V →ₗ[k] W)

Tactic:
simp [Module.End.mul_eq_comp, comp_assoc]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_assoc
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f : V →ₗ[k] W
⊢ Eq (α := V →ₗ[k] W)
    ((((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g : (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) :
          (a : V →ₗ[k] W) → V →ₗ[k] W)
        f :
      V →ₗ[k] W)
    ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : Dual k V
⊢ (f₁ + f₂) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HAdd.hAdd (α := Dual k V) (f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) (f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)

Tactic:
simp only [add_comp]

Premises used: LinearMap.add_comp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : Dual k V
h :
  ∀ (x : V),
    Eq.{u_1 + 1} (α := k) (((r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ : (a : V) → k) x : k)
      ((HSMul.hSMul (α := k) (β := Dual k V) ((RingHom.id k : (a : k) → k) r : k)
              (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) :
            (a : V) → k)
          x :
        k)
⊢ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (α := k) (β := Dual k V) ((RingHom.id k : (a : k) → k) r : k) (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : Dual k V
x : V
⊢ Eq.{u_1 + 1} (α := k) (((r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ : (a : V) → k) x : k)
    ((HSMul.hSMul (α := k) (β := Dual k V) ((RingHom.id k : (a : k) → k) r : k) (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) :
          (a : V) → k)
        x :
      k)

Tactic:
simp only [coe_comp, Function.comp_apply, smul_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
h :
  ∀ (x : Dual k V) (x_1 : V),
    Eq.{u_1 + 1} (α := k)
      (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } :
                  (a : Dual k V) → Dual k V)
                x :
              Dual k V) :
            (a : V) → k)
          x_1 :
        k)
      ((((1 : (a : Dual k V) → Dual k V) x : Dual k V) : (a : V) → k) x_1 : k)
⊢ Eq (α := Dual k V →ₗ[k] Dual k V)
    { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
x : Dual k V
x_1 : V
⊢ Eq.{u_1 + 1} (α := k)
    (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)
    ((((1 : (a : Dual k V) → Dual k V) x : Dual k V) : (a : V) → k) x_1 : k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
h₁ :
  ∀ (x : Dual k V) (x_1 : V),
    Eq.{u_1 + 1} (α := k)
      (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } :
                  (a : Dual k V) → Dual k V)
                x :
              Dual k V) :
            (a : V) → k)
          x_1 :
        k)
      ((((HMul.hMul (α := Dual k V →ₗ[k] Dual k V)
                    { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹, map_add' := ⋯, map_smul' := ⋯ :
                      Dual k V →ₗ[k] Dual k V }
                    { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹, map_add' := ⋯, map_smul' := ⋯ :
                      Dual k V →ₗ[k] Dual k V } :
                  (a : Dual k V) → Dual k V)
                x :
              Dual k V) :
            (a : V) → k)
          x_1 :
        k)
⊢ { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := Dual k V →ₗ[k] Dual k V)
      { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹, map_add' := ⋯, map_smul' := ⋯ :
        Dual k V →ₗ[k] Dual k V }
      { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹, map_add' := ⋯, map_smul' := ⋯ :
        Dual k V →ₗ[k] Dual k V }

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x : Dual k V
x_1 : V
⊢ Eq.{u_1 + 1} (α := k)
    (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)
    ((((HMul.hMul (α := Dual k V →ₗ[k] Dual k V)
                  { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹, map_add' := ⋯, map_smul' := ⋯ :
                    Dual k V →ₗ[k] Dual k V }
                  { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹, map_add' := ⋯, map_smul' := ⋯ :
                    Dual k V →ₗ[k] Dual k V } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρV : Representation k G V
g : G
⊢ Eq (α := Dual k V →ₗ[k] Dual k V) ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g : Dual k V →ₗ[k] Dual k V)
    ((Dual.transpose : (a : V →ₗ[k] V) → Dual k V →ₗ[k] Dual k V) ((ρV : (a : G) → V →ₗ[k] V) g⁻¹) :
      Dual k V →ₗ[k] Dual k V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
a :
  ∀ (x : Dual k V) (x_1 : W) (x_2 : V),
    Eq.{u_4 + 1} (α := W)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            (dualTensorHom k V W ∘ₗ
                              TensorProduct.map ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g)
                                ((ρW : (a : G) → W →ₗ[k] W) g)) :
                          Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                        (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                      x :
                    W →ₗ[k] V →ₗ[k] W) :
                  (a : W) → V →ₗ[k] W)
                x_1 :
              V →ₗ[k] W) :
            (a : V) → W)
          x_2 :
        W)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            ((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ dualTensorHom k V W) :
                          Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                        (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                      x :
                    W →ₗ[k] V →ₗ[k] W) :
                  (a : W) → V →ₗ[k] W)
                x_1 :
              V →ₗ[k] W) :
            (a : V) → W)
          x_2 :
        W)
⊢ Eq (α := TensorProduct k (Dual k V) W →ₗ[k] V →ₗ[k] W)
    (dualTensorHom k V W ∘ₗ
      TensorProduct.map ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g) ((ρW : (a : G) → W →ₗ[k] W) g))
    ((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ dualTensorHom k V W)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
x : Dual k V
x_1 : W
x_2 : V
⊢ Eq.{u_4 + 1} (α := W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (dualTensorHom k V W ∘ₗ
                            TensorProduct.map ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g)
                              ((ρW : (a : G) → W →ₗ[k] W) g)) :
                        Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    x :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              x_1 :
            V →ₗ[k] W) :
          (a : V) → W)
        x_2 :
      W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ dualTensorHom k V W) :
                        Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    x :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              x_1 :
            V →ₗ[k] W) :
          (a : V) → W)
        x_2 :
      W)

Tactic:
simp [Module.Dual.transpose_apply]

Premises used: Module.Dual.transpose_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x : α
x_1 : A
⊢ Eq (α := α →₀ A)
    (((Finsupp.lsum k : (a : α → A →ₗ[k] α →₀ A) → (α →₀ A) →ₗ[k] α →₀ A) fun (i : α) ↦
            lsingle i ∘ₗ (ρ : (a : G) → A →ₗ[k] A) 1 :
          (a : α →₀ A) → α →₀ A)
        (Finsupp.single x x_1) :
      α →₀ A)
    ((1 : (a : α →₀ A) → α →₀ A) (Finsupp.single x x_1) : α →₀ A)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x x_1 : G
x_2 : α
x_3 : A
⊢ Eq (α := α →₀ A)
    (((Finsupp.lsum k : (a : α → A →ₗ[k] α →₀ A) → (α →₀ A) →ₗ[k] α →₀ A) fun (i : α) ↦
            lsingle i ∘ₗ (ρ : (a : G) → A →ₗ[k] A) (x * x_1) :
          (a : α →₀ A) → α →₀ A)
        (Finsupp.single x_2 x_3) :
      α →₀ A)
    ((HMul.hMul (α := (α →₀ A) →ₗ[k] α →₀ A)
            ((Finsupp.lsum k : (a : α → A →ₗ[k] α →₀ A) → (α →₀ A) →ₗ[k] α →₀ A) fun (i : α) ↦
              lsingle i ∘ₗ (ρ : (a : G) → A →ₗ[k] A) x)
            ((Finsupp.lsum k : (a : α → A →ₗ[k] α →₀ A) → (α →₀ A) →ₗ[k] α →₀ A) fun (i : α) ↦
              lsingle i ∘ₗ (ρ : (a : G) → A →ₗ[k] A) x_1) :
          (a : α →₀ A) → α →₀ A)
        (Finsupp.single x_2 x_3) :
      α →₀ A)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α : Type u_3
A : Type u_4
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
g : G
x : α
a : A
⊢ Eq (α := α →₀ A)
    ((((ρ.finsupp α : (a : G) → (α →₀ A) →ₗ[k] α →₀ A) g : (α →₀ A) →ₗ[k] α →₀ A) : (a : α →₀ A) → α →₀ A)
        (Finsupp.single x a) :
      α →₀ A)
    (Finsupp.single x ((((ρ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) a) : α →₀ A)

Tactic:
simp [finsupp_apply]

Premises used: Representation.finsupp_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α : Type u_3
g h : G
i : α
r : k
⊢ Eq (α := α →₀ G →₀ k)
    ((((free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g : (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) :
          (a : α →₀ G →₀ k) → α →₀ G →₀ k)
        (Finsupp.single i (Finsupp.single h r)) :
      α →₀ G →₀ k)
    (Finsupp.single i (Finsupp.single (g * h) r) : α →₀ G →₀ k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x_1 : k[G]
x : α →₀ k[G]
simp : x_1 • x = x_1 • x
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (α →₀ k[G]))) (x_1 • x) =
    HSMul.hSMul (α := k[G]) ((RingHom.id k[G] : (a : k[G]) → k[G]) x_1 : k[G])
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (α →₀ k[G]))) x)

Tactic:
simp only [AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
        AddEquiv.refl_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe, AddEquiv.refl_apply, EquivLike.coe_coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x : k[G]
⊢ HSMul.hSMul (β := α →₀ k[G]) x 0 = HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α)) x 0

Tactic:
simp only [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x : k[G]
a : α
b : k[G]
f : α →₀ k[G]
h_1 : a ∉ f.support
h_2 : b ≠ 0
h : x • f = x • f
single_add : HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b) + x • f = x • (Finsupp.single a b + f)
⊢ x • (Finsupp.single a b + f) = x • (Finsupp.single a b + f)

Tactic:
rw [smul_add, h]

Premises used: smul_add