awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (hypothesis)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A_1 : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
A B : Rep.{w, u, v} k G
f : A ⟶ B
x : ↥A.ρ.invariants
g : G
c : (↑A : Type w)
hc : c ∈ A.ρ.invariants
⊢ Eq (α := (↑B : Type w))
    ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
          (a : (↑B : Type w)) → (↑B : Type w))
        (((↑(Hom.hom f) :
                  [inst_3 : FunLike (A.ρ.IntertwiningMap B.ρ) (↑A : Type w) (↑B : Type w)] →
                    [SemilinearMapClass (A.ρ.IntertwiningMap B.ρ) (RingHom.id k) (↑A : Type w) (↑B : Type w)] →
                      (↑A : Type w) →ₗ[k] (↑B : Type w)) ∘ₗ
                A.ρ.invariants.subtype :
              (a : ↥A.ρ.invariants) → (↑B : Type w))
            (Subtype.mk (p := fun (x : (↑A : Type w)) ↦ x ∈ A.ρ.invariants) c hc) :
          (↑B : Type w)) :
      (↑B : Type w))
    (((↑(Hom.hom f) :
              [inst_3 : FunLike (A.ρ.IntertwiningMap B.ρ) (↑A : Type w) (↑B : Type w)] →
                [SemilinearMapClass (A.ρ.IntertwiningMap B.ρ) (RingHom.id k) (↑A : Type w) (↑B : Type w)] →
                  (↑A : Type w) →ₗ[k] (↑B : Type w)) ∘ₗ
            A.ρ.invariants.subtype :
          (a : ↥A.ρ.invariants) → (↑B : Type w))
        (Subtype.mk (p := fun (x : (↑A : Type w)) ↦ x ∈ A.ρ.invariants) c hc) :
      (↑B : Type w))
have this : Eq (α := (↑B : Type w))
  ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
        (a : (↑B : Type w)) → (↑B : Type w))
      ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w)) c : (↑B : Type w)) :
    (↑B : Type w))
  ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w))
      ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          c :
        (↑A : Type w)) :
    (↑B : Type w))
