awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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]) (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)
have 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 α))
Tactic: simp only [map_add, smul_single, smul_eq_mul, MonoidAlgebra.mul_def,
          asAlgebraHom_def, MonoidAlgebra.lift_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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]
⊢ x_1 • x = x_1 • x
have zero : HSMul.hSMul (β := α →₀ k[G]) x_1 0 = HSMul.hSMul (β := asModule (V := α →₀ G →₀ k) (free k G α)) x_1 0
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ x_1 • x = x_1 • x
have 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)
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
⊢ (tensorObj (𝒞 := Action.instCategory) V W).character = V.character * W.character
have h : ∀ (g : G), (tensorObj (𝒞 := Action.instCategory) V W).character g = (V.character * W.character) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
⊢ V.character = W.character
have h : ∀ (g : G), V.character g = W.character g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ V.character g = W.character g
have 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)
Tactic: simp only [character, FDRep.Iso.conj_ρ i]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
V : FDRep k G
g h : G
⊢ V.character (h * g * h⁻¹) = V.character g
have rw : V.character (h⁻¹ * (h * g)) = V.character g
Tactic: rw [char_mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ V.character (h * g * h⁻¹) = V.character g
have rw₁ : V.character g = V.character g
Tactic: rw [char_mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
V W : FDRep k G
g : G
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
have rw : (tensorObj (𝒞 := Action.instCategory) (of (V := Dual k (↑V.V : Type u)) (dual V.ρ)) W).character g =
  V.character g⁻¹ * W.character g
Tactic: rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
have 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
Tactic: rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
have rw₂ : character (of (V := Dual k (↑V.V : Type u)) (dual V.ρ)) g * W.character g = V.character g⁻¹ * W.character g
Tactic: rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
have rw₃ : V.character g⁻¹ * W.character g = V.character g⁻¹ * W.character g
Tactic: rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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) =
    (↑(finrank k ↥(invariants V.ρ)) : k)
have 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.ρ)
Tactic: rw [← (isProj_averageMap V.ρ).trace]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
| HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ g : G, W.character g * V.character g⁻¹)
have a : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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) _
| HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ g : G, W.character g * V.character g⁻¹)
have a₁ : ∑ g : G, W.character g * V.character g⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
| ∑ g : G, W.character g * V.character g⁻¹
have a : Finset.univ
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
| ∑ g : G, W.character g * V.character g⁻¹
have a₁ : fun (g : G) ↦ W.character g * V.character g⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
| W.character x * V.character x⁻¹
have a : (of (linHom V.ρ W.ρ)).character x
Tactic: rw [mul_comm, ← FDRep.char_linHom]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
| HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ g : G, W.character g * V.character g⁻¹)
have a : ∀ (x : G), (of (linHom V.ρ W.ρ)).character x
Tactic: congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ 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)
have 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)
Tactic: conv_lhs => congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ 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)
have rw : Eq.{u + 1} (α := k) (↑(finrank k ↥(invariants (of (linHom V.ρ W.ρ)).ρ)) : k) (↑(finrank k (V ⟶ W)) : k)
Tactic: rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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)
⊢ 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)
have rw₁ : Eq.{u + 1} (α := k) (↑(finrank k ↥(invariants (of (linHom V.ρ W.ρ)).ρ)) : k)
  (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k)
Tactic: rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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)
⊢ 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)
have rw₂ : Eq.{u + 1} (α := k) (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k) (↑(finrank k ↥(linHom V.ρ W.ρ).invariants) : k)
Tactic: rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ 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
have rw : Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (if Nonempty.{u + 1} (V ≅ W) then 1 else 0)
Tactic: rw [scalar_product_char_eq_finrank_equivariant]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (if Nonempty.{u + 1} (V ≅ W) then 1 else 0)
have rw_mod_cast : Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (↑(if Nonempty.{u + 1} (V ≅ W) then 1 else 0) : k)
Tactic: rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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)
⊢ Eq.{u + 1} (α := k) (↑(finrank k (W ⟶ V)) : k) (if Nonempty.{u + 1} (V ≅ W) then 1 else 0)
have 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)
Tactic: rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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
⊢ (ρ.tprod σ).character = ρ.character * σ.character
have h : ∀ (g : G), (ρ.tprod σ).character g = (ρ.character * σ.character) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
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 σ
⊢ ρ.character = σ.character
have h : ∀ (g : G), ρ.character g = σ.character g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g h : G
⊢ ρ.character (h * g * h⁻¹) = ρ.character g
have rw : ρ.character (h⁻¹ * (h * g)) = ρ.character g
Tactic: rw [char_mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g h : G
rw : ρ.character (h⁻¹ * (h * g)) = ρ.character g
⊢ ρ.character (h * g * h⁻¹) = ρ.character g
have rw₁ : ρ.character g = ρ.character g
Tactic: rw [char_mul_comm, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)
have have : ∀ (this : Invertible (α := k) (↑(Fintype.card G) : k)),
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)
Tactic: have : Invertible (Fintype.card G : k) := by rw [Fintype.card_eq_nat_card]; assumption
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
this : Invertible (α := k) (↑(Fintype.card G) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)
have rw : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (trace k V : (a : V →ₗ[k] V) → k) ρ.averageMap
Tactic: rw [← (isProj_averageMap ρ).trace]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group 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
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, σ.character g * ρ.character g⁻¹) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
have simp_rw : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, ρ.character x⁻¹ * σ.character x) =
  (↑(finrank k (ρ.IntertwiningMap σ)) : k)
Tactic: simp_rw [mul_comm, ← char_linHom, card_inv_mul_sum_char_eq_finrank,
    (invariantsEquivIntertwiningMap ρ σ).finrank_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group 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
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
simp_rw :
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, ρ.character x⁻¹ * σ.character x) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, σ.character g * ρ.character g⁻¹) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
have simp_rw₁ : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, (ρ.linHom σ).character x) = (↑(finrank k (ρ.IntertwiningMap σ)) : k)
Tactic: simp_rw [mul_comm, ← char_linHom, card_inv_mul_sum_char_eq_finrank,
    (invariantsEquivIntertwiningMap ρ σ).finrank_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group 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
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
simp_rw :
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, ρ.character x⁻¹ * σ.character x) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
simp_rw₁ :
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, (ρ.linHom σ).character x) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, σ.character g * ρ.character g⁻¹) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
have simp_rw₂ : Eq.{u_2 + 1} (α := k) (↑(finrank k ↥(ρ.linHom σ).invariants) : k) (↑(finrank k (ρ.IntertwiningMap σ)) : k)
Tactic: simp_rw [mul_comm, ← char_linHom, card_inv_mul_sum_char_eq_finrank,
    (invariantsEquivIntertwiningMap ρ σ).finrank_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group 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
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
inst_10 : IsAlgClosed k
inst_11 : ρ.IsIrreducible
inst_12 : σ.IsIrreducible
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
have inl : IsEmpty (σ.Equiv ρ) →
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
Tactic: cases isEmpty_or_nonempty (Equiv σ ρ)