def LieSubmodule.ofUEASubmodule {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : Submodule (UniversalEnvelopingAlgebra R L) M) : LieSubmodule R L M

theorem LieSubmodule.mem_ofUEASubmodule {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : Submodule (UniversalEnvelopingAlgebra R L) M) (m : M) : m ∈ ofUEASubmodule hcompat N ↔ m ∈ N

theorem isSimpleOrder_submodule_of_isIrreducible {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) [hirr : LieModule.IsIrreducible R L M] : IsSimpleOrder (Submodule (UniversalEnvelopingAlgebra R L) M)

theorem LieModule.isSimpleModule_of_isIrreducible {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) [hirr : IsIrreducible R L M] : IsSimpleModule (UniversalEnvelopingAlgebra R L) M