feat(algebra/lie/cartan_subalgebra): add lemma `lie_subalgebra.exists…

…_nested_lie_ideal_of_le_normalizer` (#11820)

src/algebra/lie/cartan_subalgebra.lean

@@ -48,10 +48,22 @@ forall_congr (λ y, forall_congr (λ hy, by rw [← lie_skew, H.neg_mem_iff]))
 lemma le_normalizer : H ≤ H.normalizer :=
 λ x hx, show ∀ (y : L), y ∈ H → ⁅x,y⁆ ∈ H, from λ y, H.lie_mem hx
 
+variables {H}
+
 /-- A Lie subalgebra is an ideal of its normalizer. -/
-lemma ideal_in_normalizer : ∀ (x y : L), x ∈ H.normalizer → y ∈ H → ⁅x,y⁆ ∈ H :=
+lemma ideal_in_normalizer : ∀ {x y : L}, x ∈ H.normalizer → y ∈ H → ⁅x,y⁆ ∈ H :=
 λ x y h, h y
 
+/-- A Lie subalgebra `H` is an ideal of any Lie subalgebra `K` containing `H` and contained in the
+normalizer of `H`. -/
+lemma exists_nested_lie_ideal_of_le_normalizer
+  {K : lie_subalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) :
+  ∃ (I : lie_ideal R K), (I : lie_subalgebra R K) = of_le h₁ :=
+begin
+  rw exists_nested_lie_ideal_coe_eq_iff,
+  exact λ x y hx hy, ideal_in_normalizer (h₂ hx) hy,
+end
+
 /-- The normalizer of a Lie subalgebra `H` is the maximal Lie subalgebra in which `H` is a Lie
 ideal. -/
 lemma le_normalizer_of_ideal {N : lie_subalgebra R L}
@@ -78,6 +90,8 @@ begin
     simpa using h y hy, },
 end
 
+variables (H)
+
 /-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra. -/
 class is_cartan_subalgebra : Prop :=
 (nilpotent        : lie_algebra.is_nilpotent R H)