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
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) ⊥
apply : LieIdeal.map f (derivedSeries R L' k) = ⊥
⊢ Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥

Tactic:
apply LieIdeal.bot_of_map_eq_bot h

Premises used: LieIdeal.bot_of_map_eq_bot
-- 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
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) ⊥
rw : LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥

Tactic:
rw [eq_bot_iff, ← hk]

Premises used: eq_bot_iff
-- 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
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) ≤ derivedSeries R L k

Tactic:
apply LieIdeal.derivedSeries_map_le

Premises used: LieIdeal.derivedSeries_map_le
-- Module: Mathlib.Algebra.Lie.Solvable
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 : LieIdeal R L
inst_5 : IsSolvable L
⊢ IsSolvable.{v} ↥A

Tactic:
A.incl_injective.lieAlgebra_isSolvable

Premises used: LieIdeal.incl_injective, Function.Injective.lieAlgebra_isSolvable
-- 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
hL' : IsSolvable L'
h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
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) ⊥
⊢ IsSolvable L

Tactic:
rw [isSolvable_iff R] at hL' ⊢

Premises used: LieAlgebra.isSolvable_iff
-- 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
hL' : ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
h : Surjective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
apply : ∀ (a : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' a) ⊥ → Eq (α := LieIdeal R L) (derivedSeries R L a) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
apply hL'.imp

Premises used: Exists.imp
-- 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
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) ⊥
rw : LieIdeal.map f ⊥ = ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
rw [← LieIdeal.derivedSeries_map_eq k h, hk]

Premises used: LieIdeal.derivedSeries_map_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
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) ⊥
⊢ LieIdeal.map f ⊥ = ⊥

Tactic:
simp only [LieIdeal.map_eq_bot_iff, bot_le]

Premises used: bot_le, LieIdeal.map_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
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_1 f : L' →ₗ⁅R⁆ L
inst_5 : LieAlgebra.IsSolvable L'
⊢ LieAlgebra.IsSolvable.{v} ↥f.range

Tactic:
f.surjective_rangeRestrict.lieAlgebra_isSolvable

Premises used: LieHom.surjective_rangeRestrict, Function.Surjective.lieAlgebra_isSolvable
-- 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'
e : L' ≃ₗ⁅R⁆ L
mp : IsSolvable L' → IsSolvable L
mpr : IsSolvable L → IsSolvable L'
⊢ IsSolvable L' ↔ IsSolvable L

Tactic:
constructor
-- 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'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L

Tactic:
e.symm.injective.lieAlgebra_isSolvable

Premises used: LieEquiv.injective, Function.Injective.lieAlgebra_isSolvable, LieEquiv.symm
-- 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'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L

Tactic:
exact e.symm.injective.lieAlgebra_isSolvable

Premises used: LieEquiv.injective, Function.Injective.lieAlgebra_isSolvable, LieEquiv.symm
-- 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'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Tactic:
e.injective.lieAlgebra_isSolvable

Premises used: LieEquiv.injective, Function.Injective.lieAlgebra_isSolvable
-- 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'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Tactic:
exact e.injective.lieAlgebra_isSolvable

Premises used: LieEquiv.injective, Function.Injective.lieAlgebra_isSolvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h : IsSolvable.{v} ↥J
⊢ IsSolvable.{v} ↥I

Tactic:
(LieIdeal.inclusion_injective h₁).lieAlgebra_isSolvable

Premises used: LieIdeal.inclusion_injective, Function.Injective.lieAlgebra_isSolvable
-- Module: Mathlib.Algebra.Lie.Solvable
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
h : Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L 1) ⊥
⊢ IsSolvable L

Tactic:
use 1
-- Module: Mathlib.Algebra.Lie.Solvable
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 h : IsLieAbelian L
⊢ Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L 1) ⊥

Tactic:
rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv]

Premises used: LieIdeal.topEquiv, lie_abelian_iff_equiv_lie_abelian, LieAlgebra.abelian_iff_derived_one_eq_bot
-- Module: Mathlib.Algebra.Lie.Solvable
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
⊢ IsLieAbelian L

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Solvable
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
⊢ WellFoundedGT.{v} (LieSubmodule R L L)

