awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Irreducible
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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
inst_7 : σ.IsIrreducible
rw :
  Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨ f = 0

Tactic:
rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]

Premises used: Representation.IntertwiningMap.equivLinearMapAsModule, LinearEquiv.map_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Irreducible
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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
inst_7 : σ.IsIrreducible
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)

Tactic:
LinearMap.bijective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Premises used: Representation.instAddCommMonoidAsModule._aux_4, Representation.asModule, Representation.instAddCommMonoidAsModule._aux_1, Representation.IntertwiningMap.equivLinearMapAsModule, LinearMap.bijective_or_eq_zero, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Irreducible
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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
inst_7 : σ.IsIrreducible
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨
    Eq (α := LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      ((equivLinearMapAsModule ρ σ : (a : ρ.IntertwiningMap σ) → ρ.asModule →ₗ[k[G]] σ.asModule) f :
        LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)
      (0 : LinearMap (R := k[G]) (RingHom.id k[G]) ρ.asModule σ.asModule)

Tactic:
exact LinearMap.bijective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Premises used: Representation.IntertwiningMap.equivLinearMapAsModule, LinearMap.bijective_or_eq_zero, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Irreducible
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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
inst_7 : σ.IsIrreducible
inst_8 : IsEmpty (ρ.Equiv σ)
⊢ Subsingleton (ρ.IntertwiningMap σ)

Tactic:
⟨fun f g ↦ sub_eq_zero.mp <| (bijective_or_eq_zero _).resolve_left
    fun h ↦ isEmpty_iff.mp inferInstance <| (f - g).ofBijective h⟩

Premises used: Representation.IntertwiningMap.ofBijective, sub_eq_zero, isEmpty_iff, HSub.hSub, Representation.IsIrreducible.bijective_or_eq_zero, inferInstance, Or.resolve_left, Subsingleton.intro, Iff.mp
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
⊢ Bijective.{u_2 + 1, u_3 + 1} (α := k) (β := Module.End k[G] ρ.asModule)
    (⇑(algebraMap k (Module.End k[G] ρ.asModule)) : (a : k) → Module.End k[G] ρ.asModule)

Tactic:
have : Bijective (algebraMap k (Module.End k[G] ρ.asModule)) :=
    IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
this :
  Bijective.{u_2 + 1, u_3 + 1} (α := k) (β := Module.End k[G] ρ.asModule)
    (⇑(algebraMap k (Module.End k[G] ρ.asModule)) : (a : k) → Module.End k[G] ρ.asModule)
⊢ Bijective.{u_2 + 1, u_3 + 1} (α := k) (β := ρ.IntertwiningMap ρ)
    (⇑(algebraMap k (ρ.IntertwiningMap ρ)) : (a : k) → ρ.IntertwiningMap ρ)

Tactic:
(Bijective.of_comp_iff' (IntertwiningMap.equivAlgEnd (ρ := ρ)).bijective _).1 this

Premises used: Representation.IntertwiningMap.equivAlgEnd, Function.Bijective.of_comp_iff', Iff.mp, AlgEquiv.bijective
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
this :
  Bijective.{u_2 + 1, u_3 + 1} (α := k) (β := Module.End k[G] ρ.asModule)
    (⇑(algebraMap k (Module.End k[G] ρ.asModule)) : (a : k) → Module.End k[G] ρ.asModule)
⊢ Bijective.{u_2 + 1, u_3 + 1} (α := k) (β := ρ.IntertwiningMap ρ)
    (⇑(algebraMap k (ρ.IntertwiningMap ρ)) : (a : k) → ρ.IntertwiningMap ρ)

Tactic:
exact (Bijective.of_comp_iff' (IntertwiningMap.equivAlgEnd (ρ := ρ)).bijective _).1 this

Premises used: Representation.IntertwiningMap.equivAlgEnd, Function.Bijective.of_comp_iff', Iff.mp, AlgEquiv.bijective
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
rw : Module.finrank k k = 1
⊢ Module.finrank.{u_2, u_3} k (ρ.IntertwiningMap ρ) = 1

Tactic:
rw [LinearEquiv.finrank_eq (LinearEquiv.ofBijective (Algebra.linearMap k (IntertwiningMap ρ ρ))
      algebraMap_intertwiningMap_bijective_of_isAlgClosed).symm]

Premises used: LinearEquiv.symm, Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed, Algebra.linearMap, LinearEquiv.finrank_eq, Representation.IntertwiningMap, LinearEquiv.ofBijective
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
⊢ Module.finrank k k = 1

Tactic:
CommSemiring.finrank_self k

Premises used: CommSemiring.finrank_self
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
⊢ Module.finrank k k = 1

Tactic:
exact CommSemiring.finrank_self k

Premises used: CommSemiring.finrank_self
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
inst_7 : IsMulCommutative G
⊢ Module.finrank k V = 1

Tactic:
IsSimpleModule.finrank_eq_one_of_isMulCommutative k[G] ρ.asModule k

Premises used: Representation.instAddCommMonoidAsModule._aux_4, IsSimpleModule.finrank_eq_one_of_isMulCommutative, Representation.asModule, Representation.instAddCommMonoidAsModule._aux_1, MonoidAlgebra, Representation.instModuleAsModule._aux_1
-- Module: Mathlib.RepresentationTheory.Irreducible
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
inst_4 : ρ.IsIrreducible
inst_5 : FiniteDimensional k V
inst_6 : IsAlgClosed k
inst_7 : IsMulCommutative G
⊢ Module.finrank k V = 1

Tactic:
exact IsSimpleModule.finrank_eq_one_of_isMulCommutative k[G] ρ.asModule k

Premises used: IsSimpleModule.finrank_eq_one_of_isMulCommutative, Representation.asModule, MonoidAlgebra
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
g : G
v : W
⊢ (π.conjugate g : (a : W) → V) v =
    HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single g⁻¹ 1)
      ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v) : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
h : ∀ (v : V), (π : (a : W) → V) ((i : (a : V) → W) v : W) = v
g : G
v : V
rw :
  HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single g⁻¹ 1)
      ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (β := W) (MonoidAlgebra.single g 1) ((i : (a : V) → W) v : W)) : V) =
    v
