awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
simp :
  ∀ (g : G),
    ∀ x₁ ∈ ρ₁.toSubmodule,
      ∀ x₂ ∈ ρ₂.toSubmodule,
        HAdd.hAdd (α := W) (β := W) ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₁ : W)
            ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₂ : W) ∈
          ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
⊢ ∀ (g : G) ⦃v : W⦄,
    v ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule →
      Membership.mem (α := W) (ρ₁.toSubmodule ⊔ ρ₂.toSubmodule)
        ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)

Tactic:
simp only [Submodule.forall_mem_sup, map_add]

Premises used: map_add, Submodule.forall_mem_sup
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
hx₂ : x₂ ∈ ρ₂.toSubmodule
⊢ HAdd.hAdd (α := W) (β := W) ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₁ : W)
      ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₂ : W) ∈
    ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
Submodule.mem_sup.mpr
        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩

Premises used: Iff.mpr, Subrepresentation.apply_mem_toSubmodule, And.intro, Exists.intro, Submodule.mem_sup, DFunLike.coe, rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
hx₂ : x₂ ∈ ρ₂.toSubmodule
⊢ HAdd.hAdd (α := W) (β := W) ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₁ : W)
      ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₂ : W) ∈
    ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
exact Submodule.mem_sup.mpr
        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩

Premises used: Iff.mpr, Subrepresentation.apply_mem_toSubmodule, And.intro, Exists.intro, Submodule.mem_sup, DFunLike.coe, rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
simp :
  ∀ (g : G) ⦃v : W⦄,
    v ∈ ρ₁.toSubmodule →
      v ∈ ρ₂.toSubmodule →
        Membership.mem (α := W) ρ₁.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W) ∧
          Membership.mem (α := W) ρ₂.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)
⊢ ∀ (g : G) ⦃v : W⦄,
    v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule →
      Membership.mem (α := W) (ρ₁.toSubmodule ⊓ ρ₂.toSubmodule)
        ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)

Tactic:
simp only [Submodule.mem_inf, and_imp]

Premises used: and_imp, Submodule.mem_inf
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x : W
hx₁ : x ∈ ρ₁.toSubmodule
hx₂ : x ∈ ρ₂.toSubmodule
⊢ Membership.mem (α := W) ρ₁.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x : W) ∧
    Membership.mem (α := W) ρ₂.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x : W)

Tactic:
⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩

Premises used: Subrepresentation.apply_mem_toSubmodule, And.intro
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x : W
hx₁ : x ∈ ρ₁.toSubmodule
hx₂ : x ∈ ρ₂.toSubmodule
⊢ Membership.mem (α := W) ρ₁.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x : W) ∧
    Membership.mem (α := W) ρ₂.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x : W)

Tactic:
exact ⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
ρ₁ ρ₂ : Subrepresentation ρ
⊢ (↑(ρ₁ ⊔ ρ₂) : Set W) = (↑ρ₁ : Set W) + (↑ρ₂ : Set W)

Tactic:
Submodule.coe_sup ρ₁.toSubmodule ρ₂.toSubmodule

Premises used: Submodule.coe_sup, Subrepresentation.toSubmodule
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
ρ₁ ρ₂ : Subrepresentation ρ
⊢ (↑(ρ₁ ⊓ ρ₂) : Set W) = (↑ρ₁ : Set W) ∩ (↑ρ₂ : Set W)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
ρ₁ ρ₂ : Subrepresentation ρ
⊢ (ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
ρ₁ ρ₂ : Subrepresentation ρ
⊢ (ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
⊢ ∀ (g : G) ⦃v : W⦄,
    Membership.mem (γ := Submodule A W) ⊤ v →
      Membership.mem (α := W) (γ := Submodule A W) ⊤ ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
⊢ ∀ (g : G) ⦃v : W⦄,
    Membership.mem (γ := Submodule A W) ⊥ v →
      Membership.mem (α := W) (γ := Submodule A W) ⊥ ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
⊢ HSMul.hSMul (α := A[G]) 0 v ∈ σ.toSubmodule.carrier

Tactic:
simp [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
add : x • v + y • v ∈ σ.toSubmodule.carrier
⊢ (x + y) • v ∈ σ.toSubmodule.carrier

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ x • v + y • v ∈ σ.toSubmodule.carrier

Tactic:
σ.toSubmodule.add_mem' hx hy

Premises used: Submodule.toAddSubmonoid, Set.Mem, Subrepresentation.toSubmodule, AddSubmonoid.toAddSubsemigroup, Representation.asModule, AddSubsemigroup.add_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ x • v + y • v ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.add_mem' hx hy

Premises used: Submodule.toAddSubmonoid, Subrepresentation.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
g : G
a : A
single :
  HSMul.hSMul (β := W) a
      ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) v : W) : W) ∈
    σ.toSubmodule.carrier
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v ∈ σ.toSubmodule.carrier

Tactic:
rw [Representation.single_smul]

Premises used: Representation.single_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (β := W) a
      ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) v : W) : W) ∈
    σ.toSubmodule.carrier

Tactic:
σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)

Premises used: Submodule.smul_mem', Set.Mem, Subrepresentation.toSubmodule, Subrepresentation.apply_mem_toSubmodule
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (β := W) a
      ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) v : W) : W) ∈
    σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)

