awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  HAdd.hAdd (β := α →₀ k[G]) (HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b))
      ((((asAlgebraHom (free k G α) : (a : k[G]) → End k (α →₀ k[G])) x : End k (α →₀ k[G])) :
            (a : α →₀ k[G]) → α →₀ k[G])
          f :
        α →₀ k[G]) =
    (((asAlgebraHom (free k G α) : (a : k[G]) → End k (free k G α).asModule) x :
          End k (asModule (V := α →₀ G →₀ k) (free k G α))) :
        (a : (free k G α).asModule) → (free k G α).asModule)
      (Finsupp.single a b + f)
⊢ HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b) + x • f = x • (Finsupp.single a b + f)

Tactic:
change _ + asAlgebraHom _ _ _ = asAlgebraHom _ _ _

Premises used: Representation.asAlgebraHom, DFunLike.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]
a : α
b : k[G]
f : α →₀ k[G]
h_1 : a ∉ f.support
h_2 : b ≠ 0
h : x • f = x • f
single_add :
  HAdd.hAdd (α := α →₀ k[G]) (β := α →₀ k[G])
      (Finsupp.single a
        (sum x fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ MonoidAlgebra.single (m₁ * m₂) (r₁ * r₂)))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := (α →₀ k[G]) →ₗ[k] α →₀ k[G]) b
                ((free k G α : (a : G) → (α →₀ k[G]) →ₗ[k] α →₀ k[G]) a : (α →₀ k[G]) →ₗ[k] α →₀ k[G]) :
            (a : α →₀ k[G]) → α →₀ k[G])
          f :
        α →₀ k[G]) =
    HAdd.hAdd (α := asModule (V := α →₀ G →₀ k) (free k G α)) (β := asModule (V := α →₀ G →₀ k) (free k G α))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α))
                b
                ((free k G α : (a : G) → (free k G α).asModule →ₗ[k] (free k G α).asModule) a :
                  asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α)) :
            (a : (free k G α).asModule) → (free k G α).asModule)
          (Finsupp.single a b) :
        asModule (V := α →₀ G →₀ k) (free k G α))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α))
                b
                ((free k G α : (a : G) → (free k G α).asModule →ₗ[k] (free k G α).asModule) a :
                  asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α)) :
            (a : (free k G α).asModule) → (free k G α).asModule)
          f :
        asModule (V := α →₀ G →₀ k) (free k G α))
⊢ HAdd.hAdd (β := α →₀ k[G]) (HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b))
      ((((asAlgebraHom (free k G α) : (a : k[G]) → End k (α →₀ k[G])) x : End k (α →₀ k[G])) :
            (a : α →₀ k[G]) → α →₀ k[G])
          f :
        α →₀ k[G]) =
    (((asAlgebraHom (free k G α) : (a : k[G]) → End k (free k G α).asModule) x :
          End k (asModule (V := α →₀ G →₀ k) (free k G α))) :
        (a : (free k G α).asModule) → (free k G α).asModule)
      (Finsupp.single a b + f)

Tactic:
simp only [map_add, smul_single, smul_eq_mul, MonoidAlgebra.mul_def,
          asAlgebraHom_def, MonoidAlgebra.lift_apply]

Premises used: MonoidAlgebra.mul_def, Representation.asAlgebraHom_def, map_add, MonoidAlgebra.lift_apply, smul_eq_mul, Finsupp.smul_single
-- 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
⊢ HAdd.hAdd (α := α →₀ k[G]) (β := α →₀ k[G])
      (Finsupp.single a
        (sum x fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ MonoidAlgebra.single (m₁ * m₂) (r₁ * r₂)))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := (α →₀ k[G]) →ₗ[k] α →₀ k[G]) b
                ((free k G α : (a : G) → (α →₀ k[G]) →ₗ[k] α →₀ k[G]) a : (α →₀ k[G]) →ₗ[k] α →₀ k[G]) :
            (a : α →₀ k[G]) → α →₀ k[G])
          f :
        α →₀ k[G]) =
    HAdd.hAdd (α := asModule (V := α →₀ G →₀ k) (free k G α)) (β := asModule (V := α →₀ G →₀ k) (free k G α))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α))
                b
                ((free k G α : (a : G) → (free k G α).asModule →ₗ[k] (free k G α).asModule) a :
                  asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α)) :
            (a : (free k G α).asModule) → (free k G α).asModule)
          (Finsupp.single a b) :
        asModule (V := α →₀ G →₀ k) (free k G α))
      ((sum x fun (a : G) (b : k) ↦
              HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α))
                b
                ((free k G α : (a : G) → (free k G α).asModule →ₗ[k] (free k G α).asModule) a :
                  asModule (V := α →₀ G →₀ k) (free k G α) →ₗ[k] asModule (V := α →₀ G →₀ k) (free k G α)) :
            (a : (free k G α).asModule) → (free k G α).asModule)
          f :
        asModule (V := α →₀ G →₀ k) (free k G α))

