R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
⊢ ⁅I, N⁆ ≤ ⁅J, N'⁆
intro m h
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆
rw [lieIdeal_oper_eq_span, mem_lieSpan] at h
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1
⊢ ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆
rw [lieIdeal_oper_eq_span, mem_lieSpan]
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
⊢ m ∈ N
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1
⊢ ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
intro N hN
case a
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
⊢ m ∈ N
apply h
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ m' ∈ ↑N
case a
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
rintro m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈ ↑N
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ m' ∈ ↑N
rw [← hm]
case a.intro.mk.intro.mk.a
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈ ↑N
apply hN
no goals
case a.intro.mk.intro.mk.a
R : Type u
L : Type v
M : Type w
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
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
N₂ : LieSubmodule R L M₂
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ = m'
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