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₂
x : { x // x ∈ I }
m : { x // x ∈ N }
⊢ ⁅↑x, ↑m⁆ ∈ lieSpan R L {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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₂
x : { x // x ∈ I }
m : { x // x ∈ N }
⊢ ⁅↑x, ↑m⁆ ∈ ⁅I, N⁆
rw [lieIdeal_oper_eq_span]
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₂
x : { x // x ∈ I }
m : { x // x ∈ N }
⊢ ⁅↑x, ↑m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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₂
x : { x // x ∈ I }
m : { x // x ∈ N }
⊢ ⁅↑x, ↑m⁆ ∈ lieSpan R L {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
apply subset_lieSpan
no goals
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₂
x : { x // x ∈ I }
m : { x // x ∈ N }
⊢ ⁅↑x, ↑m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
use x, m