Tactic:
simp [free, MonoidAlgebra, asModule, ofMulAction_def, mapDomain, smul_sum, single_sum]

Premises used: Finsupp.mapDomain, Representation.free, Representation.asModule, MonoidAlgebra, Finsupp.smul_sum, Finsupp.single_sum, Representation.ofMulAction_def
-- 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]
zero : HSMul.hSMul (β := α →₀ k[G]) x_1 0 = HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α)) x_1 0
single_add :
  ∀ (a : α) (b : k[G]) (f : α →₀ k[G]),
    a ∉ f.support → b ≠ 0 → ∀ (h : x_1 • f = x_1 • f), x_1 • (Finsupp.single a b + f) = x_1 • (Finsupp.single a b + f)
⊢ x_1 • x = x_1 • x

Tactic:
induction x using Finsupp.induction with
      | zero => simp only [smul_zero]
      | single_add _ _ _ _ _ h =>
        rw [smul_add, h]
        change _ + asAlgebraHom _ _ _ = asAlgebraHom _ _ _
        simp only [map_add, smul_single, smul_eq_mul, MonoidAlgebra.mul_def,
          asAlgebraHom_def, MonoidAlgebra.lift_apply]
        simp [free, MonoidAlgebra, asModule, ofMulAction_def, mapDomain, smul_sum, single_sum]

Premises used: MonoidAlgebra.mul_def, Representation.asAlgebraHom_def, Representation.asAlgebraHom, Finsupp.mapDomain, smul_zero, map_add, Representation.free, Representation.asModule, Finsupp.single_add, MonoidAlgebra.lift_apply, MonoidAlgebra, Finsupp.smul_sum, smul_eq_mul, Finsupp.single_sum, DFunLike.coe, Finsupp.smul_single, smul_add, Representation.ofMulAction_def
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α : Type u_6
⊢ Free k[G] (asModule (V := α →₀ G →₀ k) (free k G α))

Tactic:
Module.Free.of_basis (freeAsModuleBasis k G α)

Premises used: Module.Free.of_basis, Representation.freeAsModuleBasis
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V : FDRep k G
g h : G
⊢ V.character (h * g) = V.character (g * h)

Tactic:
simp only [trace_mul_comm, character, map_mul]

Premises used: LinearMap.trace_mul_comm, FDRep.character, map_mul
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V : FDRep k G
⊢ V.character 1 = (↑(finrank k (↑V.V : Type u)) : k)

Tactic:
simp only [character, map_one, trace_one]

Premises used: LinearMap.trace_one, FDRep.character, map_one
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
h : ∀ (g : G), (tensorObj (𝒞 := Action.instCategory) V W).character g = (V.character * W.character) g
⊢ (tensorObj (𝒞 := Action.instCategory) V W).character = V.character * W.character

Tactic:
ext g
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
g : G
⊢ (trace k (TensorProduct k (↑V.V : Type u) (↑W.V : Type u)) :
        (a : TensorProduct k (↑V.V : Type u) (↑W.V : Type u) →ₗ[k] TensorProduct k (↑V.V : Type u) (↑W.V : Type u)) → k)
      (TensorProduct.map ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g)
        ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) g)) =
    HMul.hMul (α := k) (β := k)
      ((trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k)
          ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) :
        k)
      ((trace k (↑W.V : Type u) : (a : (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) → k)
          ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) g : (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) :
        k)

Tactic:
trace_tensorProduct' (V.ρ g) (W.ρ g)

Premises used: LinearMap.trace_tensorProduct', DFunLike.coe, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
g : G
⊢ (tensorObj (𝒞 := Action.instCategory) V W).character g = (V.character * W.character) g

Tactic:
convert! trace_tensorProduct' (V.ρ g) (W.ρ g)

Premises used: LinearMap.trace_tensorProduct', DFunLike.coe, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
h : ∀ (g : G), V.character g = W.character g
⊢ V.character = W.character

