-- Mathlib/Algebra/Lie/Normalizer.lean
theorem normalizer_eq_self_iff :
    H.normalizer = H ↔ (LieModule.maxTrivSubmodule R H <| L ⧸ H.toLieSubmodule) = ⊥

Proof state:
case mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅⟨z, hz⟩, y⁆ = 0

Tactic:
rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
  Submodule.coe_mk, mem_toLieSubmodule]

Result:
case mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

Tactic:
refine ⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩

Result:
case refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
⊢ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H

Proof state:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
intro y hy

Result:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Proof state:
case mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Tactic:
exact (H.mem_normalizer_iff' x).mp hx z hz

Result:
no goals

Proof state:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩

Result:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, (LieSubmodule.Quotient.mk' H.toLieSubmodule) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H

Proof state:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
hy : y ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ x ∈ H

Tactic:
simpa [y] using h y hy

Result:
no goals

Proof state:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ x ∈ H

Tactic:
rw [← h, H.mem_normalizer_iff']

Result:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Proof state:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
⊢ x ∈ H

Tactic:
let y := LieSubmodule.Quotient.mk' H.toLieSubmodule x

Result:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
⊢ x ∈ H

Proof state:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x = 0

Tactic:
suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
  coe_toLieSubmodule, mem_toSubmodule]

Result:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ x ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x = 0

Tactic:
rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
coe_toLieSubmodule, mem_toSubmodule]

Result:
no goals

Proof state:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, (LieSubmodule.Quotient.mk' H.toLieSubmodule) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H

Tactic:
rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
⊢ y ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)

Tactic:
rintro ⟨z, hz⟩

Result:
case mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅⟨z, hz⟩, y⁆ = 0