-- 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 h.zero.mk
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 : ℕ
val✝ : L
property✝ : val✝ ∈ N
⊢ ⟨val✝, property✝⟩ ∈ LinearMap.ker (dx ^ 0) → ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 0

Tactic:
intro hy

Result:
case h.zero.mk
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 : ℕ
val✝ : L
property✝ : val✝ ∈ N
hy : ⟨val✝, property✝⟩ ∈ LinearMap.ker (dx ^ 0)
⊢ ((ad R L) x ^ 0) (N.subtype ⟨val✝, property✝⟩) = 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 ∈ N, ⁅x, n⁆ ∈ H

Tactic:
intro n hn

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 ∈ N
⊢ ⁅x, n⁆ ∈ H

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)))
⊢ LinearMap.ker (dx ^ (k + 1)) ≤ Submodule.comap N.subtype (engel R x).toSubmodule

Tactic:
intro y hy

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))
⊢ y ∈ Submodule.comap N.subtype (engel R x).toSubmodule

Proof state:
case 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 : ∀ b ≥ k, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b))
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Tactic:
specialize hk (k+1) (Nat.le_add_right k 1)

Result:
case 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)))
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

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
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Tactic:
have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)

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
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Proof state:
case h.succ
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✝ k : ℕ
y : ↥N
ih : ∀ ⦃y : ↥N⦄, (dx ^ k) y = 0 → ((ad R L) x ^ k) (N.subtype y) = 0
⊢ (dx ^ k) (dx y) = 0 → ((ad R L) x ^ k) (((ad R L) x) (N.subtype y)) = 0

Tactic:
apply ih

Result:
no goals

Proof state:
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

Tactic:
clear hk

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 : ℕ
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Proof state:
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 : ℕ
y : ↥N
hy : y ∈ LinearMap.ker (dx ^ (k + 1))
⊢ ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

Tactic:
revert hy

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 : ℕ
y : ↥N
⊢ y ∈ LinearMap.ker (dx ^ (k + 1)) → ((ad R L) x ^ (k + 1)) (N.subtype y) = 0

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)))
⊢ Submodule.map N.subtype (LinearMap.range (dx ^ (k + 1))) ≤ H.toSubmodule

Tactic:
rw [Submodule.map_le_iff_le_comap]

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)))
⊢ LinearMap.range (dx ^ (k + 1)) ≤ Submodule.comap N.subtype H.toSubmodule