Tactic: have := (hom_comm_apply f g c).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S_1 : Subgroup G
inst_2 : S_1.Normal
S : Subgroup G
inst_3 : S.Normal
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g_1 : G ⧸ S
g : G
⊢ Eq (α := ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
    (ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (invariantsFunctor k ↥S) (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
        ((X.ρ.quotientToInvariants S :
              Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp X.ρ S.subtype))) :
            (a : G ⧸ S) →
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp X.ρ S.subtype)))
          (↑g : G ⧸ S) :
      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
    (((Y.ρ.quotientToInvariants S : Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : G ⧸ S) →
              ↥(invariants (MonoidHom.comp Y.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          (↑g : G ⧸ S) ∘ₗ
        ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (invariantsFunctor k ↥S) (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
have h : ∀ (x : ↥(invariants (MonoidHom.comp X.ρ S.subtype))),
  Eq.{w + 1} (α := (↑Y : Type w))
    (↑(((ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
                ((X.ρ.quotientToInvariants S :
                      Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp X.ρ S.subtype))) :
                    (a : G ⧸ S) →
                      ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp X.ρ S.subtype)))
                  (↑g : G ⧸ S) :
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          x) :
      (↑Y : Type w))
    (↑(((((Y.ρ.quotientToInvariants S :
                      Representation.{u, v, w} k (G ⧸ S) ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
                    (a : G ⧸ S) →
                      ↥(invariants (MonoidHom.comp Y.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
                  (↑g : G ⧸ S) ∘ₗ
                ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (invariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
              ↥(invariants (MonoidHom.comp X.ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp Y.ρ S.subtype))) :
            (a : ↥(invariants (MonoidHom.comp X.ρ S.subtype))) → ↥(invariants (MonoidHom.comp Y.ρ S.subtype)))
          x) :
      (↑Y : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
X : Rep.{u_1, u, v} k G
g : G
⊢ X.ρ.invariants.subtype ∘ₗ
      (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
          (a : G) → (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
        g =
    (X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype
have h : ∀ (x : (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1)),
  Eq (α := (↑X : Type u_1))
    ((X.ρ.invariants.subtype ∘ₗ
            (Representation.trivial k G (↑(Functor.obj (invariantsFunctor k G) X) : Type u_1) :
                (a : G) →
                  (↑((invariantsFunctor k G).obj X) : Type u_1) →ₗ[k] (↑((invariantsFunctor k G).obj X) : Type u_1))
              g :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))
    (((X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g ∘ₗ X.ρ.invariants.subtype :
          (a : (↑((invariantsFunctor k G).obj X) : Type u_1)) → (↑X : Type u_1))
        x :
      (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
X : ModuleCat.{u_1, u} k
Y : Rep.{u_1, u, v} k G
f : Functor.obj (trivialFunctor k G) X ⟶ Y
c : (↑(Functor.obj (trivialFunctor k G) X) : Type u_1)
⊢ Membership.mem (α := (↑Y : Type u_1)) Y.ρ.invariants
    (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c : (↑Y : Type u_1))
have _ : ∀ (g : G),
  Eq (α := (↑Y : Type u_1))
    ((((Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) g : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
          (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
        (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c :
          (↑Y : Type u_1)) :
      (↑Y : Type u_1))
    (((Hom.hom f).toLinearMap : (a : (↑((trivialFunctor k G).obj X) : Type u_1)) → (↑Y : Type u_1)) c : (↑Y : Type u_1))
Tactic: _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (goal)
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
⊢ ρ.IsIrreducible ↔ IsSimpleModule k[G] ρ.asModule
have rw : ρ.IsIrreducible ↔ IsSimpleOrder.{u_3} (Submodule k[G] ρ.asModule)
Tactic: rw [isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (goal)
Goal:
G : Type u_1
k : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_5
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ IsSimpleModule k[G] M ↔ IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)
have rw : IsSimpleOrder.{u_5} (Submodule k[G] M) ↔
  IsIrreducible.{u_1, u_2, u_5} (G := G) (k := k) (V := RestrictScalars k k[G] M) (ofModule M)
Tactic: rw [isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
⊢ Injective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨ f = 0
have rw : Injective.{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: rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (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
f : ρ.IntertwiningMap σ
inst_6 : ρ.IsIrreducible
inst_7 : σ.IsIrreducible
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W) ∨ f = 0
have 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)
Tactic: rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (hypothesis)
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) (β := ρ.IntertwiningMap ρ)
    (⇑(algebraMap k (ρ.IntertwiningMap ρ)) : (a : k) → ρ.IntertwiningMap ρ)
have 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)
Tactic: have : Bijective (algebraMap k (Module.End k[G] ρ.asModule)) :=
    IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k
-- Lean 4 proof step from Mathlib.RepresentationTheory.Irreducible (goal)
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.{u_2, u_3} k (ρ.IntertwiningMap ρ) = 1
have rw : Module.finrank k k = 1
Tactic: rw [LinearEquiv.finrank_eq (LinearEquiv.ofBijective (Algebra.linearMap k (IntertwiningMap ρ ρ))
      algebraMap_intertwiningMap_bijective_of_isAlgClosed).symm]
-- 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
h : ∀ (v : V), (π : (a : W) → V) ((i : (a : V) → W) v : W) = v
g : G
v : V
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have 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
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have 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
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₂ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g⁻¹ 1) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g 1) v) = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₃ : HMul.hMul (α := k[G]) (MonoidAlgebra.single g⁻¹ 1) (MonoidAlgebra.single g 1) • v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₄ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single (g⁻¹ * g) (HMul.hMul (α := k) 1 1)) v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₅ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single (g⁻¹ * g) 1) v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₆ : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single 1 1) v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₇ : HSMul.hSMul (α := k[G]) 1 v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, 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
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
⊢ (π.conjugate g : (a : W) → V) ((i : (a : V) → W) v : W) = v
have rw₈ : v = v
Tactic: rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, one_smul]