case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
⊢ (∃ N, ↑N = p) → ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
⊢ (∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
⊢ (∃ N, ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
constructor
case mp.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x✝ : L
m✝ : M
⊢ m✝ ∈ ↑N → ⁅x✝, m✝⁆ ∈ ↑N
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
⊢ (∃ N, ↑N = p) → ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
rintro ⟨N, rfl⟩ _ _
no goals
case mp.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x✝ : L
m✝ : M
⊢ m✝ ∈ ↑N → ⁅x✝, m✝⁆ ∈ ↑N
exact N.lie_mem
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
h : ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
⊢ (∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p
intro h
no goals
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
p : Submodule R M
h : ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p
use { p with lie_mem := @h }