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
k : ℕ
zero :
  (↑(↑(derivedSeriesOfIdeal R L 0 ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L 0 ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
have succ : ∀ (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)
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
⊢ IsSolvable.{v} ↥(I + J)
have obtain : ∀ (k : ℕ) (hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥), IsSolvable.{v} ↥(I + J)
Tactic: obtain ⟨k, hk⟩ := IsSolvable.solvable R I
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
⊢ IsSolvable.{v} ↥(I + J)
have obtain : ∀ (l : ℕ) (hl : Eq.{v + 1} (α := LieIdeal R ↥J) (derivedSeries R (↥J) l) ⊥), IsSolvable.{v} ↥(I + J)
Tactic: obtain ⟨l, hl⟩ := IsSolvable.solvable R J
-- 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
inst_3 : IsSolvable L
inst_4 : Nontrivial L
⊢ LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤
have obtain : ∀ (n : ℕ) (hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥), LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤
Tactic: obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)
-- 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
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥
⊢ LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤
have rw : Ne (α := LieIdeal R L) (derivedSeries R L 1) ⊤
Tactic: rw [lt_top_iff_ne_top]
-- 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
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥
contra : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ False
have hn₁ : Eq.{v + 1} (α := LieIdeal R L) ⊤ ⊥
Tactic: rw [LieIdeal.derivedSeries_eq_top n contra] at hn
Cleared hypotheses: hn, contra
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
⊢ IsSolvable (A ⊗[R] L)
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥), IsSolvable (A ⊗[R] L)
Tactic: obtain ⟨k, hk⟩ := IsSolvable.solvable R L
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ IsSolvable (A ⊗[R] L)
have rw : ∃ (k : ℕ), Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
Tactic: rw [isSolvable_iff A]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
have h : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
Tactic: rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
have h₁ : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A ⊥) ⊥
Tactic: rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
h₁ : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A ⊥) ⊥
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
have h₂ : Eq (α := LieIdeal A (A ⊗[R] L)) ⊥ ⊥
Tactic: rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) ↔ IsSolvable L
have refine : IsSolvable (A ⊗[R] L) → IsSolvable L
Tactic: refine ⟨?_, fun _ ↦ inferInstance⟩
-- 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
inst_5 : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) → IsSolvable L
have rw : (∃ (k : ℕ), Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥) →
  ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
Tactic: rw [isSolvable_iff A, isSolvable_iff R]
-- 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
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
have h₁ : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
Tactic: use 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
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
have h₁ : ∀ (h : LE.le (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥),
  LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊥
Tactic: rw [eq_bot_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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : LE.le (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ x
have h₁ : ∀ (h : LE.le (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥) ⦃x : L⦄
  (hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x), Membership.mem (γ := LieSubmodule R L L) ⊥ x
Tactic: rw [derivedSeries_baseChange] at h
Cleared hypotheses: h, x, hx
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : LE.le (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ x
have h₁ : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) ⊥ (1 ⊗ₜ[R] x)
Tactic: specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx
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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
h : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) ⊥ (1 ⊗ₜ[R] x)
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ x
have h₁ : ∀ (h : Eq (α := A ⊗[R] L) (1 ⊗ₜ[R] x) 0), x = 0
Tactic: rw [LieSubmodule.mem_bot] 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
h : Eq (α := A ⊗[R] L) (1 ⊗ₜ[R] x) 0
⊢ x = 0
have h₁ : ∀ (h : x = 0), x = 0
Tactic: rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h
Cleared hypotheses: h
-- 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
hL : IsSolvable L
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ IsSolvable L'
have rw : ∀ (hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥)
  (h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)),
  ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
Tactic: rw [isSolvable_iff R] at hL ⊢
Cleared hypotheses: hL, h
-- 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
hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
have apply : ∀ (a : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L a) ⊥ → Eq (α := LieIdeal R L') (derivedSeries R L' a) ⊥
Tactic: apply hL.imp
-- 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
hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
have apply : LieIdeal.map f (derivedSeries R L' k) = ⊥
Tactic: apply LieIdeal.bot_of_map_eq_bot h
-- 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
hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥
have rw : LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k
Tactic: rw [eq_bot_iff, ← hk]
-- 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
hL' : IsSolvable L'
h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ IsSolvable L
have rw : ∀ (hL' : ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥)
  (h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)),
  ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
Tactic: rw [isSolvable_iff R] at hL' ⊢
Cleared hypotheses: hL', h
-- 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
hL' : ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
have apply : ∀ (a : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' a) ⊥ → Eq (α := LieIdeal R L) (derivedSeries R L a) ⊥
Tactic: apply hL'.imp
-- 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
hL' : ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
k : ℕ
hk : Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
have rw : LieIdeal.map f ⊥ = ⊥
Tactic: rw [← LieIdeal.derivedSeries_map_eq k h, hk]
-- 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'
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable L' ↔ IsSolvable L
have mp : IsSolvable L' → IsSolvable L
Tactic: constructor
-- 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'
e : L' ≃ₗ⁅R⁆ L
mp : IsSolvable L' → IsSolvable L
⊢ IsSolvable L' ↔ IsSolvable L
have mpr : IsSolvable L → IsSolvable L'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsLieAbelian L
⊢ IsSolvable L
have h : Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L 1) ⊥
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsNoetherian R L
⊢ IsSolvable.{v} ↥(radical R L)
have hwf : WellFoundedGT.{v} (LieSubmodule R L L)
Tactic: have hwf := LieSubmodule.wellFoundedGT_of_noetherian R L L
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsNoetherian R L
hwf : WellFoundedGT.{v} (LieSubmodule R L L)
⊢ IsSolvable.{v} ↥(radical R L)
have hwf₁ : CompleteLattice.IsSupClosedCompact.{v} (LieSubmodule R L L)
Tactic: rw [← CompleteLattice.isSupClosedCompact_iff_wellFoundedGT] at hwf
Cleared hypotheses: hwf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact.{v} (LieSubmodule R L L)
⊢ IsSolvable.{v} ↥(radical R L)
have refine_1 : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} ⊥
Tactic: refine hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact.{v} (LieSubmodule R L L)
refine_1 : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} ⊥
⊢ IsSolvable.{v} ↥(radical R L)
have refine_2 : ∀ (I : LieSubmodule R L L)
  (hI : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} I)
  (J : LieSubmodule R L L)
  (hJ : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} J),
  Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} (I ⊔ J)
