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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N

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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N
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✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N ↔ s ⊆ ↑N
constructor
no goals
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N
exact Subset.trans subset_lieSpan
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N
intro hs m hm
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N
rw [mem_lieSpan] at hm
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
N✝ N' : LieSubmodule R L M
I J : LieIdeal R L
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N
exact hm _ hs