awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
rwa : ∀ (h₂ : l = k + 1 ∨ l < k + 1), l = k.succ ∨ l ≤ k
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h₂ : l = k + 1 ∨ l ≤ k), l = k.succ ∨ l ≤ k
⊢ l = k.succ ∨ l ≤ k

Tactic:
rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂

Premises used: le_iff_eq_or_lt, Nat.lt_succ_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ l = k.succ ∨ l ≤ k

Tactic:
have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ ∨ l ≤ k
succ : ∀ (h : l = k.succ), D (k + 1) I ≤ D l J
succ₁ : ∀ (h : l ≤ k), D (k + 1) I ≤ D l J
⊢ D (k + 1) I ≤ D l J

Tactic:
rcases h with h | h
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
succ : ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆
⊢ D (k + 1) I ≤ D l J

Tactic:
rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆

Tactic:
LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))

Premises used: le_refl, Set.Mem, LieSubmodule.mono_lie
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆

Tactic:
exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))

Premises used: le_refl, LieSubmodule.mono_lie
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
succ : ⁅D k I, D k I⁆ ≤ D l J
⊢ D (k + 1) I ≤ D l J

Tactic:
rw [derivedSeriesOfIdeal_succ]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J

Tactic:
le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Premises used: LieSubmodule.lie_le_left, le_trans
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J

Tactic:
exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Premises used: LieSubmodule.lie_le_left, le_trans
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
zero : ∀ {l : ℕ} (h₂ : l ≤ 0), D 0 I ≤ D l J
succ : ∀ (k : ℕ) (ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J) {l : ℕ} (h₂ : l ≤ k + 1), D (k + 1) I ≤ D l J
⊢ D k I ≤ D l J

Tactic:
induction k generalizing l with
  | zero => rw [le_zero_iff] at h₂; rw [h₂, derivedSeriesOfIdeal_zero]; exact h₁
  | succ k ih =>
    have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
    rcases h with h | h
    · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
      exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
    · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Premises used: le_zero_iff, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ D (k + 1) I ≤ D k I

Tactic:
derivedSeriesOfIdeal_le le_rfl k.le_succ

Premises used: le_rfl, Nat.le_succ, LieAlgebra.derivedSeriesOfIdeal_le
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ D k I ≤ I

Tactic:
derivedSeriesOfIdeal_le le_rfl zero_le

Premises used: zero_le, le_rfl, Set.Mem, LieAlgebra.derivedSeriesOfIdeal_le
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h : I ≤ J
k : ℕ
⊢ D k I ≤ D k J

Tactic:
derivedSeriesOfIdeal_le h le_rfl

Premises used: le_rfl, LieAlgebra.derivedSeriesOfIdeal_le
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k l : ℕ
h : l ≤ k
⊢ D k I ≤ D l I

Tactic:
derivedSeriesOfIdeal_le le_rfl h

Premises used: le_rfl, LieAlgebra.derivedSeriesOfIdeal_le
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun (I : LieIdeal R L) ↦ ⁅I, I⁆, monotone' := ⋯ }
⊢ ∀ (I J : LieIdeal R L),
    LE.le (α := LieIdeal R L) ((D₁ : (a : LieIdeal R L) → LieIdeal R L) (I ⊔ J) : LieIdeal R L)
      ((D₁ : (a : LieIdeal R L) → LieIdeal R L) I ⊔ J : LieIdeal R L)

Tactic:
simp [D₁, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]

Premises used: le_sup_of_le_right, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun (I : LieIdeal R L) ↦ ⁅I, I⁆, monotone' := ⋯ }
⊢ ∀ (I J : LieIdeal R L),
    LE.le (α := LieIdeal R L) ((D₁ : (a : LieIdeal R L) → LieIdeal R L) (I ⊔ J) : LieIdeal R L)
      ((D₁ : (a : LieIdeal R L) → LieIdeal R L) I ⊔ J : LieIdeal R L)

Tactic:
have h₁ : ∀ I J : LieIdeal R L, D₁ (I ⊔ J) ≤ D₁ I ⊔ J := by
    simp [D₁, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun (I : LieIdeal R L) ↦ ⁅I, I⁆, monotone' := ⋯ }
h₁ :
  ∀ (I J : LieIdeal R L),
    LE.le (α := LieIdeal R L) ((D₁ : (a : LieIdeal R L) → LieIdeal R L) (I ⊔ J) : LieIdeal R L)
      ((D₁ : (a : LieIdeal R L) → LieIdeal R L) I ⊔ J : LieIdeal R L)
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L),
    (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁ + n₂] (a₁ ⊔ a₂) ≤
      (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁] a₁ ⊔ (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₂] a₂

