-- Mathlib/Algebra/Lie/EngelSubalgebra.lean
/-- A Lie-subalgebra of an Artinian Lie algebra is self-normalizing
if it contains an Engel subalgebra.
See `LieSubalgebra.normalizer_engel` for a proof that Engel subalgebras are self-normalizing,
avoiding the Artinian condition. -/
lemma normalizer_eq_self_of_engel_le [IsArtinian R L]
    (H : LieSubalgebra R L) (x : L) (h : engel R x ≤ H) :
    normalizer H = H

Proof state:
case intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
⊢ LinearMap.ker (dx ^ (k + 1)) ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]

Result:
case intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
⊢ Submodule.map N.subtype (LinearMap.ker (dx ^ (k + 1))) ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Proof state:
case intro.a.h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ ∃ n, ((ad R L) x ^ n) (N.subtype y) = 0

Tactic:
use k+1

Result:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Tactic:
rwa [← lie_skew, neg_mem_iff (G := L)]

Result:
no goals

Proof state:
case intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
⊢ LinearMap.range (dx ^ (k + 1)) ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]

Result:
case intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
⊢ Submodule.map N.subtype (LinearMap.range (dx ^ (k + 1))) ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Proof state:
case intro.a.h.intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
⊢ N.subtype ((dx ^ k) y) ∈ N

Tactic:
simp only [Submodule.coe_subtype, SetLike.coe_mem]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
⊢ H.normalizer = H

Tactic:
set N := normalizer H

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
⊢ N = H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ∀ y ∈ H, ⁅n, y⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Tactic:
specialize hn x (h (self_mem_engel R x))

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Proof state:
case intro.a.h.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
⊢ N.subtype (dx ((dx ^ k) y)) ∈ H

Tactic:
apply aux₁

Result:
case intro.a.h.intro.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
⊢ N.subtype ((dx ^ k) y) ∈ N

Proof state:
case intro.a.h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ y ∈ Submodule.comap N.subtype (engel R x).toSubmodule

Tactic:
simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]

Result:
case intro.a.h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ ∃ n, ((ad R L) x ^ n) (N.subtype y) = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
⊢ N = H

Tactic:
apply le_antisymm _ (le_normalizer H)

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
⊢ H.normalizer ≤ H