awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
this : Module.Finite.{u_3, u_2} k (Module.End A V)
⊢ 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)

Tactic:
exact IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

Premises used: IsAlgClosed.algebraMap_bijective_of_isIntegral
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
this : Module.Finite.{u_3, u_2} k (Module.End A V)
⊢ 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)

Tactic:
classical exact IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

Premises used: IsAlgClosed.algebraMap_bijective_of_isIntegral
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
⊢ Nontrivial V

Tactic:
have : Nontrivial V := IsSimpleModule.nontrivial A V
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
obtain : ∀ (v : V) (v_nz : v ≠ 0), Module.finrank k V = 1
⊢ Module.finrank k V = 1

Tactic:
obtain ⟨v, v_nz⟩ := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
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)
⊢ 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)
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
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:
simpa only [← show _ = a • w from congr($ht w)] using (k ∙ v).smul_mem t hw

Premises used: congrArg, id, Submodule.span, Singleton.singleton, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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
inr : ∀ (hU : U = ⊤), Module.finrank k V = 1
⊢ Module.finrank k V = 1

Tactic:
obtain hU | hU := eq_bot_or_eq_top U

Premises used: IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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

Tactic:
(v_nz <| hU.le <| Submodule.mem_span_singleton_self v).elim

Premises used: False.elim, Eq.le, Submodule.mem_span_singleton_self
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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

Tactic:
exact (v_nz <| hU.le <| Submodule.mem_span_singleton_self v).elim

Premises used: False.elim, Eq.le, Submodule.mem_span_singleton_self
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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 = ⊤
inr : Eq (α := Submodule k V) (k ∙ v) ⊤
⊢ Module.finrank k V = 1

Tactic:
rw [finrank_eq_one_iff_of_nonzero v v_nz]

Premises used: finrank_eq_one_iff_of_nonzero
-- Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
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 = ⊤
inr inr₁ inr₂ inr₃ : ∀ (hU : ⊤ ≤ U), LE.le (α := Submodule k V) ⊤ (k ∙ v)
⊢ Eq (α := Submodule k V) (k ∙ v) ⊤

Tactic:
rwa [← top_le_iff] at hU ⊢

