case h
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ LieSubalgebra.normalizer (↑R L I) ↔ x ∈ ⊤
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ LieSubalgebra.normalizer (↑R L I) = ⊤
ext x
no goals
case h
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ LieSubalgebra.normalizer (↑R L I) ↔ x ∈ ⊤
simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true_iff] using
  fun y hy => I.lie_mem hy