no goals
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
⊢ LieSubmodule.normalizer (toLieSubmodule H) = toLieSubmodule H
rw [← LieSubmodule.coe_toSubmodule_eq_iff, coe_normalizer_eq_normalizer,
  IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]