Tactic:
have hwf := LieSubmodule.wellFoundedGT_of_noetherian R L L
-- Module: Mathlib.Algebra.Lie.Solvable
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)
⊢ CompleteLattice.IsSupClosedCompact.{v} (LieSubmodule R L L)

Tactic:
rw [← CompleteLattice.isSupClosedCompact_iff_wellFoundedGT] at hwf

Premises used: CompleteLattice.isSupClosedCompact_iff_wellFoundedGT
-- Module: Mathlib.Algebra.Lie.Solvable
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)

Tactic:
hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_

Premises used: Set.Mem, setOf, Membership.mem, Subtype, Bot.bot, LieAlgebra.IsSolvable, Exists.intro, LieAlgebra.radical
-- Module: Mathlib.Algebra.Lie.Solvable
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} ⊥
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)
⊢ IsSolvable.{v} ↥(radical R L)

Tactic:
refine hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_

Premises used: setOf, Membership.mem, Subtype, Bot.bot, LieAlgebra.IsSolvable, Exists.intro
-- Module: Mathlib.Algebra.Lie.Solvable
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)
⊢ Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} ⊥

Tactic:
LieAlgebra.isSolvableBot R L

Premises used: Set.Mem, setOf, LieAlgebra.isSolvableBot
-- Module: Mathlib.Algebra.Lie.Solvable
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)
⊢ Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} ⊥

Tactic:
exact LieAlgebra.isSolvableBot R L

Premises used: LieAlgebra.isSolvableBot
-- Module: Mathlib.Algebra.Lie.Solvable
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
refine_2 : ∀ (hI : IsSolvable.{v} ↥I) (J : LieSubmodule R L L) (hJ : IsSolvable.{v} ↥J), IsSolvable.{v} ↥(I ⊔ J)
⊢ Membership.mem (γ := Set (LieSubmodule R L L)) {I : LieIdeal R L | IsSolvable.{v} ↥I} (I ⊔ J)

Tactic:
rw [Set.mem_setOf_eq] at hI hJ ⊢

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Lie.Solvable
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 : IsSolvable.{v} ↥I
J : LieSubmodule R L L
hJ : IsSolvable.{v} ↥J
⊢ IsSolvable.{v} ↥(I ⊔ J)

Tactic:
apply LieAlgebra.isSolvableAdd R L

Premises used: LieAlgebra.isSolvableAdd
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
I : LieIdeal R L
⊢ IsSolvable.{v} ↥I ↔ I ≤ radical R L

Tactic:
⟨fun h => le_sSup h, fun h => le_solvable_ideal_solvable h inferInstance⟩

Premises used: LieAlgebra.le_solvable_ideal_solvable, inferInstance, Iff.intro, le_sSup
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LE.le (α := LieIdeal R L) (center R L) (radical R L)

Tactic:
have h : IsSolvable (center R L) := inferInstance
  le_sSup h

Premises used: Set.Mem, inferInstance, le_sSup
-- Module: Mathlib.Algebra.Lie.Solvable
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 rwa rwa₁ rwa₂ rwa₃ : IsSolvable L
⊢ IsSolvable.{v} ↥⊤

Tactic:
rwa [solvable_iff_equiv_solvable LieSubalgebra.topEquiv]

Premises used: LieSubalgebra.topEquiv, LieAlgebra.solvable_iff_equiv_solvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
rw : LE.le (α := LieIdeal R L) ⊤ (radical R L)
⊢ Eq (α := LieIdeal R L) (radical R L) ⊤

