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) }
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) }
dsimp only [derivedAbelianOfIdeal]
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) }

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) }
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) }
cases' h : derivedLengthOfIdeal R L I with k
no goals
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) }
exact isLieAbelian_bot R L
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) }
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) }
rw [derivedSeries_of_derivedLength_succ] at h
no goals
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) }
exact h.1