Tactic:
rw [← D₁.iterate_sup_le_sup_iff] at h₁

Premises used: OrderHom.iterate_sup_le_sup_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun (I : LieIdeal R L) ↦ ⁅I, I⁆, monotone' := ⋯ }
h₁ :
  ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L),
    (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁ + n₂] (a₁ ⊔ a₂) ≤
      (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁] a₁ ⊔ (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
h₁ k l I J

Premises used: Set.Mem, setOf, LieSubmodule.lieSpan
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun (I : LieIdeal R L) ↦ ⁅I, I⁆, monotone' := ⋯ }
h₁ :
  ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L),
    (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁ + n₂] (a₁ ⊔ a₂) ≤
      (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₁] a₁ ⊔ (⇑D₁ : (a : LieIdeal R L) → LieIdeal R L)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
exact h₁ k l I J
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
rw : LE.le (α := LieIdeal R L) (D k ⊥) ⊥
⊢ Eq (α := LieIdeal R L) (D k ⊥) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
⊢ LE.le (α := LieIdeal R L) (D k ⊥) ⊥

Tactic:
derivedSeriesOfIdeal_le_self ⊥ k

Premises used: Set.Mem, LieAlgebra.derivedSeriesOfIdeal_le_self, Bot.bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
⊢ LE.le (α := LieIdeal R L) (D k ⊥) ⊥

Tactic:
exact derivedSeriesOfIdeal_le_self ⊥ k

Premises used: LieAlgebra.derivedSeriesOfIdeal_le_self, Bot.bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
rw : IsLieAbelian.{v} ↥I ↔ ⁅D 0 I, D 0 I⁆ = ⊥
rw₁ : IsLieAbelian.{v} ↥I ↔ ⁅I, I⁆ = ⊥
rw₂ rw₃ : ⁅I, I⁆ = ⊥ ↔ ⁅I, I⁆ = ⊥
⊢ IsLieAbelian.{v} ↥I ↔ D 1 I = ⊥

Tactic:
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieSubmodule.lie_abelian_iff_lie_self_eq_bot]

Premises used: LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
rw : IsLieAbelian.{v} ↥(D k I) ↔ D (1 + k) I = ⊥
rw₁ : IsLieAbelian.{v} ↥(D k I) ↔ D 1 (D k I) = ⊥
rw₂ rw₃ : D 1 (D k I) = ⊥ ↔ D 1 (D k I) = ⊥
⊢ IsLieAbelian.{v} ↥(D k I) ↔ D (k + 1) I = ⊥

Tactic:
rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]

Premises used: LieAlgebra.abelian_iff_derived_one_eq_bot, add_comm, LieAlgebra.derivedSeriesOfIdeal_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) 0 (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D 0 I))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
k : ℕ
ih :
  Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D k I))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) (k + 1) (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D (k + 1) I))

Tactic:
simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieSubmodule.lie_baseChange
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
k : ℕ
zero :
  Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) 0 (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D 0 I))
succ :
  ∀ (k : ℕ)
    (ih :
      Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I))
        (LieSubmodule.baseChange A (D k I))),
    Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) (k + 1) (LieSubmodule.baseChange A I))
      (LieSubmodule.baseChange A (D (k + 1) I))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D k I))

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieSubmodule.lie_baseChange
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
k : ℕ
rw :
  Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
    (LieSubmodule.baseChange A (derivedSeries R L k))
rw₁ : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤) (LieSubmodule.baseChange A (D k ⊤))
rw₂ :
  Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
    (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A ⊤))
rw₃ rw₄ :
  Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) (LieSubmodule.baseChange A (derivedSeries R L k))

Tactic:
rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
    LieSubmodule.baseChange_top]

Premises used: LieAlgebra.derivedSeries_def, LieAlgebra.derivedSeriesOfIdeal_baseChange, LieSubmodule.baseChange_top
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ derivedSeries R (↥I) 0 = comap I.incl (derivedSeriesOfIdeal R L 0 I)

Tactic:
simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]

Premises used: LieAlgebra.derivedSeries_def, LieIdeal.comap_incl_self, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
succ :
  Bracket.bracket (L := LieIdeal R ↥I) (derivedSeriesOfIdeal R (↥I) k ⊤) (derivedSeriesOfIdeal R (↥I) k ⊤) =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
