awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (hypothesis)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := k) (β := Module.End A V)
    (⇑(algebraMap k (Module.End A V)) : (a : k) → Module.End A V)
have this : Module.Finite.{u_3, u_2} k (Module.End A V)
Tactic: have : Module.Finite k (Module.End A V) := .of_injective (LinearMap.restrictScalarsₗ k A V V k) <|
    LinearMap.restrictScalars_injective _
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (hypothesis)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
⊢ Module.finrank k V = 1
have this : Nontrivial V
Tactic: have : Nontrivial V := IsSimpleModule.nontrivial A V
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
⊢ Module.finrank k V = 1
have obtain : ∀ (v : V) (v_nz : v ≠ 0), Module.finrank k V = 1
Tactic: obtain ⟨v, v_nz⟩ := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
a : A
w : V
hw :
  Membership.mem (γ := Set V)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (k ∙ v)))) w
⊢ Membership.mem (γ := Set V)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (k ∙ v)))) (a • w)
have have : ∀ (t : k)
  (ht :
    Eq.{u_2 + 1} (α := Module.End A V) ((algebraMap k (Module.End A V) : (a : k) → Module.End A V) t : Module.End A V)
      ((Module.toModuleEnd A V : (a : A) → Module.End A V) a : Module.End A V)),
  Membership.mem (γ := Set V)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (k ∙ v)))) (a • w)
Tactic: have ⟨t, ht⟩ := (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k).2
        (Module.toModuleEnd A V a)
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src : Submodule k V := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
⊢ Module.finrank k V = 1
have inl : ∀ (hU : U = ⊥), Module.finrank k V = 1
Tactic: obtain hU | hU := eq_bot_or_eq_top U
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src : Submodule k V := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
inl : ∀ (hU : U = ⊥), Module.finrank k V = 1
⊢ Module.finrank k V = 1
have inr : ∀ (hU : U = ⊤), Module.finrank k V = 1
Tactic: obtain hU | hU := eq_bot_or_eq_top U
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src : Submodule k V := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
hU : U = ⊤
⊢ Module.finrank k V = 1
have inr : Eq (α := Submodule k V) (k ∙ v) ⊤
Tactic: rw [finrank_eq_one_iff_of_nonzero v v_nz]
-- Lean 4 proof step from Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (goal)
Goal:
A : Type u_1
V : Type u_2
k : Type u_3
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : Module A V
inst_6 : IsScalarTower k A V
inst_7 : IsSimpleModule A V
inst_8 : FiniteDimensional k V
inst_9 : IsAlgClosed k
inst_10 : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src : Submodule k V := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
hU : U = ⊤
⊢ Eq (α := Submodule k V) (k ∙ v) ⊤
have inr : ∀ (hU : ⊤ ≤ U), LE.le (α := Submodule k V) ⊤ (k ∙ v)
Tactic: rwa [← top_le_iff] at hU ⊢
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
r : k
x : V
⊢ (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) (r • x) =
    HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((algebraMap k k[G] : (a : k) → k[G]) r : k[G])
      ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)
have rw : r • x =
  (ρ.asModuleEquiv : (a : ρ.asModule) → V)
    (HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((algebraMap k k[G] : (a : k) → k[G]) r : k[G])
      ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule))
Tactic: rw [LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) =
    HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((of k G : (a : G) → k[G]) g : k[G])
      ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)
have rw : Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)
  ((ρ.asModuleEquiv : (a : ρ.asModule) → V)
      (HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((of k G : (a : G) → k[G]) g : k[G])
        ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)) :
    V)
Tactic: rw [LinearEquiv.symm_apply_eq]
-- 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
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
            End k (RestrictScalars k k[G] M)) :
          (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
        m :
      RestrictScalars k k[G] M)
    ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
        (HSMul.hSMul (β := M) r ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)
have hM : ∀ (m_1 : G),
  Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) ((of k G : (a : G) → k[G]) m_1) :
            End k (RestrictScalars k k[G] M)) :
          (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
        m :
      RestrictScalars k k[G] M)
    ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
        (HSMul.hSMul (α := k[G]) (β := M) ((of k G : (a : G) → k[G]) m_1 : k[G])
          ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)
