R : Type u_1
L : Type u_2
M : Type ?u.59016
M' : Type ?u.59019
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'
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ normalizer H
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
R : Type u_1
L : Type u_2
M : Type ?u.59016
M' : Type ?u.59019
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'
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ normalizer H
⊢ ∃ I, ↑R { x // x ∈ K } I = ofLe h₁
rw [exists_nested_lieIdeal_coe_eq_iff]
no goals
R : Type u_1
L : Type u_2
M : Type ?u.59016
M' : Type ?u.59019
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'
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ normalizer H
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
exact fun x y hx hy => ideal_in_normalizer (h₂ hx) hy