⊢ derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
succ :
  ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
⊢ Bracket.bracket (L := LieIdeal R ↥I) (derivedSeriesOfIdeal R (↥I) k ⊤) (derivedSeriesOfIdeal R (↥I) k ⊤) =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

Premises used: LieIdeal.comap_bracket_incl_of_le, LieAlgebra.derivedSeriesOfIdeal_le_self
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

Premises used: LieIdeal.comap_bracket_incl_of_le, LieAlgebra.derivedSeriesOfIdeal_le_self
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
zero : derivedSeries R (↥I) 0 = comap I.incl (derivedSeriesOfIdeal R L 0 I)
succ :
  ∀ (k : ℕ) (ih : derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)),
    derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)
⊢ derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)

Tactic:
induction k with
  | zero => simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
  | succ k ih =>
    simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢; rw [ih]
    exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

Premises used: LieIdeal.comap_bracket_incl_of_le, LieAlgebra.derivedSeriesOfIdeal_le_self, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def, LieIdeal.comap_incl_self, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
rw : derivedSeriesOfIdeal R L k I ≤ I
⊢ map I.incl (derivedSeries R (↥I) k) = derivedSeriesOfIdeal R L k I

Tactic:
rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]

Premises used: LieIdeal.map_comap_incl, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, inf_eq_right
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I

Tactic:
apply derivedSeriesOfIdeal_le_self

Premises used: LieAlgebra.derivedSeriesOfIdeal_le_self
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
rw : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ map I.incl (derivedSeries R (↥I) k) = ⊥
rw₁ : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeries R (↥I) k ≤ I.incl.ker
rw₂ :
  Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
rw₃ rw₄ :
  LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
⊢ Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥

Tactic:
rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]

Premises used: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, eq_bot_iff, LieIdeal.ker_incl, LieIdeal.map_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hI : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
hJ : Eq.{v + 1} (α := LieIdeal R ↥J) (derivedSeries R (↥J) l) ⊥
rw :
  ∀ (hI : derivedSeriesOfIdeal R L k I = ⊥) (hJ : derivedSeriesOfIdeal R L l J = ⊥),
    derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥
⊢ Eq.{v + 1} (α := LieIdeal R ↥(I + J)) (derivedSeries R (↥(I + J)) (k + l)) ⊥

Tactic:
rw [LieIdeal.derivedSeries_eq_bot_iff] at hI hJ ⊢

Premises used: LieIdeal.derivedSeries_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
rw : derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥

Tactic:
rw [← le_bot_iff]

Premises used: le_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
⊢ D k I = ⊥

Tactic:
change D k I = ⊥ at hI
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hJ : derivedSeriesOfIdeal R L l J = ⊥
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
⊢ D l J = ⊥

Tactic:
change D l J = ⊥ at hJ
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
derivedSeriesOfIdeal_add_le_add I J k l

Premises used: Set.Mem, setOf, LieAlgebra.derivedSeriesOfIdeal_add_le_add
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
rw : HAdd.hAdd (α := LieIdeal R L) ⊥ ⊥ ≤ ⊥
⊢ D k I + D l J ≤ ⊥

Tactic:
rw [hI, hJ]
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ HAdd.hAdd (α := LieIdeal R L) ⊥ ⊥ ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
D : (k : ℕ) → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
D₁ : D k I + D l J ≤ ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥

Tactic:
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

Premises used: LieAlgebra.derivedSeriesOfIdeal_add_le_add, HAdd.hAdd
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
⊢ map f (derivedSeries R L' 0) ≤ derivedSeries R L 0

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]

Premises used: LieAlgebra.derivedSeries_def, le_top, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeries R L' k) ≤ derivedSeries R L k
succ :
  map f (Bracket.bracket (L := LieIdeal R L') (derivedSeriesOfIdeal R L' k ⊤) (derivedSeriesOfIdeal R L' k ⊤)) ≤
    Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤)
⊢ map f (derivedSeries R L' (k + 1)) ≤ derivedSeries R L (k + 1)

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeriesOfIdeal R L' k ⊤) ≤ derivedSeriesOfIdeal R L k ⊤
⊢ map f (Bracket.bracket (L := LieIdeal R L') (derivedSeriesOfIdeal R L' k ⊤) (derivedSeriesOfIdeal R L' k ⊤)) ≤
    Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤)

Tactic:
le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, le_trans