Tactic: refine hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst_5 : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact.{v} (LieSubmodule R L L)
I : LieSubmodule R L L
hI : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} I
J : LieSubmodule R L L
hJ : Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} J
⊢ Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} (I ⊔ J)
have refine_2 : ∀ (hI : IsSolvable.{v} ↥I) (J : LieSubmodule R L L) (hJ : IsSolvable.{v} ↥J), IsSolvable.{v} ↥(I ⊔ J)
Tactic: rw [Set.mem_setOf_eq] at hI hJ ⊢
Cleared hypotheses: hI, J, 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
inst_3 : IsSolvable L
⊢ Eq (α := LieIdeal R L) (radical R L) ⊤
have rw : LE.le (α := LieIdeal R L) ⊤ (radical R L)
Tactic: rw [eq_top_iff]
-- 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
inst_3 : IsSolvable L
⊢ LE.le (α := LieIdeal R L) ⊤ (radical R L)
have h : IsSolvable.{v} ↥⊤
Tactic: have h : IsSolvable (⊤ : LieSubalgebra R L) := inferInstance
-- 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 : ℕ
⊢ derivedLengthOfIdeal R L I = k + 1 ↔
    IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
have rw : derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
Tactic: rw [abelian_iff_derived_succ_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 : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
have change : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
Tactic: change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
-- 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 : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ k₂ ∈ s
have suffices : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
Tactic: suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
-- 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 : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ derivedSeriesOfIdeal R L k₂ I ≤ ⊥
have h₂ : derivedSeriesOfIdeal R L k₁ I = ⊥
Tactic: change derivedSeriesOfIdeal R L k₁ I = ⊥ 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
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : derivedSeriesOfIdeal R L k₁ I = ⊥
⊢ derivedSeriesOfIdeal R L k₂ I ≤ ⊥
have rw : derivedSeriesOfIdeal R L k₂ I ≤ derivedSeriesOfIdeal R L k₁ I
Tactic: rw [← 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 : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
Tactic: have hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := by
    intro k₁ k₂ h₁₂ h₁
    suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
    change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁; rw [← h₁]
    exact derivedSeriesOfIdeal_antitone I 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 : LieIdeal R L
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLength.{u, v} R ↥I = derivedLengthOfIdeal R L I
have change : sInf s₁ = sInf s₂
Tactic: change sInf s₁ = sInf s₂
-- 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
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s₁ = sInf s₂
have e_a : s₁ = s₂
Tactic: congr
-- 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
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s₁ = s₂
have e_a : ∀ (k : ℕ), k ∈ s₁ ↔ k ∈ s₂
Tactic: ext 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
⊢ IsLieAbelian.{v} ↥(derivedAbelianOfIdeal I)
have dsimp : IsLieAbelian.{v}
  ↥(match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I :
      LieIdeal R L)
Tactic: dsimp +instances only [derivedAbelianOfIdeal]