rw₁ :
  HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single g⁻¹ 1)
      ((π : (a : W) → V) ((i : (a : V) → W) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v) : W) : V) =
    v
rw₂ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g⁻¹ 1) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v) = v
rw₃ : HMul.hMul (α := k[G]) (MonoidAlgebra.single g⁻¹ 1) (MonoidAlgebra.single g 1) • v = v
rw₄ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single (g⁻¹ * g) (HMul.hMul (α := k) 1 1)) v = v
rw₅ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single (g⁻¹ * g) 1) v = v
rw₆ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single 1 1) v = v
rw₇ : HSMul.hSMul (α := k[G]) 1 v = v
rw₈ rw₉ : v = v
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v

Tactic:
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, one_smul]

Premises used: inv_mul_cancel, MonoidAlgebra.single_mul_single, LinearMap.conjugate_apply, one_smul, LinearMap.map_smul, MonoidAlgebra.one_def, mul_one, SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
inst_10 : Fintype G
v : W
⊢ Eq.{u_3 + 1} (α := V) ((sumOfConjugates G π : (a : W) → V) v : V) (∑ g : G, (π.conjugate g : (a : W) → V) v : V)

Tactic:
LinearMap.sum_apply _ _ _

Premises used: LinearMap.sum_apply
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
g : G
v : W
simp :
  Eq.{u_3 + 1} (α := V)
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
        ((π : (a : W) → V)
            (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1)
              (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v)) :
          V))
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1)
        (HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
          ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1) v) : V)))
⊢ (sumOfConjugates G π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v) =
    HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single g 1) ((sumOfConjugates G π : (a : W) → V) v : V)

Tactic:
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]

Premises used: LinearMap.conjugate_apply, LinearMap.sumOfConjugates_apply, Finset.smul_sum
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
g : G
v : W
⊢ Eq.{u_3 + 1} (α := V)
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
        ((π : (a : W) → V)
            (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1)
              (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v)) :
          V))
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1)
        (HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
          ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1) v) : V)))

Tactic:
Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_

Premises used: HMul.hMul, Fintype.sum_bijective, Group.mulRight_bijective
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
g : G
v : W
refine :
  ∀ (i : G),
    HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single i⁻¹ 1)
        ((π : (a : W) → V)
            (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single i 1)
              (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v)) :
          V) =
      HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1)
        (HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single ((fun (x : G) ↦ x * g) i)⁻¹ 1)
          ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single ((fun (x : G) ↦ x * g) i) 1) v) : V))