Tactic: apply MonoidAlgebra.induction_on r
-- 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
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
hM :
  ∀ (m_1 : G),
    Eq (α := RestrictScalars k k[G] M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) ((of k G : (a : G) → k[G]) m_1) :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          m :
        RestrictScalars k k[G] M)
      ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
          (HSMul.hSMul (α := k[G]) (β := M) ((of k G : (a : G) → k[G]) m_1 : k[G])
            ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
        RestrictScalars k k[G] M)
⊢ Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
            End k (RestrictScalars k k[G] M)) :
          (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
        m :
      RestrictScalars k k[G] M)
    ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
        (HSMul.hSMul (β := M) r ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)
have hadd : ∀ (x y : k[G]),
  Eq (α := RestrictScalars k k[G] M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) x :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          m :
        RestrictScalars k k[G] M)
      ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
          (HSMul.hSMul (β := M) x ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
        RestrictScalars k k[G] M) →
    Eq (α := RestrictScalars k k[G] M)
        ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) y :
                End k (RestrictScalars k k[G] M)) :
              (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
            m :
          RestrictScalars k k[G] M)
        ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
            (HSMul.hSMul (β := M) y ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
          RestrictScalars k k[G] M) →
      Eq (α := RestrictScalars k k[G] M)
        ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) (x + y) :
                End k (RestrictScalars k k[G] M)) :
              (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
            m :
          RestrictScalars k k[G] M)
        ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
            (HSMul.hSMul (β := M) (x + y)
              ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
          RestrictScalars k k[G] M)
Tactic: apply MonoidAlgebra.induction_on r
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
g : G
x : RestrictScalars k k[G] ρ.asModule
⊢ Eq (α := RestrictScalars k k[G] ρ.asModule)
    ((((ofModule ρ.asModule : (a : G) → RestrictScalars k k[G] ρ.asModule →ₗ[k] RestrictScalars k k[G] ρ.asModule) g :
            RestrictScalars k k[G] ρ.asModule →ₗ[k] RestrictScalars k k[G] ρ.asModule) :
          (a : RestrictScalars k k[G] ρ.asModule) → RestrictScalars k k[G] ρ.asModule)
        x :
      RestrictScalars k k[G] ρ.asModule)
    ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] ρ.asModule) : (a : ρ.asModule) → RestrictScalars k k[G] ρ.asModule)
        ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule)
            ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
                ((ρ.asModuleEquiv : (a : ρ.asModule) → V)
                    ((RestrictScalars.addEquiv k k[G] ρ.asModule : (a : RestrictScalars k k[G] ρ.asModule) → ρ.asModule)
                        x :
                      ρ.asModule) :
                  V) :
              V) :
          ρ.asModule) :
      RestrictScalars k k[G] ρ.asModule)
have dsimp : Eq (α := RestrictScalars k k[G] ρ.asModule)
  ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] ρ.asModule) : (a : ρ.asModule) → RestrictScalars k k[G] ρ.asModule)
      (HSMul.hSMul (α := k[G]) (β := ρ.asModule) (MonoidAlgebra.single g 1)
        ((RestrictScalars.addEquiv k k[G] ρ.asModule : (a : RestrictScalars k k[G] ρ.asModule) → ρ.asModule) x :
          ρ.asModule)) :
    RestrictScalars k k[G] ρ.asModule)
  ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] ρ.asModule) : (a : ρ.asModule) → RestrictScalars k k[G] ρ.asModule)
      ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
              ((ρ.asModuleEquiv : (a : ρ.asModule) → V)
                  ((RestrictScalars.addEquiv k k[G] ρ.asModule : (a : RestrictScalars k k[G] ρ.asModule) → ρ.asModule)
                      x :
                    ρ.asModule) :
                V) :
            V) :
        ρ.asModule) :
    RestrictScalars k k[G] ρ.asModule)
Tactic: dsimp [ofModule, RestrictScalars.lsmul_apply_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
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : asModule.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
⊢ (RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
      ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) (r • m) :
        RestrictScalars k k[G] M) =
    HSMul.hSMul (β := M) r
      ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        M)
