R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
⊢ normalizer H = H ↔
    ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
⊢ normalizer H = H ↔ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) = ⊥
rw [LieSubmodule.eq_bot_iff]
case refine'_1
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
⊢ ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0

case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
⊢ normalizer H ≤ H
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
⊢ normalizer H = H ↔
    ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
refine' ⟨fun h => _, fun h => le_antisymm _ H.le_normalizer⟩
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ Quot.mk Setoid.r x = 0
case refine'_1
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
⊢ ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
rintro ⟨x⟩ hx
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ Quot.mk Setoid.r x = 0
suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
  coe_toLieSubmodule, mem_coe_submodule]
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ ∀ (y : L), y ∈ H → ⁅y, x⁆ ∈ H
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
rw [← h, H.mem_normalizer_iff']
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ ∀ (y : L), y ∈ H → ⁅y, x⁆ ∈ H
intro y hy
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x y : L
hy : y ∈ H
hx : ⁅{ val := y, property := hy }, ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
no goals
case refine'_1.mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x y : L
hy : y ∈ H
hx : ⁅{ val := y, property := hy }, ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H
rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx
no goals
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : normalizer H = H
m✝ : L ⧸ toLieSubmodule H
x : L
hx : Quot.mk Setoid.r x ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
this : x ∈ H
⊢ Quot.mk Setoid.r x = 0
rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
coe_toLieSubmodule, mem_coe_submodule]
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
⊢ x ∈ H
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
⊢ normalizer H ≤ H
intro x hx
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
⊢ x ∈ H
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
⊢ x ∈ H
let y := LieSubmodule.Quotient.mk' H.toLieSubmodule x
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
hy : y ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
⊢ x ∈ H
have hy : y ∈ LieModule.maxTrivSubmodule R H (L ⧸ H.toLieSubmodule) := by
  rintro ⟨z, hz⟩
  rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
    Submodule.coe_mk, mem_toLieSubmodule]
  exact (H.mem_normalizer_iff' x).mp hx z hz
no goals
case refine'_2
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
hy : y ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
⊢ x ∈ H
simpa using h y hy
case mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅{ val := z, property := hz }, y⁆ = 0
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
⊢ y ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H)
rintro ⟨z, hz⟩
case mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H
case mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅{ val := z, property := hz }, y⁆ = 0
rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
  Submodule.coe_mk, mem_toLieSubmodule]
no goals
case mk
R : Type u_2
L : Type u_1
M : Type ?u.62528
M' : Type ?u.62531
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 : LieSubalgebra R L
h : ∀ (m : L ⧸ toLieSubmodule H), m ∈ LieModule.maxTrivSubmodule R { x // x ∈ H } (L ⧸ toLieSubmodule H) → m = 0
x : L
hx : x ∈ normalizer H
y : (fun x => L ⧸ toLieSubmodule H) x := ↑(LieSubmodule.Quotient.mk' (toLieSubmodule H)) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H
exact (H.mem_normalizer_iff' x).mp hx z hz