awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ (↑(assoc ρ σ τ).symm : (ρ.tprod (σ.tprod τ)).IntertwiningMap ((ρ.tprod σ).tprod τ)).toLinearMap =
    (↑(LinearEquiv.symm (_root_.TensorProduct.assoc A V W U)) :
      TensorProduct A V (TensorProduct A W U) →ₗ[A] TensorProduct A (TensorProduct A V W) U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
v : V
w : W
u : U
⊢ Eq (α := TensorProduct A V (TensorProduct A W U))
    ((assoc ρ σ τ : (a : TensorProduct A (TensorProduct A V W) U) → TensorProduct A V (TensorProduct A W U))
        (v ⊗ₜ[A] w ⊗ₜ[A] u) :
      TensorProduct A V (TensorProduct A W U))
    (v ⊗ₜ[A] (w ⊗ₜ[A] u) : TensorProduct A V (TensorProduct A W U))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
a :
  ∀ (x : W),
    Eq.{u_4 + 1} (α := W)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W) ∘ₗ
                        (σ.tprod (trivial A G A) : (a : G) → TensorProduct A W A →ₗ[A] TensorProduct A W A) g) :
                    W →ₗ[A] A →ₗ[A] W) :
                  (a : W) → A →ₗ[A] W)
                x :
              A →ₗ[A] W) :
            (a : A) → W)
          1 :
        W)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W)) :
                    W →ₗ[A] A →ₗ[A] W) :
                  (a : W) → A →ₗ[A] W)
                x :
              A →ₗ[A] W) :
            (a : A) → W)
          1 :
        W)
⊢ Eq (α := TensorProduct A W A →ₗ[A] W)
    ((↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W) ∘ₗ
      (σ.tprod (trivial A G A) : (a : G) → TensorProduct A W A →ₗ[A] TensorProduct A W A) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x : W
⊢ Eq.{u_4 + 1} (α := W)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W) ∘ₗ
                      (σ.tprod (trivial A G A) : (a : G) → TensorProduct A W A →ₗ[A] TensorProduct A W A) g) :
                  W →ₗ[A] A →ₗ[A] W) :
                (a : W) → A →ₗ[A] W)
              x :
            A →ₗ[A] W) :
          (a : A) → W)
        1 :
      W)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W)) :
                  W →ₗ[A] A →ₗ[A] W) :
                (a : W) → A →ₗ[A] W)
              x :
            A →ₗ[A] W) :
          (a : A) → W)
        1 :
      W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
⊢ (↑(rid A σ) : (σ.tprod (trivial A G A)).IntertwiningMap σ).toLinearMap =
    (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W)

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
w : W
a : A
⊢ (rid A σ : (a : TensorProduct A W A) → W) (w ⊗ₜ[A] a) = a • w

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
w : W
⊢ Eq (α := TensorProduct A W A) (((rid A σ).symm : (a : W) → TensorProduct A W A) w : TensorProduct A W A)
    (w ⊗ₜ[A] 1 : TensorProduct A W A)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
a :
  ∀ (x : W),
    Eq (α := W)
      ((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W) ∘ₗ
                      (tprod (trivial A G A) σ : (a : G) → TensorProduct A A W →ₗ[A] TensorProduct A A W) g) :
                  LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
                (a : A) → W →ₗ[A] W)
              1 :
            (a : W) → W)
          x :
        W)
      ((((TensorProduct.AlgebraTensorModule.curry
                    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W)) :
                  LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
                (a : A) → W →ₗ[A] W)
              1 :
            (a : W) → W)
          x :
        W)
⊢ Eq (α := TensorProduct A A W →ₗ[A] W)
    ((↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W) ∘ₗ
      (tprod (trivial A G A) σ : (a : G) → TensorProduct A A W →ₗ[A] TensorProduct A A W) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x : W
⊢ Eq (α := W)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W) ∘ₗ
                    (tprod (trivial A G A) σ : (a : G) → TensorProduct A A W →ₗ[A] TensorProduct A A W) g) :
                LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
              (a : A) → W →ₗ[A] W)
            1 :
          (a : W) → W)
        x :
      W)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W)) :
                LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
              (a : A) → W →ₗ[A] W)
            1 :
          (a : W) → W)
        x :
      W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