Tactic:
ext g
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
h :
  Eq (α := k)
    ((trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k)
        ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) :
      k)
    ((trace k (↑W.V : Type u) : (a : (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) → k)
        (((isoToLinearEquiv i).conj : (a : Module.End k (↑V.V : Type u)) → Module.End k (↑W.V : Type u))
            ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g) :
          Module.End k (↑W.V : Type u)) :
      k)
⊢ V.character g = W.character g

Tactic:
simp only [character, FDRep.Iso.conj_ρ i]

Premises used: FDRep.character, FDRep.Iso.conj_ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ Eq (α := k)
    ((trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k)
        ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) :
      k)
    ((trace k (↑W.V : Type u) : (a : (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) → k)
        (((isoToLinearEquiv i).conj : (a : Module.End k (↑V.V : Type u)) → Module.End k (↑W.V : Type u))
            ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g) :
          Module.End k (↑W.V : Type u)) :
      k)

Tactic:
(trace_conj' (V.ρ g) _).symm

Premises used: LinearMap.trace_conj', Eq.symm, DFunLike.coe, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ Eq (α := k)
    ((trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k)
        ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) :
      k)
    ((trace k (↑W.V : Type u) : (a : (↑W.V : Type u) →ₗ[k] (↑W.V : Type u)) → k)
        (((isoToLinearEquiv i).conj : (a : Module.End k (↑V.V : Type u)) → Module.End k (↑W.V : Type u))
            ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) g) :
          Module.End k (↑W.V : Type u)) :
      k)

Tactic:
exact (trace_conj' (V.ρ g) _).symm

Premises used: LinearMap.trace_conj', Eq.symm, DFunLike.coe, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
V : FDRep k G
g h : G
rw : V.character (h⁻¹ * (h * g)) = V.character g
rw₁ rw₂ : V.character g = V.character g
⊢ V.character (h * g * h⁻¹) = V.character g

Tactic:
rw [char_mul_comm, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, FDRep.char_mul_comm
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
V : FDRep k G
g : G
⊢ character (of (V := Dual k (↑V.V : Type u)) (dual V.ρ)) g = V.character g⁻¹

Tactic:
trace_transpose' (V.ρ g⁻¹)

Premises used: FDRep.character, LinearMap.trace_transpose', Inv.inv, DFunLike.coe, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
V W : FDRep k G
g : G
rw :
  (tensorObj (𝒞 := Action.instCategory) (of (V := Dual k (↑V.V : Type u)) (dual V.ρ)) W).character g =
    V.character g⁻¹ * W.character g
rw₁ :
  HMul.hMul (α := (g : G) → k) (character (of (V := Dual k (↑V.V : Type u)) (dual V.ρ))) W.character g =
    V.character g⁻¹ * W.character g
rw₂ : character (of (V := Dual k (↑V.V : Type u)) (dual V.ρ)) g * W.character g = V.character g⁻¹ * W.character g
rw₃ rw₄ : V.character g⁻¹ * W.character g = V.character g⁻¹ * W.character g
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g

Tactic:
rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]

Premises used: FDRep.char_tensor, Pi.mul_apply, FDRep.char_iso, FDRep.char_dual, FDRep.dualTensorIsoLinHom
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V : FDRep k G
rw :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g) =
    (trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k) (averageMap V.ρ)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g) =
    (↑(finrank k ↥(invariants V.ρ)) : k)

Tactic:
rw [← (isProj_averageMap V.ρ).trace]

Premises used: Representation.isProj_averageMap, LinearMap.IsProj.trace, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V : FDRep k G
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g) =
    (trace k (↑V.V : Type u) : (a : (↑V.V : Type u) →ₗ[k] (↑V.V : Type u)) → k) (averageMap V.ρ)

Tactic:
simp [character, GroupAlgebra.average, _root_.map_sum]

Premises used: GroupAlgebra.average, FDRep.character, map_sum
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
a : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _
a₁ : ∑ g : G, W.character g * V.character g⁻¹
| HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ g : G, W.character g * V.character g⁻¹)

Tactic:
congr
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
| @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
a : Finset.univ
a₁ : fun (g : G) ↦ W.character g * V.character g⁻¹
| ∑ g : G, W.character g * V.character g⁻¹

Tactic:
congr
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
| Finset.univ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
x : G
a : (of (linHom V.ρ W.ρ)).character x
| W.character x * V.character x⁻¹

Tactic:
rw [mul_comm, ← FDRep.char_linHom]

