[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
⊢ D (k + l) I = D k (D l I)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
l : ℕ
⊢ D (Nat.zero + l) I = D Nat.zero (D l I)
[PROOFSTEP]
rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
l k : ℕ
ih : D (k + l) I = D k (D l I)
⊢ D (Nat.succ k + l) I = D (Nat.succ k) (D l I)
[PROOFSTEP]
rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
⊢ D k I ≤ D l J
[PROOFSTEP]
revert l
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
k : ℕ
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ Nat.zero → D Nat.zero I ≤ D l J
[PROOFSTEP]
intro l h₂
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
⊢ ∀ {l : ℕ}, l ≤ Nat.succ k → D (Nat.succ k) I ≤ D l J
[PROOFSTEP]
intro l h₂
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ Nat.zero
⊢ D Nat.zero I ≤ D l J
[PROOFSTEP]
rw [Nat.zero_eq, le_zero_iff] at h₂ 
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D Nat.zero I ≤ D l J
[PROOFSTEP]
rw [h₂, derivedSeriesOfIdeal_zero]
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J
[PROOFSTEP]
exact h₁
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J
[PROOFSTEP]
have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂ 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
⊢ l = Nat.succ k ∨ l ≤ k
[PROOFSTEP]
rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂ 
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k ∨ l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
[PROOFSTEP]
cases' h with h h
[GOAL]
case succ.inl
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J
[PROOFSTEP]
rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
[GOAL]
case succ.inl
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆
[PROOFSTEP]
exact LieSubmodule.mono_lie _ _ _ _ (ih (le_refl k)) (ih (le_refl k))
[GOAL]
case succ.inr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
[PROOFSTEP]
rw [derivedSeriesOfIdeal_succ]
[GOAL]
case succ.inr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J
[PROOFSTEP]
exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
J : LieIdeal R L
k l : ℕ
⊢ D (k + l) (I + J) ≤ D k I + D l J
[PROOFSTEP]
let D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆
    monotone' := fun I J h => LieSubmodule.mono_lie I J I J h h }
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
⊢ D (k + l) (I + J) ≤ D k I + D l J
[PROOFSTEP]
have h₁ : ∀ I J : LieIdeal R L, D₁ (I ⊔ J) ≤ D₁ I ⊔ J := by
  simp [LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
⊢ ∀ (I J : LieIdeal R L), ↑D₁ (I ⊔ J) ≤ ↑D₁ I ⊔ J
[PROOFSTEP]
simp [LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (I J : LieIdeal R L), ↑D₁ (I ⊔ J) ≤ ↑D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ D k I + D l J
[PROOFSTEP]
rw [← D₁.iterate_sup_le_sup_iff] at h₁ 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (↑D₁)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑D₁)^[n₁] a₁ ⊔ (↑D₁)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J
[PROOFSTEP]
exact h₁ k l I J
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ D k ⊥ = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ D k ⊥ ≤ ⊥
[PROOFSTEP]
exact derivedSeriesOfIdeal_le_self ⊥ k
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ D 1 I = ⊥
[PROOFSTEP]
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, LieSubmodule.lie_abelian_iff_lie_self_eq_bot]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian { x // x ∈ ↑(D k I) } ↔ D (k + 1) I = ⊥
[PROOFSTEP]
rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ derivedSeries R { x // x ∈ ↑I } k = comap (incl I) (derivedSeriesOfIdeal R L k I)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ derivedSeries R { x // x ∈ ↑I } Nat.zero = comap (incl I) (derivedSeriesOfIdeal R L Nat.zero I)
[PROOFSTEP]
simp only [Nat.zero_eq, derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeries R { x // x ∈ ↑I } k = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R { x // x ∈ ↑I } (Nat.succ k) = comap (incl I) (derivedSeriesOfIdeal R L (Nat.succ k) I)
[PROOFSTEP]
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤, derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
[PROOFSTEP]
rw [ih]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap (incl I) (derivedSeriesOfIdeal R L k I), comap (incl I) (derivedSeriesOfIdeal R L k I)⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
[PROOFSTEP]
exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k) (derivedSeriesOfIdeal_le_self I k)
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ map (incl I) (derivedSeries R { x // x ∈ ↑I } k) = derivedSeriesOfIdeal R L k I
[PROOFSTEP]
rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I
[PROOFSTEP]
apply derivedSeriesOfIdeal_le_self
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ derivedSeries R { x // x ∈ ↑I } k = ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
[PROOFSTEP]
rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeries R { x // x ∈ ↑I } k = ⊥
hJ : derivedSeries R { x // x ∈ ↑J } l = ⊥
⊢ derivedSeries R { x // x ∈ ↑(I + J) } (k + l) = ⊥
[PROOFSTEP]
rw [LieIdeal.derivedSeries_eq_bot_iff] at hI hJ ⊢
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥
[PROOFSTEP]
rw [← le_bot_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
[PROOFSTEP]
let D := derivedSeriesOfIdeal R L
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
[PROOFSTEP]
change D k I = ⊥ at hI 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
hJ : derivedSeriesOfIdeal R L l J = ⊥
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
[PROOFSTEP]
change D l J = ⊥ at hJ 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
[PROOFSTEP]
calc
  D (k + l) (I + J) ≤ D k I + D l J := derivedSeriesOfIdeal_add_le_add I J k l
  _ ≤ ⊥ := by rw [hI, hJ]; simp
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ D k I + D l J ≤ ⊥
[PROOFSTEP]
rw [hI, hJ]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k l : ℕ
I J : LieIdeal R L
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ ⊥ + ⊥ ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ map f (derivedSeries R L' k) ≤ derivedSeries R L k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ map f (derivedSeries R L' Nat.zero) ≤ derivedSeries R L Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeries R L' k) ≤ derivedSeries R L k
⊢ map f (derivedSeries R L' (Nat.succ k)) ≤ derivedSeries R L (Nat.succ k)
[PROOFSTEP]
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeriesOfIdeal R L' k ⊤) ≤ derivedSeriesOfIdeal R L k ⊤
⊢ map f ⁅derivedSeriesOfIdeal R L' k ⊤, derivedSeriesOfIdeal R L' k ⊤⁆ ≤
    ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆
[PROOFSTEP]
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie _ _ _ _ ih ih)
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
h : Function.Surjective ↑f
⊢ map f (derivedSeries R L' k) = derivedSeries R L k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ↑f
⊢ map f (derivedSeries R L' Nat.zero) = derivedSeries R L Nat.zero
[PROOFSTEP]
change (⊤ : LieIdeal R L').map f = ⊤
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ↑f
⊢ map f ⊤ = ⊤
[PROOFSTEP]
rw [← f.idealRange_eq_map]
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ↑f
⊢ LieHom.idealRange f = ⊤
[PROOFSTEP]
exact f.idealRange_eq_top_of_surjective h
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ↑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (Nat.succ k)) = derivedSeries R L (Nat.succ k)
[PROOFSTEP]
simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
hJ : IsSolvable R { x // x ∈ ↑J }
⊢ IsSolvable R { x // x ∈ I + J }
[PROOFSTEP]
obtain ⟨k, hk⟩ := id hI
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
hJ : IsSolvable R { x // x ∈ ↑J }
k : ℕ
hk : derivedSeries R { x // x ∈ ↑I } k = ⊥
⊢ IsSolvable R { x // x ∈ I + J }
[PROOFSTEP]
obtain ⟨l, hl⟩ := id hJ
[GOAL]
case mk.intro.mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
hJ : IsSolvable R { x // x ∈ ↑J }
k : ℕ
hk : derivedSeries R { x // x ∈ ↑I } k = ⊥
l : ℕ
hl : derivedSeries R { x // x ∈ ↑J } l = ⊥
⊢ IsSolvable R { x // x ∈ I + J }
[PROOFSTEP]
exact ⟨⟨k + l, LieIdeal.derivedSeries_add_eq_bot hk hl⟩⟩
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L
h₂ : Injective ↑f
⊢ IsSolvable R L'
[PROOFSTEP]
obtain ⟨k, hk⟩ := id h₁
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L
h₂ : Injective ↑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ IsSolvable R L'
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L
h₂ : Injective ↑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ derivedSeries R L' k = ⊥
[PROOFSTEP]
apply LieIdeal.bot_of_map_eq_bot h₂
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L
h₂ : Injective ↑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← hk]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L
h₂ : Injective ↑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k
[PROOFSTEP]
apply LieIdeal.derivedSeries_map_le
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L'
h₂ : Surjective ↑f
⊢ IsSolvable R L
[PROOFSTEP]
obtain ⟨k, hk⟩ := id h₁
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L'
h₂ : Surjective ↑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ IsSolvable R L
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L'
h₂ : Surjective ↑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ derivedSeries R L k = ⊥
[PROOFSTEP]
rw [← LieIdeal.derivedSeries_map_eq k h₂, hk]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
h₁ : IsSolvable R L'
h₂ : Surjective ↑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
[PROOFSTEP]
simp only [LieIdeal.map_eq_bot_iff, bot_le]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable R L' ↔ IsSolvable R L
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable R L' → IsSolvable R L
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable R L → IsSolvable R L'
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L'
⊢ IsSolvable R L
[PROOFSTEP]
exact e.symm.injective.lieAlgebra_isSolvable
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L
⊢ IsSolvable R L'
[PROOFSTEP]
exact e.injective.lieAlgebra_isSolvable
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsLieAbelian L
⊢ IsSolvable R L
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsLieAbelian L
⊢ derivedSeries R L 1 = ⊥
[PROOFSTEP]
rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsLieAbelian L
⊢ IsLieAbelian L
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
⊢ IsSolvable R { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
have hwf := LieSubmodule.wellFounded_of_noetherian R L L
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : WellFounded fun x x_1 => x > x_1
⊢ IsSolvable R { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
rw [← CompleteLattice.isSupClosedCompact_iff_wellFounded] at hwf 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ IsSolvable R { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
refine' hwf {I : LieIdeal R L | IsSolvable R I} ⟨⊥, _⟩ fun I hI J hJ => _
[GOAL]
case refine'_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ ⊥ ∈ {I | IsSolvable R { x // x ∈ ↑I }}
[PROOFSTEP]
exact LieAlgebra.isSolvableBot R L
[GOAL]
case refine'_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable R { x // x ∈ ↑I }}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable R { x // x ∈ ↑I }}
⊢ I ⊔ J ∈ {I | IsSolvable R { x // x ∈ ↑I }}
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hI hJ ⊢
[GOAL]
case refine'_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : IsSolvable R { x // x ∈ ↑I }
J : LieSubmodule R L L
hJ : IsSolvable R { x // x ∈ ↑J }
⊢ IsSolvable R { x // x ∈ ↑(I ⊔ J) }
[PROOFSTEP]
apply LieAlgebra.isSolvableAdd R L
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
⊢ derivedLengthOfIdeal R L I = k + 1 ↔
    IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) } ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
[PROOFSTEP]
rw [abelian_iff_derived_succ_eq_bot]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
[PROOFSTEP]
let s := {k | derivedSeriesOfIdeal R L k I = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
[PROOFSTEP]
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
have hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s :=
  by
  intro k₁ k₂ h₁₂ h₁
  suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
  change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁ ; rw [← h₁]
  exact derivedSeriesOfIdeal_antitone I h₁₂
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
[PROOFSTEP]
intro k₁ k₂ h₁₂ h₁
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ k₂ ∈ s
[PROOFSTEP]
suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
this : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
⊢ k₂ ∈ s
[PROOFSTEP]
exact eq_bot_iff.mpr this
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ derivedSeriesOfIdeal R L k₂ I ≤ ⊥
[PROOFSTEP]
change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁ 
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : derivedSeriesOfIdeal R L k₁ I = ⊥
⊢ derivedSeriesOfIdeal R L k₂ I ≤ ⊥
[PROOFSTEP]
rw [← h₁]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : derivedSeriesOfIdeal R L k₁ I = ⊥
⊢ derivedSeriesOfIdeal R L k₂ I ≤ derivedSeriesOfIdeal R L k₁ I
[PROOFSTEP]
exact derivedSeriesOfIdeal_antitone I h₁₂
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
exact Nat.sInf_upward_closed_eq_succ_iff hs k
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
⊢ derivedLength R { x // x ∈ ↑I } = derivedLengthOfIdeal R L I
[PROOFSTEP]
let s₁ := {k | derivedSeries R I k = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R { x // x ∈ ↑I } k = ⊥}
⊢ derivedLength R { x // x ∈ ↑I } = derivedLengthOfIdeal R L I
[PROOFSTEP]
let s₂ := {k | derivedSeriesOfIdeal R L k I = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R { x // x ∈ ↑I } k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLength R { x // x ∈ ↑I } = derivedLengthOfIdeal R L I
[PROOFSTEP]
change sInf s₁ = sInf s₂
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R { x // x ∈ ↑I } k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s₁ = sInf s₂
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R { x // x ∈ ↑I } k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s₁ = s₂
[PROOFSTEP]
ext k
[GOAL]
case e_a.h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R { x // x ∈ ↑I } k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂
[PROOFSTEP]
exact I.derivedSeries_eq_bot_iff k
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑(derivedAbelianOfIdeal I) }
[PROOFSTEP]
dsimp only [derivedAbelianOfIdeal]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
⊢ IsLieAbelian
    { x //
      x ∈
        ↑(match derivedLengthOfIdeal R L I with
          | 0 => ⊥
          | Nat.succ k => derivedSeriesOfIdeal R L k I) }
[PROOFSTEP]
cases' h : derivedLengthOfIdeal R L I with k
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = Nat.zero
⊢ IsLieAbelian
    { x //
      x ∈
        ↑(match Nat.zero with
          | 0 => ⊥
          | Nat.succ k => derivedSeriesOfIdeal R L k I) }
[PROOFSTEP]
exact isLieAbelian_bot R L
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
⊢ IsLieAbelian
    { x //
      x ∈
        ↑(match Nat.succ k with
          | 0 => ⊥
          | Nat.succ k => derivedSeriesOfIdeal R L k I) }
[PROOFSTEP]
rw [derivedSeries_of_derivedLength_succ] at h 
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) } ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian
    { x //
      x ∈
        ↑(match Nat.succ k with
          | 0 => ⊥
          | Nat.succ k => derivedSeriesOfIdeal R L k I) }
[PROOFSTEP]
exact h.1
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
[PROOFSTEP]
let s := {k | derivedSeriesOfIdeal R L k I = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
[PROOFSTEP]
change sInf s = 0 ↔ _
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ I = ⊥
[PROOFSTEP]
have hne : s ≠ ∅ := by
  obtain ⟨k, hk⟩ := id hI
  refine' Set.Nonempty.ne_empty ⟨k, _⟩
  rw [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk ; exact hk
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s ≠ ∅
[PROOFSTEP]
obtain ⟨k, hk⟩ := id hI
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R { x // x ∈ ↑I } k = ⊥
⊢ s ≠ ∅
[PROOFSTEP]
refine' Set.Nonempty.ne_empty ⟨k, _⟩
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R { x // x ∈ ↑I } k = ⊥
⊢ k ∈ s
[PROOFSTEP]
rw [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk 
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeriesOfIdeal R L k I = ⊥
⊢ k ∈ s
[PROOFSTEP]
exact hk
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
hI : IsSolvable R { x // x ∈ ↑I }
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
hne : s ≠ ∅
⊢ sInf s = 0 ↔ I = ⊥
[PROOFSTEP]
simp [hne]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h : IsSolvable R { x // x ∈ ↑I }
⊢ derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥
[PROOFSTEP]
dsimp only [derivedAbelianOfIdeal]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h : IsSolvable R { x // x ∈ ↑I }
⊢ (match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | Nat.succ k => derivedSeriesOfIdeal R L k I) =
      ⊥ ↔
    I = ⊥
[PROOFSTEP]
split
  -- Porting note: Original tactic was `cases' h : derivedAbelianOfIdeal R L I with k`
[GOAL]
case h_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h : IsSolvable R { x // x ∈ ↑I }
x✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = 0
⊢ ⊥ = ⊥ ↔ I = ⊥
[PROOFSTEP]
rename_i h
[GOAL]
case h_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ : ℕ
h : derivedLengthOfIdeal R L I = 0
⊢ ⊥ = ⊥ ↔ I = ⊥
[PROOFSTEP]
rw [derivedLength_zero] at h 
[GOAL]
case h_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ : ℕ
h : I = ⊥
⊢ ⊥ = ⊥ ↔ I = ⊥
[PROOFSTEP]
rw [h]
[GOAL]
case h_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h : IsSolvable R { x // x ∈ ↑I }
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = Nat.succ k✝
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥
[PROOFSTEP]
rename_i k h
[GOAL]
case h_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
[PROOFSTEP]
obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
[GOAL]
case h_2.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
[PROOFSTEP]
have h₃ : I ≠ ⊥ := by intro contra; apply h₂; rw [contra]; apply derivedSeries_of_bot_eq_bot
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ I ≠ ⊥
[PROOFSTEP]
intro contra
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
contra : I = ⊥
⊢ False
[PROOFSTEP]
apply h₂
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
contra : I = ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥
[PROOFSTEP]
rw [contra]
[GOAL]
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
contra : I = ⊥
⊢ derivedSeriesOfIdeal R L k ⊥ = ⊥
[PROOFSTEP]
apply derivedSeries_of_bot_eq_bot
[GOAL]
case h_2.intro
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I✝ J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I : LieIdeal R L
h✝ : IsSolvable R { x // x ∈ ↑I }
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = Nat.succ k
left✝ : IsLieAbelian { x // x ∈ ↑(derivedSeriesOfIdeal R L k I) }
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
h₃ : I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
[PROOFSTEP]
simp only [h₂, h₃]
