awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, le_trans
-- 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 : ℕ
zero : map f (derivedSeries R L' 0) ≤ derivedSeries R L 0
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)
⊢ map f (derivedSeries R L' k) ≤ derivedSeries R L k

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)

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, 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
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
zero : f.idealRange = ⊤
⊢ map f ⊤ = ⊤

Tactic:
rw [← f.idealRange_eq_map]

Premises used: LieHom.idealRange_eq_map
-- 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
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ f.idealRange = ⊤

Tactic:
f.idealRange_eq_top_of_surjective h

Premises used: LieHom.idealRange_eq_top_of_surjective
-- 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
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ f.idealRange = ⊤

Tactic:
exact f.idealRange_eq_top_of_surjective h

Premises used: LieHom.idealRange_eq_top_of_surjective
-- 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
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → 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)

Tactic:
simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def, LieIdeal.map_bracket_eq
-- 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 : ℕ
h : Function.Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
zero : map f (derivedSeries R L' 0) = derivedSeries R L 0
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)
⊢ map f (derivedSeries R L' k) = derivedSeries R L k

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]

Premises used: LieIdeal.map, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def, LieHom.idealRange_eq_map, LieIdeal.map_bracket_eq, Top.top, LieHom.idealRange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (HAdd.hAdd (α := ℕ) 0 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤

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
n : ℕ
ih :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
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 ⊤) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1 + 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤

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
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 ⊤) ⊤
rwa rwa₁ rwa₂ rwa₃ : Eq.{v + 1} (α := LieIdeal R L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) ⊤
⊢ Eq (α := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)) ⊤

Tactic:
rwa [ih.mpr h]

Premises used: Iff.mpr
-- Module: Mathlib.Algebra.Lie.Solvable
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 ⊤) ⊤
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 ⊤) ⊤
⊢ 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]⟩
-- Module: Mathlib.Algebra.Lie.Solvable
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) ⊤)) ⊤
succ : LE.le (α := LieIdeal R L) ⊤ (derivedSeriesOfIdeal R L (n + 1) ⊤)
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤

Tactic:
rw [← ih, eq_top_iff]

Premises used: eq_top_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
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) ⊤)) ⊤
rw : Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤)
| ⊤

Tactic:
rw [← 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
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) ⊤)) ⊤
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) ⊤)
⊢ LE.le (α := LieIdeal R L) ⊤ (derivedSeriesOfIdeal R L (n + 1) ⊤)

Tactic:
conv_lhs => rw [← 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
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)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤))
    (derivedSeriesOfIdeal R L (n + 1) ⊤)

Tactic:
LieSubmodule.lie_le_right _ _

Premises used: Set.Mem, LieSubmodule.lie_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
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)
    (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 1) ⊤) (derivedSeriesOfIdeal R L (n + 1) ⊤))
    (derivedSeriesOfIdeal R L (n + 1) ⊤)

Tactic:
exact LieSubmodule.lie_le_right _ _

Premises used: LieSubmodule.lie_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
n : ℕ
zero :
  Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (HAdd.hAdd (α := ℕ) 0 1) ⊤) ⊤ ↔
    Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L 1 ⊤) ⊤
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 ⊤) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L (n + 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 _ _

Premises used: eq_top_iff, LieAlgebra.derivedSeriesOfIdeal_succ, LieSubmodule.lie_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
n : ℕ
h : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
zero : Eq (α := LieIdeal R L) (derivedSeries R L 0) ⊤
succ : ∀ (n : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L (n + 1)) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeries R L n) ⊤

Tactic:
cases n
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeries R L 0) ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
n : ℕ
succ succ₁ succ₂ succ₃ : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ Eq (α := LieIdeal R L) (derivedSeries R L (n + 1)) ⊤

Tactic:
rwa [derivedSeries_succ_eq_top_iff]

Premises used: LieIdeal.derivedSeries_succ_eq_top_iff
-- Module: Mathlib.Algebra.Lie.Solvable
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)
⊢ Membership.mem (γ := Submodule R₁ L) (Submodule.span R₁ S) x

Tactic:
simp only [SetLike.mem_coe] at hx ⊢

Premises used: SetLike.mem_coe
-- Module: Mathlib.Algebra.Lie.Solvable
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
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) 0

Tactic:
Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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 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:
Submodule.add_mem _ hy₂ hz₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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 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:
exact Submodule.add_mem _ hy₂ hz₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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
smul_mem :
  ∀ (a : L) (ha : a ∈ I) (b : L) (hb : b ∈ I), Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • ⁅a, b⁆)
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • y)

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Solvable
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
smul_mem : Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) ⁅c • a, b⁆
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • ⁅a, b⁆)

Tactic:
rw [← smul_lie]

Premises used: smul_lie
-- Module: Mathlib.Algebra.Lie.Solvable
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⁆

Tactic:
Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩

Premises used: And.intro, Exists.intro, HSMul.hSMul, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Lie.Solvable
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
smul_mem : c • a ∈ I
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) ⁅c • a, b⁆

Tactic:
refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
-- Module: Mathlib.Algebra.Lie.Solvable
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
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)
⊢ c • a ∈ I

Tactic:
rw [← ih] at ha ⊢
-- Module: Mathlib.Algebra.Lie.Solvable
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 : 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:
Submodule.smul_mem _ _ ha

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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 : 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:
exact Submodule.smul_mem _ _ ha

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Solvable
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)
smul_mem : ∀ (c : R₁) (y : L) (hy : y ∈ S), Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) (c • y)
⊢ Membership.mem (γ := Submodule R₂ L) (Submodule.span R₂ S) x

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

Premises used: smul_lie, Submodule.zero_mem, rfl
-- 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 :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(derivedSeries R L k) : Set L) = (↑(derivedSeries ℤ L k) : Set L)

Tactic:
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule, derivedSeries_def,
    derivedSeries_def]

Premises used: LieAlgebra.derivedSeries_def, LieSubmodule.coe_toSubmodule
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ (↑(↑(derivedSeriesOfIdeal R L 0 ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L 0 ⊤) : Submodule ℤ L) : Set L)

Tactic:
rfl
-- 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 : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
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)
⊢ (↑(↑(derivedSeriesOfIdeal R L (k + 1) ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L (k + 1) ⊤) : Submodule ℤ L) : Set L)

Tactic:
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