Premises used: FDRep.char_linHom, mul_comm
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
a : ∀ (x : G), (of (linHom V.ρ W.ρ)).character x
| HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ g : G, W.character g * V.character g⁻¹)

Tactic:
congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]

Premises used: FDRep.char_linHom, mul_comm
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
conv_lhs :
  HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ (of (linHom V.ρ W.ρ)).character) =
    (↑(finrank k (V ⟶ W)) : k)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, W.character g * V.character g⁻¹) =
    (↑(finrank k (V ⟶ W)) : k)

Tactic:
conv_lhs => congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]

Premises used: FDRep.char_linHom, mul_comm
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
rw : Eq.{u + 1} (α := k) (↑(finrank k ↥(invariants (of (linHom V.ρ W.ρ)).ρ)) : k) (↑(finrank k (V ⟶ W)) : k)
rw₁ :
  Eq.{u + 1} (α := k) (↑(finrank k ↥(invariants (of (linHom V.ρ W.ρ)).ρ)) : k)
    (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k)
rw₂ rw₃ :
  Eq.{u + 1} (α := k) (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k) (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k)
⊢ HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ (of (linHom V.ρ W.ρ)).character) =
    (↑(finrank k (V ⟶ W)) : k)

Tactic:
rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']

Premises used: FDRep.of_ρ', FDRep.average_char_eq_finrank_invariants, LinearEquiv.finrank_eq, Representation.linHom.invariantsEquivFDRepHom
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : IsAlgClosed k
inst_3 : Fintype G
inst_4 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
inst_5 : Simple V
inst_6 : Simple W
rw : Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (if Nonempty.{u + 1} (V ≅ W) then 1 else 0)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g * W.character g⁻¹) =
    if Nonempty.{u + 1} (V ≅ W) then 1 else 0

Tactic:
rw [scalar_product_char_eq_finrank_equivariant]

Premises used: FDRep.scalar_product_char_eq_finrank_equivariant
-- Module: Mathlib.RepresentationTheory.Character
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
inst_2 : IsAlgClosed k
inst_3 : Fintype G
inst_4 : Invertible (α := k) (↑(Fintype.card G) : k)
V W : FDRep k G
inst_5 : Simple V
inst_6 : Simple W
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (↑(if Nonempty.{u + 1} (V ≅ W) then 1 else 0) : k)
rw_mod_cast₆ :
  Eq.{u + 1} (α := k) (↑(if Nonempty.{u + 1} (W ≅ V) then 1 else 0) : k)
    (↑(if Nonempty.{u + 1} (V ≅ W) then 1 else 0) : k)
⊢ Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (if Nonempty.{u + 1} (V ≅ W) then 1 else 0)

Tactic:
rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]

Premises used: CategoryTheory.Iso.nonempty_iso_symm, FDRep.finrank_hom_simple_simple
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g h : G
⊢ ρ.character (h * g) = ρ.character (g * h)

Tactic:
simp only [trace_mul_comm, character, map_mul]

Premises used: Representation.character, LinearMap.trace_mul_comm, map_mul
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
⊢ ρ.character 1 = (↑(finrank k V) : k)

Tactic:
simp only [character, map_one, trace_one]

Premises used: Representation.character, LinearMap.trace_one, map_one
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
h : ∀ (g : G), (ρ.tprod σ).character g = (ρ.character * σ.character) g
⊢ (ρ.tprod σ).character = ρ.character * σ.character

Tactic:
ext g
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ (trace k (TensorProduct k V W) : (a : TensorProduct k V W →ₗ[k] TensorProduct k V W) → k)
      (TensorProduct.map ((ρ : (a : G) → V →ₗ[k] V) g) ((σ : (a : G) → W →ₗ[k] W) g)) =
    HMul.hMul (α := k) (β := k) ((trace k V : (a : V →ₗ[k] V) → k) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : k)
      ((trace k W : (a : W →ₗ[k] W) → k) ((σ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : k)

Tactic:
trace_tensorProduct' (ρ g) (σ g)

Premises used: LinearMap.trace_tensorProduct', DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ (ρ.tprod σ).character g = (ρ.character * σ.character) g

Tactic:
convert! trace_tensorProduct' (ρ g) (σ g)

Premises used: LinearMap.trace_tensorProduct', DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field 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
φ : ρ.Equiv σ
h : ∀ (g : G), ρ.character g = σ.character g
⊢ ρ.character = σ.character

Tactic:
ext g