Premises used: top_le_iff
-- Module: Mathlib.RepresentationTheory.Basic
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
g : G
v : V
⊢ ((((trivial k G V : Representation k G V) : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
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
inst_4 : ρ.IsTrivial
g : G
⊢ Eq.{u_3 + 1} (α := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) (LinearMap.id : V →ₗ[k] V)

Tactic:
IsTrivial.out g

Premises used: Representation.IsTrivial.out
-- Module: Mathlib.RepresentationTheory.Basic
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
inst_4 : ρ.IsTrivial
g : G
x : V
⊢ (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x

Tactic:
congr($(isTrivial_def ρ g) x)

Premises used: congrArg, id, Representation.isTrivial_def, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
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
g : G
x : 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) =
    x

Tactic:
simp [← Module.End.mul_apply, ← map_mul]

Premises used: map_mul, Module.End.mul_apply
-- Module: Mathlib.RepresentationTheory.Basic
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
g : G
x : 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) =
    x

Tactic:
simp [← Module.End.mul_apply, ← map_mul]

Premises used: map_mul, Module.End.mul_apply
-- Module: Mathlib.RepresentationTheory.Basic
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
g : G
⊢ Function.Bijective.{u_3 + 1, u_3 + 1} (α := V) (β := V) (⇑((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)

Tactic:
Equiv.bijective ⟨ρ g, ρ g⁻¹, inv_self_apply ρ g, self_inv_apply ρ g⟩

Premises used: Equiv.bijective, Equiv.mk, Inv.inv, Representation.self_inv_apply, Representation.inv_self_apply, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
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
⊢ ρ.asAlgebraHom = (lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ

Tactic:
rfl

Premises used: Representation.asAlgebraHom, rfl
-- Module: Mathlib.RepresentationTheory.Basic
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
r : k
⊢ (ρ.asAlgebraHom : (a : k[G]) → End k V) (MonoidAlgebra.single g r) =
    HSMul.hSMul (β := V →ₗ[k] V) r ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V)

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_single]

Premises used: Representation.asAlgebraHom_def, MonoidAlgebra.lift_single
-- Module: Mathlib.RepresentationTheory.Basic
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
⊢ Eq.{u_3 + 1} (α := End k V) ((ρ.asAlgebraHom : (a : k[G]) → End k V) (MonoidAlgebra.single g 1) : End k V)
    ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
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
⊢ Eq.{u_3 + 1} (α := End k V) ((ρ.asAlgebraHom : (a : k[G]) → End k V) ((of k G : (a : G) → k[G]) g) : End k V)
    ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V)

Tactic:
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul]

Premises used: Representation.asAlgebraHom_single, one_smul, MonoidAlgebra.of_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
inst : CommSemiring k_1
inst_1 : Monoid G_1
inst_2 : AddCommMonoid V_1
inst_3 : Module k_1 V_1
ρ_1 : Representation k_1 G_1 V_1
k : Type u_4
G : Type u_5
V : Type u_6
inst_4 : Semiring k
inst_5 : Monoid G
inst_6 : AddCommMonoid V
inst_7 : Module k V
inst_8 : Module.Finite k V
ρ : Representation k G V
⊢ Module.Finite.{u_4, u_6} k ρ.asModule

Tactic:
.equiv ρ.asModuleEquiv.symm

Premises used: LinearEquiv.symm, Representation.asModuleEquiv, Module.Finite.equiv
-- Module: Mathlib.RepresentationTheory.Basic
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[G]
x : ρ.asModule
⊢ Eq (α := V) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) (r • x) : V)
    ((((ρ.asAlgebraHom : (a : k[G]) → End k V) r : End k V) : (a : V) → V)
        ((ρ.asModuleEquiv : (a : ρ.asModule) → V) x : V) :
      V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
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
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))
⊢ (ρ.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)

Tactic:
rw [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.RepresentationTheory.Basic
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
⊢ 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:
simp
-- Module: Mathlib.RepresentationTheory.Basic
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
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)
⊢ (ρ.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)

Tactic:
rw [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.RepresentationTheory.Basic
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
⊢ 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:
simp
-- Module: Mathlib.RepresentationTheory.Basic
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
g : 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]) g) :
            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]) g : k[G])
          ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)

Tactic:
simp only [one_smul, MonoidAlgebra.lift_symm_apply, MonoidAlgebra.of_apply,
      Representation.asAlgebraHom_single, Representation.ofModule,
      RestrictScalars.lsmul_apply_apply]

Premises used: Representation.asAlgebraHom_single, MonoidAlgebra.lift_symm_apply, one_smul, Representation.ofModule, RestrictScalars.lsmul_apply_apply, MonoidAlgebra.of_apply
-- Module: Mathlib.RepresentationTheory.Basic
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
f g : k[G]
fw :
  Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) f :
            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) f ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)
gw :
  Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) g :
            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) 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)) (f + g) :
            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) (f + g)
          ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)

Tactic:
simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]

Premises used: LinearMap.add_apply, map_add, add_smul
-- Module: Mathlib.RepresentationTheory.Basic
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_1 : k[G]
m : RestrictScalars k k[G] M
r : k
f : k[G]
w :
  Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) f :
            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) f ((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 • f) :
            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 • f)
          ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)

Tactic:
simp only [w, map_smul, LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul]

Premises used: LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul, map_smul
-- Module: Mathlib.RepresentationTheory.Basic
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
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)
⊢ 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)

Tactic:
dsimp [ofModule, RestrictScalars.lsmul_apply_apply]

Premises used: Representation.ofModule, RestrictScalars.lsmul_apply_apply
-- Module: Mathlib.RepresentationTheory.Basic
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)
    ((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:
simp