⊢ Eq.{u_3 + 1} (α := V)
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
        ((π : (a : W) → V)
            (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1)
              (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v)) :
          V))
    (∑ x : G,
      HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1)
        (HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single x⁻¹ 1)
          ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single x 1) v) : V)))

Tactic:
refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_

Premises used: HMul.hMul, Fintype.sum_bijective, Group.mulRight_bijective
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i_1 : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
g : G
v : W
i : G
⊢ HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single i⁻¹ 1)
      ((π : (a : W) → V)
          (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single i 1) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v)) :
        V) =
    HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1)
      (HSMul.hSMul (α := k[G]) (β := V) (MonoidAlgebra.single ((fun (x : G) ↦ x * g) i)⁻¹ 1)
        ((π : (a : W) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single ((fun (x : G) ↦ x * g) i) 1) v) : V))

Tactic:
simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]

Premises used: smul_smul, MonoidAlgebra.single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
inst_10 : Fintype G
v : W
⊢ Eq.{u_3 + 1} (α := V) ((sumOfConjugatesEquivariant G π : (a : W) → V) v : V)
    (∑ g : G, (π.conjugate g : (a : W) → V) v : V)

Tactic:
π.sumOfConjugates_apply G v

Premises used: LinearMap.sumOfConjugates_apply
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
inst_10 : Fintype G
v : W
⊢ (equivariantProjection G π : (a : W) → V) v =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ g : G, (π.conjugate g : (a : W) → V) v)

Tactic:
simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply,
    Fintype.card_eq_nat_card]

Premises used: LinearMap.equivariantProjection, LinearMap.smul_apply, LinearMap.sumOfConjugatesEquivariant_apply, Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
hcard : IsUnit.{u_1} (M := k) (↑(Nat.card G) : k)
h : ∀ (v : V), (π : (a : W) → V) ((i : (a : V) → W) v : W) = v
v : V
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ
      (∑ g : G, (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W)) =
    v
⊢ (equivariantProjection G π : (a : W) → V) ((i : (a : V) → W) v : W) = v

Tactic:
rw [equivariantProjection_apply]

Premises used: LinearMap.equivariantProjection_apply
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
hcard : IsUnit.{u_1} (M := k) (↑(Nat.card G) : k)
h : ∀ (v : V), (π : (a : W) → V) ((i : (a : V) → W) v : W) = v
v : V
simp : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ
      (∑ g : G, (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W)) =
    v

Tactic:
simp only [conjugate_i π i h]

Premises used: LinearMap.conjugate_i
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : CommRing k
G : Type u_2
inst_1 : Group G
V : Type u_3
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k W
inst_8 : Module k[G] W
inst_9 : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : LinearMap (R := k[G]) (RingHom.id k[G]) V W
inst_10 : Fintype G
hcard : IsUnit.{u_1} (M := k) (↑(Nat.card G) : k)
h : ∀ (v : V), (π : (a : W) → V) ((i : (a : V) → W) v : W) = v
v : V
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Nat.card G) : k)⁻¹ʳ (Finset.card.{u_2} (α := G) Finset.univ • v) = v
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Nat.card G) : k)⁻¹ʳ (Fintype.card G • v) = v
rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Nat.card G) : k)⁻¹ʳ
      (HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Fintype.card G) : k) v) =
    v
rw₃ : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ʳ (↑(Fintype.card G) : k) • v = v
rw₄ : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ʳ (↑(Nat.card G) : k) • v = v
rw₅ : HSMul.hSMul.{u_1, u_3, u_3} (α := k) 1 v = v
rw₆ rw₇ : v = v
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v

Tactic:
rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul,
    Fintype.card_eq_nat_card, Ring.inverse_mul_cancel _ hcard, one_smul]

Premises used: Finset.card_univ, Ring.inverse_mul_cancel, smul_smul, one_smul, Nat.cast_smul_eq_nsmul, Fintype.card_eq_nat_card, Finset.sum_const
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this : Module k V := Module.compHom V (algebraMap k A)
⊢ IsScalarTower k A W

Tactic:
have := IsScalarTower.of_compHom k A W
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this : IsScalarTower k A W
⊢ IsScalarTower k A V

Tactic:
have := IsScalarTower.of_compHom k A V