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 = ⊥
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 = ⊥
dsimp only [derivedAbelianOfIdeal]
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 = ⊥

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 = ⊥
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 = ⊥
split
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 = ⊥
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 = ⊥
rename_i h
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 = ⊥
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 = ⊥
rw [derivedLength_zero] at h
no goals
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 = ⊥
rw [h]
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 = ⊥
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 = ⊥
rename_i k h
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 = ⊥
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 = ⊥
obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
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 = ⊥
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 = ⊥
have h₃ : I ≠ ⊥ := by intro contra; apply h₂; rw [contra]; apply derivedSeries_of_bot_eq_bot
no goals
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 = ⊥
simp only [h₂, 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
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
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 ≠ ⊥
intro contra
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 = ⊥
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
apply 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
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 ⊥ = ⊥
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 = ⊥
rw [contra]
no goals
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 ⊥ = ⊥
apply derivedSeries_of_bot_eq_bot