have dsimp : (RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
            End k (RestrictScalars k k[G] M)) :
          (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
        ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
          RestrictScalars k k[G] M) :
      RestrictScalars k k[G] M) =
  HSMul.hSMul (β := M) r
    ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
        ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
          RestrictScalars k k[G] M) :
      M)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
t : k
g : G
v : ρ.asModule
⊢ HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v =
    HSMul.hSMul (β := V) t
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) v : V) : V)
have rw : HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v =
  (ρ.asModuleEquiv : (a : ρ.asModule) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v)
Tactic: rw [← LinearMap.smul_apply, ← asAlgebraHom_single, ← asModuleEquiv_map_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
t : k
x : k[G]
v : ρ.asModule
⊢ (t • x) • v = t • x • v
have revert : ∀ (t : k), (t • x) • v = t • x • v
Tactic: revert t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (t : k), (t • x) • v = t • x • v
have hM : ∀ (m : G) (t : k),
  HSMul.hSMul (β := k[G]) t ((of k G : (a : G) → k[G]) m : k[G]) • v =
    t • HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) m : k[G]) v
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
hM :
  ∀ (m : G) (t : k),
    HSMul.hSMul (β := k[G]) t ((of k G : (a : G) → k[G]) m : k[G]) • v =
      t • HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) m : k[G]) v
⊢ ∀ (t : k), (t • x) • v = t • x • v
have hadd : ∀ (x y : k[G]),
  (∀ (t : k), (t • x) • v = t • x • v) →
    (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
hM :
  ∀ (m : G) (t : k),
    HSMul.hSMul (β := k[G]) t ((of k G : (a : G) → k[G]) m : k[G]) • v =
      t • HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) m : k[G]) v
hadd :
  ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v
⊢ ∀ (t : k), (t • x) • v = t • x • v
have hsmul : ∀ (r : k) (x : k[G]), (∀ (t : k), (t • x) • v = t • x • v) → ∀ (t : k), (t • r • x) • v = t • (r • x) • v
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ (t • s • y) • v = t • (s • y) • v
have hsmul : t • s • y • v = t • (s • y) • v
Tactic: rw [← smul_assoc, smul_eq_mul, hy (t * s), ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
⊢ ρ.norm ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = ρ.norm
have h : ∀ (x : V), Eq (α := V) ((ρ.norm ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
⊢ (ρ : (a : G) → V →ₗ[k] V) g ∘ₗ ρ.norm = ρ.norm
have h : ∀ (x : V), Eq (α := V) (((ρ : (a : G) → V →ₗ[k] V) g ∘ₗ ρ.norm : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
⊢ restrict ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ = 1
have h : ∀ (x : ↥W),
  Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) 1) sorry : (a : ↥W) → ↥W) x) : V)
    (↑((1 : (a : ↥W) → ↥W) x) : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
⊢ restrict ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ =
    restrict ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * restrict ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯
have h : ∀ (x_2 : ↥W),
  Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) sorry : (a : ↥W) → ↥W) x_2) : V)
    (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) x) sorry * restrict ((ρ : (a : G) → V →ₗ[k] V) x_1) sorry : (a : ↥W) → ↥W) x_2) : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
⊢ W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ = 1
have h : ∀ (x : V),
  Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) 1) sorry ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)
    ((1 ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
⊢ W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ =
    W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯
have h : ∀ (x_2 : V),
  Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) sorry ∘ₗ W.mkQ : (a : V) → V ⧸ W) x_2 : V ⧸ W)
    (((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x) sorry * W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x_1) sorry) ∘ₗ W.mkQ :
          (a : V) → V ⧸ W)
        x_2 :
      V ⧸ W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : Eq (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S)
⊢ Eq.{u_3 + 1} (α := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V)
have h₁ : ∀ (x : V),
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)
    ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : Eq (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S)
x : V
⊢ Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)
    ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V)
have h₁ : Eq (α := V)
  ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
    V)
  ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
      ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V) :
    V)
Tactic: apply (ρ.apply_bijective g⁻¹).1