R : Type u
L : Type v
M : Type w
N : 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 N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
⊢ ∀ (x : M), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → x = 0
R : Type u
L : Type v
M : Type w
N : 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 N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
⊢ ⁅I, maxTrivSubmodule R L M⁆ = ⊥
rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.lieIdeal_oper_eq_linear_span,
  LieSubmodule.bot_coeSubmodule, Submodule.span_eq_bot]
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
N : 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 N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := m, property := hm }⁆ = 0
R : Type u
L : Type v
M : Type w
N : 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 N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
⊢ ∀ (x : M), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → x = 0
rintro m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩
no goals
case intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
N : 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 N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : m ∈ maxTrivSubmodule R L M
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := m, property := hm }⁆ = 0
exact hm x