⊢ (↑(lid A σ) : ((trivial A G A).tprod σ).IntertwiningMap σ).toLinearMap =
    (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W)

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
a : A
w : W
⊢ (lid A σ : (a : TensorProduct A A W) → W) (a ⊗ₜ[A] w) = a • w

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
σ : Representation A G W
w : W
⊢ Eq (α := TensorProduct A A W) (((lid A σ).symm : (a : W) → TensorProduct A A W) w : TensorProduct A A W)
    (1 ⊗ₜ[A] w : TensorProduct A A W)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G_1
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G_1 V_1
σ_1 : Representation A G_1 W_1
τ : Representation A G_1 U
f : V_1 →ₗ[A] W_1
G : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst_8 : Group G
inst_9 : Field k
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
inst_14 : FiniteDimensional k V
inst_15 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
a :
  ∀ (v' : Module.Dual k V) (w : W) (v : V),
    Eq.{u_9 + 1} (α := W)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            ((↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W) ∘ₗ
                              (ρ.dual.tprod σ :
                                  (a : G) →
                                    TensorProduct k (Module.Dual k V) W →ₗ[k] TensorProduct k (Module.Dual k V) W)
                                g) :
                          Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                        (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                      v' :
                    W →ₗ[k] V →ₗ[k] W) :
                  (a : W) → V →ₗ[k] W)
                w :
              V →ₗ[k] W) :
            (a : V) → W)
          v :
        W)
      (((((((TensorProduct.AlgebraTensorModule.curry
                            ((ρ.linHom σ : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ
                              (↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W)) :
                          Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                        (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                      v' :
                    W →ₗ[k] V →ₗ[k] W) :
                  (a : W) → V →ₗ[k] W)
                w :
              V →ₗ[k] W) :
            (a : V) → W)
          v :
        W)
⊢ Eq (α := TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W)
    ((↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W) ∘ₗ
      (ρ.dual.tprod σ : (a : G) → TensorProduct k (Module.Dual k V) W →ₗ[k] TensorProduct k (Module.Dual k V) W) g)
    ((ρ.linHom σ : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ
      (↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W))

Tactic:
ext v' w v
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G_1
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G_1 V_1
σ_1 : Representation A G_1 W_1
τ : Representation A G_1 U
f : V_1 →ₗ[A] W_1
G : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst_8 : Group G
inst_9 : Field k
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
inst_14 : FiniteDimensional k V
inst_15 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
v' : Module.Dual k V
w : W
v : V
⊢ Eq.{u_9 + 1} (α := W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W) ∘ₗ
                            (ρ.dual.tprod σ :
                                (a : G) → TensorProduct k (Module.Dual k V) W →ₗ[k] TensorProduct k (Module.Dual k V) W)
                              g) :
                        Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    v' :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              w :
            V →ₗ[k] W) :
          (a : V) → W)
        v :
      W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((ρ.linHom σ : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ
                            (↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W)) :
                        Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    v' :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              w :
            V →ₗ[k] W) :
          (a : V) → W)
        v :
      W)

Tactic:
simp [Module.Dual.transpose_apply]

Premises used: Module.Dual.transpose_apply
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
simp :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)
⊢ HMul.hMul (α := k[G]) (Finsupp.single g 1) (average k G) = average k G

Tactic:
simp only [mul_one, Finset.mul_sum, Algebra.mul_smul_comm, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]

Premises used: Finset.mul_sum, Algebra.mul_smul_comm, GroupAlgebra.average, MonoidAlgebra.single_mul_single, mul_one, MonoidAlgebra.of_apply
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
set :
  let f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1;
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)

Tactic:
set f : G → k[G] := fun x => Finsupp.single x 1

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
change :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (g * x)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)

Tactic:
change ⅟(Fintype.card G : k) • ∑ x : G, f (g * x) = ⅟(Fintype.card G : k) • ∑ x : G, f x

Premises used: Fintype.card, Nat.cast
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
rw rw₁ :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ i : G, f i) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (g * x)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)

Tactic:
rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]

Premises used: Function.Bijective.sum_comp, Group.mulLeft_bijective
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
simp :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)
⊢ HMul.hMul (α := k[G]) (average k G) (Finsupp.single g 1) = average k G

Tactic:
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]

Premises used: GroupAlgebra.average, MonoidAlgebra.single_mul_single, Algebra.smul_mul_assoc, mul_one, Finset.sum_mul, MonoidAlgebra.of_apply
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
set :
  let f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1;
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)

Tactic:
set f : G → k[G] := fun x => Finsupp.single x 1

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
change :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (x * g)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)

Tactic:
change ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x

Premises used: Fintype.card, Nat.cast
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
rw rw₁ :
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ i : G, f i) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (x * g)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)

Tactic:
rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]

Premises used: Function.Bijective.sum_comp, Group.mulRight_bijective
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
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
a b : V
hv : Membership.mem (γ := Set V) {v : V | ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v} a
hw : Membership.mem (γ := Set V) {v : V | ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v} b
g : G
⊢ (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) (a + b) = a + b

Tactic:
simp only [hv g, hw g, map_add]

Premises used: map_add
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
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
g : G
⊢ Eq.{u_3 + 1} (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) 0 : V) (0 : V)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
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
r : k
v : V
hv : Membership.mem (γ := Set V) {v : V | ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v} v
g : G
⊢ (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) (r • v) = r • v

Tactic:
simp only [hv g, map_smulₛₗ, RingHom.id_apply]

Premises used: RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ ρ.invariants ↔ ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
h :
  ∀ (x : V),
    x ∈ ρ.invariants.carrier ↔
      Membership.mem (γ := Set V)
        (⋂ (g : G), Function.fixedPoints (⇑((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)) x
⊢ ρ.invariants.carrier = ⋂ (g : G), Function.fixedPoints (⇑((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)

Tactic:
ext