awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ (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)
have 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)))
Tactic: simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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)))
have 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))
Tactic: refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ (equivariantProjection G π : (a : W) → V) ((i : (a : V) → W) v : W) = v
have 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
Tactic: rw [equivariantProjection_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ 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
have simp : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
Tactic: simp only [conjugate_i π i h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Nat.card G) : k)⁻¹ʳ (Finset.card.{u_2} (α := G) Finset.univ • 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := k) (↑(Nat.card G) : k)⁻¹ʳ (Fintype.card 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have 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
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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw₃ : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ʳ (↑(Fintype.card G) : k) • 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw₄ : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ʳ (↑(Nat.card G) : k) • 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw₅ : HSMul.hSMul.{u_1, u_3, u_3} (α := k) 1 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) (↑(Nat.card G) : k)⁻¹ʳ (∑ x : G, v) = v
have rw₆ : 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (hypothesis)
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)
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
have this₁ : IsScalarTower k A W
Tactic: have := IsScalarTower.of_compHom k A W
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (hypothesis)
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
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
have this₁ : IsScalarTower k A V
Tactic: have := IsScalarTower.of_compHom k A V
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
⊢ ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
have h_inj : Eq (α := Submodule k V)
  (LinearMap.ker
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f))
  ⊥
Tactic: apply LinearMap.leftInverse_apply_of_inj
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (hypothesis)
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_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
have hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
Tactic: have hφ : ∀ (x : V), φ (f x) = x := by
    apply LinearMap.leftInverse_apply_of_inj
    simp [hf]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
have have : ∀ (x : Fintype G), ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
Tactic: have _ : Fintype G := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
x : Fintype G
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
have refine : ∀ (x_1 : V),
  Eq (α := V) ((LinearMap.equivariantProjection G φ ∘ₗ f : (a : V) → V) x_1 : V) ((LinearMap.id : (a : V) → V) x_1 : V)
Tactic: refine ⟨φ.equivariantProjection G, LinearMap.ext ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
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
p : Submodule k[G] V
⊢ ∃ (q : Submodule k[G] V), IsCompl p q
have rcases : ∀ (f : LinearMap (R := k[G]) (RingHom.id k[G]) V ↥p) (hf : f ∘ₗ p.subtype = LinearMap.id),
  ∃ (q : Submodule k[G] V), IsCompl p q
Tactic: rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Maschke (goal)
Goal:
k_1 : Type u_1
inst : Field k_1
G_1 : Type u_2
inst_1 : Finite G_1
inst_2 : NeZero.{u_1} (R := k_1) (↑(Nat.card G_1) : k_1)
inst_3 : Group G_1
V_1 : Type u_3
inst_4 : AddCommGroup V_1
inst_5 : Module k_1[G_1] V_1
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k_1[G_1] W
G : Type u_5
k : Type u_6
V : Type u_7
inst_8 : Group G
inst_9 : Field k
inst_10 : Finite G
inst_11 : NeZero.{u_6} (R := k) (↑(Nat.card G) : k)
inst_12 : AddCommGroup V
inst_13 : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation
have rw : IsSemisimpleModule k[G] ρ.asModule
Tactic: rw [isSemisimpleRepresentation_iff_isSemisimpleModule_asModule]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f₁ f₂ : A ⟶ B
g : B ⟶ C
⊢ (f₁ + f₂) ≫ g = f₁ ≫ g + f₂ ≫ g
have hf : Hom.hom ((f₁ + f₂) ≫ g) = Hom.hom (f₁ ≫ g + f₂ ≫ g)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g₁ g₂ : B ⟶ C
⊢ f ≫ (g₁ + g₂) = f ≫ g₁ + f ≫ g₂
have hf : Hom.hom (f ≫ (g₁ + g₂)) = Hom.hom (f ≫ g₁ + f ≫ g₂)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))
have empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (h : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))),
  Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, Hom.hom (f i))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]
Cleared hypotheses: s