[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
y : L
⊢ ∃ t z, z ∈ I ∧ y = t • x + z
[PROOFSTEP]
have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
y : L
hy : y ∈ ⊤
⊢ ∃ t z, z ∈ I ∧ y = t • x + z
[PROOFSTEP]
simp only [← hxI, Submodule.mem_sup, Submodule.mem_span_singleton] at hy
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
y : L
hy : ∃ y_1, (∃ a, a • x = y_1) ∧ ∃ z, z ∈ (↑R L I).toSubmodule ∧ y_1 + z = y
⊢ ∃ t z, z ∈ I ∧ y = t • x + z
[PROOFSTEP]
obtain ⟨-, ⟨t, rfl⟩, z, hz, rfl⟩ := hy
[GOAL]
case intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
t : R
z : L
hz : z ∈ (↑R L I).toSubmodule
⊢ ∃ t_1 z_1, z_1 ∈ I ∧ t • x + z = t_1 • x + z_1
[PROOFSTEP]
exact ⟨t, z, hz, rfl⟩
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ ↑⁅⊤, N⁆ = Submodule.map (↑(toEndomorphism R L M) x) ↑N ⊔ ↑⁅I, N⁆
[PROOFSTEP]
simp only [lieIdeal_oper_eq_linear_span', Submodule.sup_span, mem_top, exists_prop, true_and, Submodule.map_coe,
  toEndomorphism_apply_apply]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ Submodule.span R {m | ∃ x n, n ∈ N ∧ ⁅x, n⁆ = m} =
    Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m})
[PROOFSTEP]
refine' le_antisymm (Submodule.span_le.mpr _) (Submodule.span_mono fun z hz => _)
[GOAL]
case refine'_1
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ {m | ∃ x n, n ∈ N ∧ ⁅x, n⁆ = m} ⊆
    ↑(Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m}))
[PROOFSTEP]
rintro z ⟨y, n, hn : n ∈ N, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
y : L
n : M
hn : n ∈ N
⊢ ⁅y, n⁆ ∈ ↑(Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m}))
[PROOFSTEP]
obtain ⟨t, z, hz, rfl⟩ := exists_smul_add_of_span_sup_eq_top hxI y
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ ⁅t • x + z, n⁆ ∈ ↑(Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m}))
[PROOFSTEP]
simp only [SetLike.mem_coe, Submodule.span_union, Submodule.mem_sup]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ ∃ y,
    y ∈ Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N) ∧
      ∃ z_1, z_1 ∈ Submodule.span R {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m} ∧ y + z_1 = ⁅t • x + z, n⁆
