awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ D (k + 1) I ≤ D l J
have succ₁ : ∀ (h : l ≤ k), D (k + 1) I ≤ D l J
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 + 1) I ≤ D l J
have succ : ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆
Tactic: rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 + 1) I ≤ D l J
have succ : ⁅D k I, D k I⁆ ≤ D l J
Tactic: rw [derivedSeriesOfIdeal_succ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ D k I ≤ D l J
have zero : ∀ {l : ℕ} (h₂ : l ≤ 0), D 0 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)
Cleared hypotheses: k, l, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ D k I ≤ D l J
have 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
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)
Cleared hypotheses: k, l, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
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' := ⋯ }
⊢ D (k + l) (I + J) ≤ D k I + D l J
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
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)
⊢ D (k + l) (I + J) ≤ D k I + D l J
have 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₂
Tactic: rw [← D₁.iterate_sup_le_sup_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
⊢ Eq (α := LieIdeal R L) (D k ⊥) ⊥
have rw : LE.le (α := LieIdeal R L) (D k ⊥) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian.{v} ↥I ↔ D 1 I = ⊥
have rw : IsLieAbelian.{v} ↥I ↔ ⁅D 0 I, D 0 I⁆ = ⊥
Tactic: rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieSubmodule.lie_abelian_iff_lie_self_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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⁆ = ⊥
⊢ IsLieAbelian.{v} ↥I ↔ D 1 I = ⊥
have rw₁ : IsLieAbelian.{v} ↥I ↔ ⁅I, I⁆ = ⊥
Tactic: rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieSubmodule.lie_abelian_iff_lie_self_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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⁆ = ⊥
⊢ IsLieAbelian.{v} ↥I ↔ D 1 I = ⊥
have rw₂ : ⁅I, I⁆ = ⊥ ↔ ⁅I, I⁆ = ⊥
Tactic: rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieSubmodule.lie_abelian_iff_lie_self_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian.{v} ↥(D k I) ↔ D (k + 1) I = ⊥
have rw : IsLieAbelian.{v} ↥(D k I) ↔ D (1 + k) I = ⊥
Tactic: rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 = ⊥
⊢ IsLieAbelian.{v} ↥(D k I) ↔ D (k + 1) I = ⊥
have rw₁ : IsLieAbelian.{v} ↥(D k I) ↔ D 1 (D k I) = ⊥
Tactic: rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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) = ⊥
⊢ IsLieAbelian.{v} ↥(D k I) ↔ D (k + 1) I = ⊥
have rw₂ : D 1 (D k I) = ⊥ ↔ D 1 (D k I) = ⊥
Tactic: rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D k I))
have zero : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) 0 (LieSubmodule.baseChange A I))
  (LieSubmodule.baseChange A (D 0 I))
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I))
    (LieSubmodule.baseChange A (D k I))
have 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))
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) (LieSubmodule.baseChange A (derivedSeries R L k))
have rw : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
  (LieSubmodule.baseChange A (derivedSeries R L k))
Tactic: rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
    LieSubmodule.baseChange_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) (LieSubmodule.baseChange A (derivedSeries R L k))
have rw₁ : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤) (LieSubmodule.baseChange A (D k ⊤))
Tactic: rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
    LieSubmodule.baseChange_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 ⊤))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) (LieSubmodule.baseChange A (derivedSeries R L k))
have rw₂ : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
  (derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A ⊤))
Tactic: rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
    LieSubmodule.baseChange_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 ⊤))
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) (LieSubmodule.baseChange A (derivedSeries R L k))
have rw₃ : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤) (derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤)
Tactic: rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
    LieSubmodule.baseChange_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)
have 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⁆
Tactic: simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ 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⁆
have 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⁆
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
have zero : derivedSeries R (↥I) 0 = comap I.incl (derivedSeriesOfIdeal R L 0 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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
have 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)
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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ map I.incl (derivedSeries R (↥I) k) = derivedSeriesOfIdeal R L k I
have rw : derivedSeriesOfIdeal R L k I ≤ I
Tactic: rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
have rw : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ map I.incl (derivedSeries R (↥I) k) = ⊥
Tactic: rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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) = ⊥
⊢ Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
have rw₁ : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeries R (↥I) k ≤ I.incl.ker
Tactic: rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
have rw₂ : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
Tactic: rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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) ⊥
⊢ Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
have rw₃ : LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥ ↔ LE.le.{v} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
Tactic: rw [← derivedSeries_eq_derivedSeriesOfIdeal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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) ⊥
⊢ Eq.{v + 1} (α := LieIdeal R ↥(I + J)) (derivedSeries R (↥(I + J)) (k + l)) ⊥
have rw : ∀ (hI : derivedSeriesOfIdeal R L k I = ⊥) (hJ : derivedSeriesOfIdeal R L l J = ⊥),
  derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥
Tactic: rw [LieIdeal.derivedSeries_eq_bot_iff] at hI hJ ⊢
Cleared hypotheses: hI, hJ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥
have rw : derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
Tactic: rw [← le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 I + D l J ≤ ⊥
have rw : HAdd.hAdd (α := LieIdeal R L) ⊥ ⊥ ≤ ⊥
Tactic: rw [hI, hJ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
have D₁ : D k I + D l 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ map f (derivedSeries R L' (k + 1)) ≤ derivedSeries R L (k + 1)
have 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 ⊤)
Tactic: simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
⊢ map f (derivedSeries R L' k) ≤ derivedSeries R L k
have zero : map f (derivedSeries R L' 0) ≤ derivedSeries R L 0
Tactic: induction k with
  | zero => simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]
  | succ k ih =>
    simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
    exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
zero : map f (derivedSeries R L' 0) ≤ derivedSeries R L 0
⊢ map f (derivedSeries R L' k) ≤ derivedSeries R L k
have succ : ∀ (k : ℕ) (ih : map f (derivedSeries R L' k) ≤ derivedSeries R L k),
  map f (derivedSeries R L' (k + 1)) ≤ derivedSeries R L (k + 1)
Tactic: induction k with
  | zero => simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]
  | succ k ih =>
    simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
    exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ map f ⊤ = ⊤
have zero : f.idealRange = ⊤
Tactic: rw [← f.idealRange_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ map f (derivedSeries R L' k) = derivedSeries R L k
have zero : map f (derivedSeries R L' 0) = derivedSeries R L 0
Tactic: induction k with
  | zero =>
    change (⊤ : LieIdeal R L').map f = ⊤
    rw [← f.idealRange_eq_map]
    exact f.idealRange_eq_top_of_surjective h
  | succ k ih => simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
zero : map f (derivedSeries R L' 0) = derivedSeries R L 0
⊢ map f (derivedSeries R L' k) = derivedSeries R L k
have succ : ∀ (k : ℕ) (ih : map f (derivedSeries R L' k) = derivedSeries R L k),
  map f (derivedSeries R L' (k + 1)) = derivedSeries R L (k + 1)
Tactic: induction k with
  | zero =>
    change (⊤ : LieIdeal R L').map f = ⊤
    rw [← f.idealRange_eq_map]
    exact f.idealRange_eq_top_of_surjective h
  | succ k ih => simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1 + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
have succ : Eq (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)) ⊤ ↔
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
Tactic: rw [derivedSeriesOfIdeal_succ]