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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
h : Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
⊢ Eq (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)) ⊤
have rwa : Eq.{v + 1} (α := LieIdeal R L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) ⊤
Tactic: rwa [ih.mpr 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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
⊢ 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 ⊤) ⊤
have succ : ∀
  (h :
    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: refine ⟨fun h ↦ ?_, fun h ↦ by rwa [ih.mpr 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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
h :
  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 ⊤) ⊤
have succ : LE.le (α := LieIdeal R L) ⊤ (derivedSeriesOfIdeal R L (n + 1) ⊤)
Tactic: rw [← ih, eq_top_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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
h :
  Eq (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)) ⊤
| ⊤
have rw : Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)
Tactic: rw [← 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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
h :
  Eq (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)) ⊤
⊢ LE.le (α := LieIdeal R L) ⊤ (derivedSeriesOfIdeal R L (n + 1) ⊤)
have succ : LE.le (α := LieIdeal R L)
  (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤))
  (derivedSeriesOfIdeal R L (n + 1) ⊤)
Tactic: conv_lhs => rw [← 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
n : ℕ
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
have zero : Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (HAdd.hAdd (α := ℕ) 0 1) ⊤) ⊤ ↔
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [derivedSeriesOfIdeal_succ]
    refine ⟨fun h ↦ ?_, fun h ↦ by rwa [ih.mpr h]⟩
    rw [← ih, eq_top_iff]
    conv_lhs => rw [← h]
    exact LieSubmodule.lie_le_right _ _
Cleared hypotheses: n
-- 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 : ℕ
zero :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (HAdd.hAdd (α := ℕ) 0 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
have succ : ∀ (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 ⊤) ⊤
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [derivedSeriesOfIdeal_succ]
    refine ⟨fun h ↦ ?_, fun h ↦ by rwa [ih.mpr h]⟩
    rw [← ih, eq_top_iff]
    conv_lhs => rw [← h]
    exact LieSubmodule.lie_le_right _ _
Cleared hypotheses: n
-- 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 : ℕ
h : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeries R L n) ⊤
have zero : Eq (α := LieIdeal R L) (derivedSeries R L 0) ⊤
Tactic: cases n
Cleared hypotheses: n
-- 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 : ℕ
h : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
zero : Eq (α := LieIdeal R L) (derivedSeries R L 0) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeries R L n) ⊤
have succ : ∀ (n : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L (n + 1)) ⊤
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
hx : x ∈ (↑(Submodule.span R₁ S) : Set L)
⊢ x ∈ (↑(Submodule.span R₂ S) : Set L)
have hx₁ : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) x
Tactic: simp only [SetLike.mem_coe] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
y : L
hy : y ∈ S
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • y)
have smul_mem : ∀ (a : L) (ha : a ∈ I) (b : L) (hb : b ∈ I), Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • ⁅a, b⁆)
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • ⁅a, b⁆)
have smul_mem : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) ⁅c • a, b⁆
Tactic: rw [← smul_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) ⁅c • a, b⁆
have smul_mem : c • a ∈ I
Tactic: refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ c • a ∈ I
have smul_mem : ∀ (ha : Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) a) (b : L) (hb : b ∈ I),
  Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) (c • a)
Tactic: rw [← ih] at ha ⊢
Cleared hypotheses: ha, b, hb
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
hx : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) x
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) x
have zero : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) 0
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, ha, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
      rw [← ih] at ha ⊢
      exact Submodule.smul_mem _ _ ha
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
hx : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) x
zero : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) 0
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) x
have add : ∀ (y z : L) (hy₁ : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) y)
  (hz₁ : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) z)
  (hy₂ : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) y)
  (hz₂ : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) z),
  Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (y + z)
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, ha, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
      rw [← ih] at ha ⊢
      exact Submodule.smul_mem _ _ ha
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : LieRing L
inst_3 : LieAlgebra R₁ L
inst_4 : LieAlgebra R₂ L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R₁ L) (derivedSeriesOfIdeal R₁ L k ⊤) x ↔
      Membership.mem (γ := LieIdeal R₂ L) (derivedSeriesOfIdeal R₂ L k ⊤) x
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x : L | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
hx : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) x
zero : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) 0
add :
  ∀ (y z : L) (hy₁ : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) y)
    (hz₁ : Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) z)
    (hy₂ : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) y)
    (hz₂ : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) z),
    Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (y + z)
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) x
have smul_mem : ∀ (c : R₁) (y : L) (hy : y ∈ S), Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • y)
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, ha, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
      rw [← ih] at ha ⊢
      exact Submodule.smul_mem _ _ ha
Cleared hypotheses: hx
-- 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 : ℕ
⊢ (↑(derivedSeries R L k) : Set L) = (↑(derivedSeries ℤ L k) : Set L)
have rw : (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
  (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
Tactic: rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule, derivedSeries_def,
    derivedSeries_def]
-- 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 : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(↑(derivedSeriesOfIdeal R L (k + 1) ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L (k + 1) ⊤) : Submodule ℤ L) : Set L)
have succ : (↑(↑(Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤)) :
        Submodule R L) :
    Set L) =
  (↑(↑(Bracket.bracket (L := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) (derivedSeriesOfIdeal ℤ L k ⊤)) :
        Submodule ℤ L) :
    Set L)
Tactic: rw [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
k : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(↑(Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤)) :
          Submodule R L) :
      Set L) =
    (↑(↑(Bracket.bracket (L := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) (derivedSeriesOfIdeal ℤ L k ⊤)) :
          Submodule ℤ L) :
      Set L)
have succ : (↑(Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L) =
  (↑(Submodule.span ℤ
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L)
Tactic: rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
-- 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
k : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
have ih₁ : ∀ (x : L),
  x ∈ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) ↔
    x ∈ (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
Tactic: rw [Set.ext_iff] at ih
Cleared hypotheses: ih
-- 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
k : ℕ
ih :
  ∀ (x : L),
    x ∈ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) ↔
      x ∈ (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
have ih₁ : ∀ (x : L),
  Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
    Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
Tactic: simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
Cleared hypotheses: 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
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
have succ : (↑(Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L) =
  (↑(Submodule.span ℤ
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L)
Tactic: simp only [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
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
have succ : (↑(Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L) ≤
  (↑(Submodule.span ℤ
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L)
Tactic: apply le_antisymm
-- 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 : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
succ :
  (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
have succ₁ : (↑(Submodule.span ℤ
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L) ≤
  (↑(Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
    Set L)
Tactic: apply le_antisymm
-- 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 : ℕ
⊢ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
have zero : (↑(↑(derivedSeriesOfIdeal R L 0 ⊤) : Submodule R L) : Set L) =
  (↑(↑(derivedSeriesOfIdeal ℤ L 0 ⊤) : Submodule ℤ L) : Set L)
Tactic: induction k with
  | zero => rfl
  | succ k ih =>
    rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [ih]
    apply le_antisymm
    · exact coe_derivedSeries_eq_int_aux _ _ L k ih
    · simp
Cleared hypotheses: k