Premises used: Submodule.smul_mem', Subrepresentation.toSubmodule, Subrepresentation.apply_mem_toSubmodule
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
c : A[G]
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 v ∈ σ.toSubmodule.carrier
add :
  ∀ (x y : A[G]) (hx : x • v ∈ σ.toSubmodule.carrier) (hy : y • v ∈ σ.toSubmodule.carrier),
    (x + y) • v ∈ σ.toSubmodule.carrier
single : ∀ (g : G) (a : A), HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v ∈ σ.toSubmodule.carrier
⊢ c • v ∈ σ.toSubmodule.carrier

Tactic:
induction c using MonoidAlgebra.induction_linear with
    | zero => simp [zero_smul]
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [Representation.single_smul]
      exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)

Premises used: Representation.single_smul, zero_smul, add_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
σ : Subrepresentation ρ
v : W
⊢ v ∈ σ.asSubmodule ↔ v ∈ σ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
zero : 0 ∈ σ.toSubmodule.carrier
⊢ HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 ∈ σ.toSubmodule.carrier

Tactic:
σ.toSubmodule.zero_mem'

Premises used: Submodule.toAddSubmonoid, Set.Mem, Subrepresentation.toSubmodule, AddSubmonoid.zero_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.zero_mem'

Premises used: Submodule.toAddSubmonoid, Subrepresentation.toSubmodule, AddSubmonoid.zero_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
add : x • m + y • m ∈ σ.toSubmodule.carrier
⊢ (x + y) • m ∈ σ.toSubmodule.carrier

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • m ∈ σ.toSubmodule.carrier

Tactic:
σ.toSubmodule.add_mem' hx hy

Premises used: Submodule.toAddSubmonoid, Set.Mem, Subrepresentation.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • m ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.add_mem' hx hy

Premises used: Submodule.toAddSubmonoid, Subrepresentation.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
single :
  HSMul.hSMul (α := A[G]) ((algebraMap A A[G] : (a : A) → A[G]) a : A[G])
      (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) m) ∈
    σ.toSubmodule.carrier
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) m ∈ σ.toSubmodule.carrier

Tactic:
rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]

Premises used: MonoidAlgebra.smul_single, Algebra.smul_def, smul_eq_mul, mul_one, SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) m ∈ σ.toSubmodule.carrier

Tactic:
simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm

Premises used: Subrepresentation.apply_mem_toSubmodule, Representation.ofModule, RestrictScalars.lsmul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (α := A[G]) ((algebraMap A A[G] : (a : A) → A[G]) a : A[G])
      (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) m) ∈
    σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm

Premises used: Algebra.algebraMap, Submodule.smul_mem', Subrepresentation.toSubmodule, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
c : A[G]
m : M
hm : m ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier
add :
  ∀ (x y : A[G]) (hx : x • m ∈ σ.toSubmodule.carrier) (hy : y • m ∈ σ.toSubmodule.carrier),
    (x + y) • m ∈ σ.toSubmodule.carrier
single : ∀ (g : G) (a : A), HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) m ∈ σ.toSubmodule.carrier
⊢ c • m ∈ σ.toSubmodule.carrier

Tactic:
induction c using MonoidAlgebra.induction_linear with
    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm

Premises used: Submodule.toAddSubmonoid, Subrepresentation.toSubmodule, MonoidAlgebra.smul_single, zero_smul, add_smul, AddSubmonoid.zero_mem', Algebra.smul_def, smul_eq_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid M
inst_3 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
⊢ m ∈ σ.asSubmodule' ↔ m ∈ σ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] M
g : G
v : RestrictScalars A A[G] M
hv :
  Membership.mem (γ := Submodule A (RestrictScalars A A[G] M)) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } v
⊢ Membership.mem (α := RestrictScalars A A[G] M) (γ := Submodule A (RestrictScalars A A[G] M))
    { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
    ((((Representation.ofModule M : (a : G) → RestrictScalars A A[G] M →ₗ[A] RestrictScalars A A[G] M) g :
            RestrictScalars A A[G] M →ₗ[A] RestrictScalars A A[G] M) :
          (a : RestrictScalars A A[G] M) → RestrictScalars A A[G] M)
        v :
      RestrictScalars A A[G] M)

Tactic:
simpa [Representation.ofModule, RestrictScalars.lsmul] using
      Submodule.smul_of_tower_mem N (MonoidAlgebra.single g 1) hv

Premises used: Representation.ofModule, RestrictScalars.lsmul, OfNat.ofNat, Submodule.smul_of_tower_mem, MonoidAlgebra.single
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid M
inst_3 : Module A[G] M
N : Submodule A[G] M
m : M
⊢ m ∈ ofSubmodule N ↔ m ∈ N

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
a : A
w : W
hw : w ∈ N.carrier
⊢ a • w ∈ N.carrier

Tactic:
simpa using (N.smul_mem (algebraMap A A[G] a) hw)

Premises used: Algebra.algebraMap, MonoidAlgebra, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) w ∈ N

Tactic:
have h : (MonoidAlgebra.single g (1 : A)) • w ∈ N :=
      Submodule.smul_of_tower_mem N _ hw
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) w ∈ N
⊢ Membership.mem (α := W) N
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) w : W) : W)

Tactic:
rw [Representation.single_smul, one_smul] at h

Premises used: Representation.single_smul, one_smul