Tactic:
rw [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
inst_3 : IsSolvable L
⊢ IsSolvable.{v} ↥⊤

Tactic:
have h : IsSolvable (⊤ : LieSubalgebra R L) := inferInstance
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
h : IsSolvable.{v} ↥⊤
⊢ LE.le (α := LieIdeal R L) ⊤ (radical R L)

Tactic:
le_sSup h

Premises used: Set.Mem, le_sSup
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
h : IsSolvable.{v} ↥⊤
⊢ LE.le (α := LieIdeal R L) ⊤ (radical R L)

Tactic:
exact le_sSup h
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
rw : derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ derivedLengthOfIdeal R L I = k + 1 ↔
    IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
rw [abelian_iff_derived_succ_eq_bot]

Premises used: LieAlgebra.abelian_iff_derived_succ_eq_bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
change : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Premises used: InfSet.sInf
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
this : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
⊢ k₂ ∈ s

Tactic:
eq_bot_iff.mpr this

Premises used: Iff.mpr, Set.Mem, setOf, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
this : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
⊢ k₂ ∈ s

Tactic:
exact eq_bot_iff.mpr this

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
suffices : derivedSeriesOfIdeal R L k₂ I ≤ ⊥
⊢ k₂ ∈ s

Tactic:
suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ∈ s
⊢ derivedSeriesOfIdeal R L k₁ I = ⊥

Tactic:
change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁

Premises used: LieAlgebra.derivedSeriesOfIdeal
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : derivedSeriesOfIdeal R L k₁ I = ⊥
rw : derivedSeriesOfIdeal R L k₂ I ≤ derivedSeriesOfIdeal R L k₁ I
⊢ derivedSeriesOfIdeal R L k₂ I ≤ ⊥

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
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 ≤ derivedSeriesOfIdeal R L k₁ I

Tactic:
derivedSeriesOfIdeal_antitone I h₁₂

Premises used: LieAlgebra.derivedSeriesOfIdeal_antitone
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : derivedSeriesOfIdeal R L k₁ I = ⊥
⊢ derivedSeriesOfIdeal R L k₂ I ≤ derivedSeriesOfIdeal R L k₁ I

Tactic:
exact derivedSeriesOfIdeal_antitone I h₁₂

Premises used: LieAlgebra.derivedSeriesOfIdeal_antitone
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ ∀ (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₁₂
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
Nat.sInf_upward_closed_eq_succ_iff hs k

Premises used: Nat.sInf_upward_closed_eq_succ_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
exact Nat.sInf_upward_closed_eq_succ_iff hs k

Premises used: Nat.sInf_upward_closed_eq_succ_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
change : sInf s₁ = sInf s₂
⊢ derivedLength.{u, v} R ↥I = derivedLengthOfIdeal R L I

Tactic:
change sInf s₁ = sInf s₂

Premises used: InfSet.sInf
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
e_a : s₁ = s₂
⊢ sInf s₁ = sInf s₂

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
e_a : ∀ (k : ℕ), k ∈ s₁ ↔ k ∈ s₂
⊢ s₁ = s₂

Tactic:
ext k
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k : ℕ | Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥}
s₂ : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂

Tactic:
I.derivedSeries_eq_bot_iff k

Premises used: Set.Mem, setOf, LieIdeal.derivedSeries_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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 = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂

Tactic:
exact I.derivedSeries_eq_bot_iff k

Premises used: LieIdeal.derivedSeries_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
dsimp :
  IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
⊢ IsLieAbelian.{v} ↥(derivedAbelianOfIdeal I)

Tactic:
dsimp +instances only [derivedAbelianOfIdeal]

Premises used: LieAlgebra.derivedAbelianOfIdeal
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
zero :
  ∀ (h : derivedLengthOfIdeal R L I = 0),
    IsLieAbelian.{v}
      ↥(match (motive := ℕ → LieIdeal R L) 0 with
          | 0 => ⊥
          | k.succ => derivedSeriesOfIdeal R L k I :
          LieIdeal R L)
succ :
  ∀ (k : ℕ) (h : derivedLengthOfIdeal R L I = k + 1),
    IsLieAbelian.{v}
      ↥(match (motive := ℕ → LieIdeal R L) k + 1 with
          | 0 => ⊥
          | k.succ => derivedSeriesOfIdeal R L k I :
          LieIdeal R L)
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)

Tactic:
rcases h : derivedLengthOfIdeal R L I with - | k

Premises used: LieAlgebra.derivedLengthOfIdeal
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian.{v} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
rw [derivedSeries_of_derivedLength_succ] at h

Premises used: LieAlgebra.derivedSeries_of_derivedLength_succ