[PROOFSTEP]
exact
  ⟨t • ⁅x, n⁆, Submodule.subset_span ⟨t • n, N.smul_mem' t hn, lie_smul t x n⟩, ⁅z, n⁆,
    Submodule.subset_span ⟨z, hz, n, hn, rfl⟩, by simp⟩
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ t • ⁅x, n⁆ + ⁅z, n⁆ = ⁅t • x + z, n⁆
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
z : M
hz : z ∈ (fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ N ∧ ⁅x, n⁆ = m}
⊢ z ∈ {m | ∃ x n, n ∈ N ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
[GOAL]
case refine'_2.inl.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
m : M
hm : m ∈ ↑↑N
⊢ (fun a => ⁅x, a⁆) m ∈ {m | ∃ x n, n ∈ N ∧ ⁅x, n⁆ = m}
case refine'_2.inr.intro.intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
N : LieSubmodule R L M
y : L
m : M
hm : m ∈ N
⊢ ⁅y, m⁆ ∈ {m | ∃ x n, n ∈ N ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
exacts [⟨x, m, hm, rfl⟩, ⟨y, m, hm, rfl⟩]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
⊢ lowerCentralSeries R L M (i + n) ≤ LieIdeal.lcs I M (j + 1)
[PROOFSTEP]
suffices
  ∀ l,
    ((⊤ : LieIdeal R L).lcs M (i + l) : Submodule R M) ≤
      (I.lcs M j : Submodule R M).map (toEndomorphism R L M x ^ l) ⊔ (I.lcs M (j + 1) : Submodule R M)
  by simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using this n
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
this :
  ∀ (l : ℕ),
    ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
      Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ lowerCentralSeries R L M (i + n) ≤ LieIdeal.lcs I M (j + 1)
[PROOFSTEP]
simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using this n
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
⊢ ∀ (l : ℕ),
    ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
      Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
[PROOFSTEP]
intro l
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
⊢ ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
[PROOFSTEP]
induction' l with l ih
[GOAL]
case zero
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
⊢ ↑(LieIdeal.lcs ⊤ M (i + Nat.zero)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ Nat.zero) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
[PROOFSTEP]
simp only [Nat.zero_eq, add_zero, LieIdeal.lcs_succ, pow_zero, LinearMap.one_eq_id, Submodule.map_id]
[GOAL]
case zero
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
⊢ ↑(LieIdeal.lcs ⊤ M i) ≤ ↑(LieIdeal.lcs I M j) ⊔ ↑⁅I, LieIdeal.lcs I M j⁆
[PROOFSTEP]
exact le_sup_of_le_left hIM
[GOAL]
case succ
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ ↑(LieIdeal.lcs ⊤ M (i + Nat.succ l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ Nat.succ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
[PROOFSTEP]
simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
[GOAL]
case succ
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ Submodule.map (↑(toEndomorphism R L M) x) ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
      Submodule.map (↑(toEndomorphism R L M) x ^ Nat.succ l) ↑(LieIdeal.lcs I M j) ⊔ ↑⁅I, LieIdeal.lcs I M j⁆ ∧
    ↑⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ ≤
      Submodule.map (↑(toEndomorphism R L M) x ^ Nat.succ l) ↑(LieIdeal.lcs I M j) ⊔ ↑⁅I, LieIdeal.lcs I M j⁆
[PROOFSTEP]
refine' ⟨(Submodule.map_mono ih).trans _, le_sup_of_le_right _⟩
[GOAL]
case succ.refine'_1
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ Submodule.map (↑(toEndomorphism R L M) x)
      (Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ Nat.succ l) ↑(LieIdeal.lcs I M j) ⊔ ↑⁅I, LieIdeal.lcs I M j⁆
[PROOFSTEP]
rw [Submodule.map_sup, ← Submodule.map_comp, ← LinearMap.mul_eq_comp, ← pow_succ, ← I.lcs_succ]
[GOAL]
case succ.refine'_1
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ Submodule.map (↑(toEndomorphism R L M) x ^ (l + 1)) ↑(LieIdeal.lcs I M j) ⊔
      Submodule.map (↑(toEndomorphism R L M) x) ↑(LieIdeal.lcs I M (j + 1)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ Nat.succ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
[PROOFSTEP]
exact sup_le_sup_left coe_map_toEndomorphism_le _
[GOAL]
case succ.refine'_2
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ ↑⁅I, LieIdeal.lcs ⊤ M (i + l)⁆ ≤ ↑⁅I, LieIdeal.lcs I M j⁆
[PROOFSTEP]
refine' le_trans (mono_lie_right _ _ I _) (mono_lie_right _ _ I hIM)
[GOAL]
case succ.refine'_2
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n i j : ℕ
hxn : ↑(toEndomorphism R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ LieIdeal.lcs I M j
l : ℕ
ih :
  ↑(LieIdeal.lcs ⊤ M (i + l)) ≤
    Submodule.map (↑(toEndomorphism R L M) x ^ l) ↑(LieIdeal.lcs I M j) ⊔ ↑(LieIdeal.lcs I M (j + 1))
⊢ LieIdeal.lcs ⊤ M (i + l) ≤ lowerCentralSeries R L M i
[PROOFSTEP]
exact antitone_lowerCentralSeries R L M le_self_add
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
hnp : _root_.IsNilpotent (↑(toEndomorphism R L M) x)
hIM : LieModule.IsNilpotent R { x // x ∈ ↑I } M
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
obtain ⟨n, hn⟩ := hnp
[GOAL]
case intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent R { x // x ∈ ↑I } M
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
obtain ⟨k, hk⟩ := hIM
[GOAL]
case intro.mk.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
have hk' : I.lcs M k = ⊥ := by simp only [← coe_toSubmodule_eq_iff, I.coe_lcs_eq, hk, bot_coeSubmodule]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
⊢ LieIdeal.lcs I M k = ⊥
[PROOFSTEP]
simp only [← coe_toSubmodule_eq_iff, I.coe_lcs_eq, hk, bot_coeSubmodule]
[GOAL]
case intro.mk.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
suffices ∀ l, lowerCentralSeries R L M (l * n) ≤ I.lcs M l
  by
  use k * n
  simpa [hk'] using this k
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ LieIdeal.lcs I M l
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
use k * n
[GOAL]
case h
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ LieIdeal.lcs I M l
⊢ lowerCentralSeries R L M (k * n) = ⊥
[PROOFSTEP]
simpa [hk'] using this k
[GOAL]
case intro.mk.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
⊢ ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ LieIdeal.lcs I M l
[PROOFSTEP]
intro l
[GOAL]
case intro.mk.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
l : ℕ
⊢ lowerCentralSeries R L M (l * n) ≤ LieIdeal.lcs I M l
[PROOFSTEP]
induction' l with l ih
[GOAL]
case intro.mk.intro.zero
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
⊢ lowerCentralSeries R L M (Nat.zero * n) ≤ LieIdeal.lcs I M Nat.zero
[PROOFSTEP]
simp
[GOAL]
case intro.mk.intro.succ
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (↑R L I).toSubmodule = ⊤
n : ℕ
hn : ↑(toEndomorphism R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R { x // x ∈ ↑I } M k = ⊥
hk' : LieIdeal.lcs I M k = ⊥
l : ℕ
ih : lowerCentralSeries R L M (l * n) ≤ LieIdeal.lcs I M l
⊢ lowerCentralSeries R L M (Nat.succ l * n) ≤ LieIdeal.lcs I M (Nat.succ l)
[PROOFSTEP]
exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : Subsingleton L
⊢ IsEngelian R L
[PROOFSTEP]
intro M _i1 _i2 _i3 _i4 _h
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
⊢ lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
suffices (⊤ : LieIdeal R L) = ⊥ by simp [this]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
this : ⊤ = ⊥
⊢ lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
simp [this]
[GOAL]
case h
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
⊢ ⊤ = ⊥
[PROOFSTEP]
haveI := (LieSubmodule.subsingleton_iff R L L).mpr inferInstance
[GOAL]
case h
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
this : Subsingleton (LieSubmodule R L L)
⊢ ⊤ = ⊥
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
⊢ LieAlgebra.IsEngelian R L₂
[PROOFSTEP]
intro M _i1 _i2 _i3 _i4 h'
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
letI : LieRingModule L M := LieRingModule.compLieHom M f
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this : LieRingModule L M := LieRingModule.compLieHom M f
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
letI : LieModule R L M := compLieHom M f
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
have hnp : ∀ x, IsNilpotent (toEndomorphism R L M x) := fun x => h' (f x)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
surj_id : Surjective ↑LinearMap.id
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
haveI : LieModule.IsNilpotent R L M := h M hnp
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
surj_id : Surjective ↑LinearMap.id
this : LieModule.IsNilpotent R L M
⊢ LieModule.IsNilpotent R L₂ M
[PROOFSTEP]
apply hf.lieModuleIsNilpotent surj_id
[GOAL]
case hfg
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
surj_id : Surjective ↑LinearMap.id
this : LieModule.IsNilpotent R L M
⊢ ∀ (x : L) (m : M), ⁅↑f x, ↑LinearMap.id m⁆ = ↑LinearMap.id ⁅x, m⁆
[PROOFSTEP]
intros
[GOAL]
case hfg
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
surj_id : Surjective ↑LinearMap.id
this : LieModule.IsNilpotent R L M
x✝ : L
m✝ : M
⊢ ⁅↑f x✝, ↑LinearMap.id m✝⁆ = ↑LinearMap.id ⁅x✝, m✝⁆
[PROOFSTEP]
simp only [LinearMap.id_coe, id_eq]
[GOAL]
case hfg
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
f : L →ₗ⁅R⁆ L₂
hf : Surjective ↑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent (↑(toEndomorphism R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent (↑(toEndomorphism R L M) x)
surj_id : Surjective ↑LinearMap.id
this : LieModule.IsNilpotent R L M
x✝ : L
m✝ : M
⊢ ⁅↑f x✝, m✝⁆ = ⁅x✝, m✝⁆
[PROOFSTEP]
rfl
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ := SetLike.exists_of_lt hK₂
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
let K' : LieSubalgebra R L :=
  { (R ∙ x) ⊔ (K : Submodule R L) with lie_mem' := fun {y z} => LieSubalgebra.lie_mem_sup_of_mem_normalizer hx₁ }
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
have hKK' : K ≤ K' := (LieSubalgebra.coe_submodule_le_coe_submodule K K').mp le_sup_right
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
have hK' : K' ≤ K.normalizer := by
  rw [← LieSubalgebra.coe_submodule_le_coe_submodule]
  exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ K' ≤ LieSubalgebra.normalizer K
[PROOFSTEP]
rw [← LieSubalgebra.coe_submodule_le_coe_submodule]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
⊢ K'.toSubmodule ≤ (LieSubalgebra.normalizer K).toSubmodule
[PROOFSTEP]
exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
⊢ ∃ K', IsEngelian R { x // x ∈ K' } ∧ K < K'
[PROOFSTEP]
refine' ⟨K', _, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
⊢ IsEngelian R { x // x ∈ K' }
[PROOFSTEP]
intro M _i1 _i2 _i3 _i4 h
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
⊢ LieModule.IsNilpotent R { x // x ∈ K' } M
[PROOFSTEP]
obtain ⟨I, hI₁ : (I : LieSubalgebra R K') = LieSubalgebra.ofLe hKK'⟩ :=
  LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer hKK' hK'
[GOAL]
case intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
⊢ LieModule.IsNilpotent R { x // x ∈ K' } M
[PROOFSTEP]
have hI₂ : (R ∙ (⟨x, hxK'⟩ : K')) ⊔ (LieSubmodule.toSubmodule I) = ⊤ :=
  by
  rw [← LieIdeal.coe_to_lieSubalgebra_to_submodule R K' I, hI₁]
  apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
  simp
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
⊢ Submodule.span R {{ val := x, property := hxK' }} ⊔ ↑I = ⊤
[PROOFSTEP]
rw [← LieIdeal.coe_to_lieSubalgebra_to_submodule R K' I, hI₁]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
⊢ Submodule.span R {{ val := x, property := hxK' }} ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤
[PROOFSTEP]
apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
[GOAL]
case a
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
⊢ Submodule.map (Submodule.subtype K'.toSubmodule)
      (Submodule.span R {{ val := x, property := hxK' }} ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) =
    Submodule.map (Submodule.subtype K'.toSubmodule) ⊤
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
hI₂ : Submodule.span R {{ val := x, property := hxK' }} ⊔ ↑I = ⊤
⊢ LieModule.IsNilpotent R { x // x ∈ K' } M
[PROOFSTEP]
have e : K ≃ₗ⁅R⁆ I :=
  (LieSubalgebra.equivOfLe hKK').trans (LieEquiv.ofEq _ _ ((LieSubalgebra.coe_set_eq _ _).mpr hI₁.symm))
[GOAL]
case intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
hI₂ : Submodule.span R {{ val := x, property := hxK' }} ⊔ ↑I = ⊤
e : { x // x ∈ K } ≃ₗ⁅R⁆ { x // x ∈ ↑I }
⊢ LieModule.IsNilpotent R { x // x ∈ K' } M
[PROOFSTEP]
have hI₃ : LieAlgebra.IsEngelian R I := e.isEngelian_iff.mp hK₁
[GOAL]
case intro.intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
inst✝¹ : LieRingModule L M✝
inst✝ : LieModule R L M✝
K : LieSubalgebra R L
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K < LieSubalgebra.normalizer K
x : L
hx₁ : x ∈ LieSubalgebra.normalizer K
hx₂ : ¬x ∈ K
K' : LieSubalgebra R L :=
  let src := Submodule.span R {x} ⊔ K.toSubmodule;
  {
    toSubmodule :=
      { toAddSubmonoid := src.toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : L}, x ∈ src.carrier → c • x ∈ src.carrier) },
    lie_mem' :=
      (_ :
        ∀ {y z : L},
          y ∈ Submodule.span R {x} ⊔ K.toSubmodule →
            z ∈ Submodule.span R {x} ⊔ K.toSubmodule → ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ K.toSubmodule) }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ LieSubalgebra.normalizer K
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule { x // x ∈ K' } M
_i4 : LieModule R { x // x ∈ K' } M
h : ∀ (x : { x // x ∈ K' }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K' } M) x)
I : LieIdeal R { x // x ∈ K' }
hI₁ : ↑R { x // x ∈ K' } I = LieSubalgebra.ofLe hKK'
hI₂ : Submodule.span R {{ val := x, property := hxK' }} ⊔ ↑I = ⊤
e : { x // x ∈ K } ≃ₗ⁅R⁆ { x // x ∈ ↑I }
hI₃ : IsEngelian R { x // x ∈ ↑I }
⊢ LieModule.IsNilpotent R { x // x ∈ K' } M
[PROOFSTEP]
exact LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNoetherian R L
⊢ IsEngelian R L
[PROOFSTEP]
intro M _i1 _i2 _i3 _i4 h
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
rw [← isNilpotent_range_toEndomorphism_iff]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
⊢ LieModule.IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M
[PROOFSTEP]
let L' := (toEndomorphism R L M).range
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
⊢ LieModule.IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M
[PROOFSTEP]
replace h : ∀ y : L', _root_.IsNilpotent (y : Module.End R M)
[GOAL]
case h
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
⊢ ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
[PROOFSTEP]
rintro ⟨-, ⟨y, rfl⟩⟩
[GOAL]
case h.mk.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
h : ∀ (x : L), _root_.IsNilpotent (↑(toEndomorphism R L M) x)
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
y : L
⊢ _root_.IsNilpotent
    ↑{ val := ↑↑(toEndomorphism R L M) y,
        property := (_ : ∃ y_1, ↑↑(toEndomorphism R L M) y_1 = ↑↑(toEndomorphism R L M) y) }
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
⊢ LieModule.IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M
[PROOFSTEP]
change LieModule.IsNilpotent R L' M
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
⊢ LieModule.IsNilpotent R { x // x ∈ L' } M
[PROOFSTEP]
let s := {K : LieSubalgebra R L' | LieAlgebra.IsEngelian R K}
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
⊢ LieModule.IsNilpotent R { x // x ∈ L' } M
[PROOFSTEP]
have hs : s.Nonempty := ⟨⊥, LieAlgebra.isEngelian_of_subsingleton⟩
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
⊢ LieModule.IsNilpotent R { x // x ∈ L' } M
[PROOFSTEP]
suffices ⊤ ∈ s by
  rw [← isNilpotent_of_top_iff]
  apply this M
  simp [LieSubalgebra.toEndomorphism_eq, h]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent R { x // x ∈ L' } M
[PROOFSTEP]
rw [← isNilpotent_of_top_iff]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent R { x // x ∈ ⊤ } M
[PROOFSTEP]
apply this M
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ⊤ ∈ s
⊢ ∀ (x : { x // x ∈ ⊤ }), _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ ⊤ } M) x)
[PROOFSTEP]
simp [LieSubalgebra.toEndomorphism_eq, h]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
⊢ ⊤ ∈ s
[PROOFSTEP]
have : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K' :=
  by
  rintro K (hK₁ : LieAlgebra.IsEngelian R K) hK₂
  apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
  apply lt_of_le_of_ne K.le_normalizer
  rw [Ne.def, eq_comm, K.normalizer_eq_self_iff, ← Ne.def, ← LieSubmodule.nontrivial_iff_ne_bot R K]
  have : Nontrivial (L' ⧸ K.toLieSubmodule) :=
    by
    replace hK₂ : K.toLieSubmodule ≠ ⊤ := by
      rwa [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, K.coe_toLieSubmodule, LieSubmodule.top_coeSubmodule, ←
        LieSubalgebra.top_coe_submodule, K.coe_to_submodule_eq_iff]
    exact Submodule.Quotient.nontrivial_of_lt_top _ hK₂.lt_top
  have : LieModule.IsNilpotent R K (L' ⧸ K.toLieSubmodule) := by
    -- Porting note: was refine' hK₁ _ fun x => _
    apply hK₁
    intro x
    have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
    apply Module.End.IsNilpotent.mapQ ?_ hx
    intro X HX
    simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_coe_submodule] at HX
    simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply, LieSubalgebra.mem_coe_submodule]
    exact LieSubalgebra.lie_mem K x.prop HX
  exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
⊢ ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
[PROOFSTEP]
rintro K (hK₁ : LieAlgebra.IsEngelian R K) hK₂
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ ∃ K', K' ∈ s ∧ K < K'
[PROOFSTEP]
apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ K < LieSubalgebra.normalizer K
[PROOFSTEP]
apply lt_of_le_of_ne K.le_normalizer
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ K ≠ LieSubalgebra.normalizer K
[PROOFSTEP]
rw [Ne.def, eq_comm, K.normalizer_eq_self_iff, ← Ne.def, ← LieSubmodule.nontrivial_iff_ne_bot R K]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ Nontrivial { x // x ∈ ↑(maxTrivSubmodule R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) }
[PROOFSTEP]
have : Nontrivial (L' ⧸ K.toLieSubmodule) :=
  by
  replace hK₂ : K.toLieSubmodule ≠ ⊤ := by
    rwa [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, K.coe_toLieSubmodule, LieSubmodule.top_coeSubmodule, ←
      LieSubalgebra.top_coe_submodule, K.coe_to_submodule_eq_iff]
  exact Submodule.Quotient.nontrivial_of_lt_top _ hK₂.lt_top
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
replace hK₂ : K.toLieSubmodule ≠ ⊤ := by
  rwa [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, K.coe_toLieSubmodule, LieSubmodule.top_coeSubmodule, ←
    LieSubalgebra.top_coe_submodule, K.coe_to_submodule_eq_iff]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
⊢ LieSubalgebra.toLieSubmodule K ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, K.coe_toLieSubmodule, LieSubmodule.top_coeSubmodule, ←
  LieSubalgebra.top_coe_submodule, K.coe_to_submodule_eq_iff]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : LieSubalgebra.toLieSubmodule K ≠ ⊤
⊢ Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
exact Submodule.Quotient.nontrivial_of_lt_top _ hK₂.lt_top
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
⊢ Nontrivial { x // x ∈ ↑(maxTrivSubmodule R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) }
[PROOFSTEP]
have : LieModule.IsNilpotent R K (L' ⧸ K.toLieSubmodule) := by
  -- Porting note: was refine' hK₁ _ fun x => _
  apply hK₁
  intro x
  have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
  apply Module.End.IsNilpotent.mapQ ?_ hx
  intro X HX
  simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_coe_submodule] at HX
  simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply, LieSubalgebra.mem_coe_submodule]
  exact LieSubalgebra.lie_mem K x.prop HX
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
⊢ LieModule.IsNilpotent R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
apply hK₁
[GOAL]
case x
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
⊢ ∀ (x : { x // x ∈ K }),
    _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) x)
[PROOFSTEP]
intro x
[GOAL]
case x
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
⊢ _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) x)
[PROOFSTEP]
have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
[GOAL]
case x
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
hx : _root_.IsNilpotent (↑(ad R { x // x ∈ L' }) ↑x)
⊢ _root_.IsNilpotent (↑(toEndomorphism R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) x)
[PROOFSTEP]
apply Module.End.IsNilpotent.mapQ ?_ hx
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
hx : _root_.IsNilpotent (↑(ad R { x // x ∈ L' }) ↑x)
⊢ ↑(LieSubalgebra.toLieSubmodule K) ≤ Submodule.comap (↑(ad R { x // x ∈ L' }) ↑x) ↑(LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
intro X HX
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
hx : _root_.IsNilpotent (↑(ad R { x // x ∈ L' }) ↑x)
X : { x // x ∈ L' }
HX : X ∈ ↑(LieSubalgebra.toLieSubmodule K)
⊢ X ∈ Submodule.comap (↑(ad R { x // x ∈ L' }) ↑x) ↑(LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_coe_submodule] at HX
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
hx : _root_.IsNilpotent (↑(ad R { x // x ∈ L' }) ↑x)
X : { x // x ∈ L' }
HX : X ∈ K
⊢ X ∈ Submodule.comap (↑(ad R { x // x ∈ L' }) ↑x) ↑(LieSubalgebra.toLieSubmodule K)
[PROOFSTEP]
simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply, LieSubalgebra.mem_coe_submodule]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
x : { x // x ∈ K }
hx : _root_.IsNilpotent (↑(ad R { x // x ∈ L' }) ↑x)
X : { x // x ∈ L' }
HX : X ∈ K
⊢ ⁅↑x, X⁆ ∈ K
[PROOFSTEP]
exact LieSubalgebra.lie_mem K x.prop HX
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : IsEngelian R { x // x ∈ K }
hK₂ : K ≠ ⊤
this✝ : Nontrivial ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
this : LieModule.IsNilpotent R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)
⊢ Nontrivial { x // x ∈ ↑(maxTrivSubmodule R { x // x ∈ K } ({ x // x ∈ L' } ⧸ LieSubalgebra.toLieSubmodule K)) }
[PROOFSTEP]
exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
⊢ ⊤ ∈ s
[PROOFSTEP]
haveI _i5 : IsNoetherian R L' := by
  -- Porting note: was
      -- isNoetherian_of_surjective L _ (LinearMap.range_rangeRestrict (toEndomorphism R L M))
      -- abusing the relation between `LieHom.rangeRestrict` and `LinearMap.rangeRestrict`
  refine isNoetherian_of_surjective L (LieHom.rangeRestrict (toEndomorphism R L M)) ?_
  simp only [LieHom.range_coeSubmodule, LieHom.coe_toLinearMap, LinearMap.range_eq_top]
  exact LieHom.surjective_rangeRestrict (toEndomorphism R L M)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
⊢ IsNoetherian R { x // x ∈ L' }
[PROOFSTEP]
refine isNoetherian_of_surjective L (LieHom.rangeRestrict (toEndomorphism R L M)) ?_
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
⊢ LinearMap.range ↑(LieHom.rangeRestrict (toEndomorphism R L M)) = ⊤
[PROOFSTEP]
simp only [LieHom.range_coeSubmodule, LieHom.coe_toLinearMap, LinearMap.range_eq_top]
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
⊢ Function.Surjective ↑(LieHom.rangeRestrict (toEndomorphism R L M))
[PROOFSTEP]
exact LieHom.surjective_rangeRestrict (toEndomorphism R L M)
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
⊢ ⊤ ∈ s
[PROOFSTEP]
obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFounded_of_noetherian R L').has_min s hs
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : K ∈ s
hK₂ : ∀ (x : LieSubalgebra R { x // x ∈ L' }), x ∈ s → ¬x > K
⊢ ⊤ ∈ s
[PROOFSTEP]
have hK₃ : K = ⊤ := by
  by_contra contra
  obtain ⟨K', hK'₁, hK'₂⟩ := this K hK₁ contra
  exact hK₂ K' hK'₁ hK'₂
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : K ∈ s
hK₂ : ∀ (x : LieSubalgebra R { x // x ∈ L' }), x ∈ s → ¬x > K
⊢ K = ⊤
[PROOFSTEP]
by_contra contra
[GOAL]
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : K ∈ s
hK₂ : ∀ (x : LieSubalgebra R { x // x ∈ L' }), x ∈ s → ¬x > K
contra : ¬K = ⊤
⊢ False
[PROOFSTEP]
obtain ⟨K', hK'₁, hK'₂⟩ := this K hK₁ contra
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : K ∈ s
hK₂ : ∀ (x : LieSubalgebra R { x // x ∈ L' }), x ∈ s → ¬x > K
contra : ¬K = ⊤
K' : LieSubalgebra R { x // x ∈ L' }
hK'₁ : K' ∈ s
hK'₂ : K < K'
⊢ False
[PROOFSTEP]
exact hK₂ K' hK'₁ hK'₂
[GOAL]
case intro.intro
R : Type u₁
L : Type u₂
L₂ : Type u₃
M✝ : Type u₄
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : LieRingModule L M✝
inst✝¹ : LieModule R L M✝
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := LieHom.range (toEndomorphism R L M)
h : ∀ (y : { x // x ∈ L' }), _root_.IsNilpotent ↑y
s : Set (LieSubalgebra R { x // x ∈ L' }) := {K | IsEngelian R { x // x ∈ K }}
hs : Set.Nonempty s
this : ∀ (K : LieSubalgebra R { x // x ∈ L' }), K ∈ s → K ≠ ⊤ → ∃ K', K' ∈ s ∧ K < K'
_i5 : IsNoetherian R { x // x ∈ L' }
K : LieSubalgebra R { x // x ∈ L' }
hK₁ : K ∈ s
hK₂ : ∀ (x : LieSubalgebra R { x // x ∈ L' }), x ∈ s → ¬x > K
hK₃ : K = ⊤
⊢ ⊤ ∈ s
[PROOFSTEP]
exact hK₃ ▸ hK₁