awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
    _root_.IsNilpotent (R := End A (A ⊗[R] M))
      ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
          x :
        End A (A ⊗[R] M))
x : L
hx : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
hx_ext : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)
⊢ _root_.IsNilpotent.{u_3} (R := End R M)
    ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx) :
      End R M)
have hbc_inj : Injective (α := End R M) (β := End A (A ⊗[R] M)) (⇑(End.baseChangeHom R A M) : (a : End R M) → End A (A ⊗[R] M))
Tactic: have hbc_inj : Injective (End.baseChangeHom R A M) := LinearMap.baseChangeHom_injective R M A
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
    _root_.IsNilpotent (R := End A (A ⊗[R] M))
      ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
          x :
        End A (A ⊗[R] M))
x : L
hx : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
hx_ext : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)
hbc_inj :
  Injective (α := End R M) (β := End A (A ⊗[R] M)) (⇑(End.baseChangeHom R A M) : (a : End R M) → End A (A ⊗[R] M))
⊢ _root_.IsNilpotent.{u_3} (R := End R M)
    ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx) :
      End R M)
have aux : Eq (α := End A (A ⊗[R] M))
  ((End.baseChangeHom R A M : (a : End R M) → End A (A ⊗[R] M))
      ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx)) :
    End A (A ⊗[R] M))
  (baseChange A (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) x) :
    A ⊗[R] M →ₗ[A] A ⊗[R] M)
Tactic: have aux : (toEnd R (derivedSeries R L 1) M ⟨x, hx⟩).baseChangeHom R A M =
      (toEnd R L M x).baseChange A := rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
    _root_.IsNilpotent (R := End A (A ⊗[R] M))
      ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
          x :
        End A (A ⊗[R] M))
x : L
hx : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
hx_ext : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)
hbc_inj :
  Injective (α := End R M) (β := End A (A ⊗[R] M)) (⇑(End.baseChangeHom R A M) : (a : End R M) → End A (A ⊗[R] M))
aux :
  Eq (α := End A (A ⊗[R] M))
    ((End.baseChangeHom R A M : (a : End R M) → End A (A ⊗[R] M))
        ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx)) :
      End A (A ⊗[R] M))
    (baseChange A (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) x) :
      A ⊗[R] M →ₗ[A] A ⊗[R] M)
⊢ _root_.IsNilpotent.{u_3} (R := End R M)
    ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx) :
      End R M)
have rw : _root_.IsNilpotent (R := End A (A ⊗[R] M))
  ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x) : End A (A ⊗[R] M))
Tactic: rw [← IsNilpotent.map_iff hbc_inj, aux, ← toEnd_baseChange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
have H : ∀ (x : L) (hx : x ∈ DI) (y : L) (hy : y ∈ DI),
  Eq.{u_1 + 1} (α := R)
    ((((LieModule.traceForm R (↥DI) L : (a : ↥DI) → ↥DI →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x hx) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥DI) R) :
          (a : ↥DI) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) y hy) :
      R)
    ((((0 : (a : ↥DI) → ↥DI →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x hx) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥DI) R) :
          (a : ↥DI) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) y hy) :
      R)
Tactic: ext ⟨x, hx⟩ ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
x : L
hx : x ∈ DI
y : L
hy : y ∈ DI
⊢ Eq.{u_1 + 1} (α := R)
    ((((LieModule.traceForm R (↥DI) L : (a : ↥DI) → ↥DI →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x hx) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥DI) R) :
          (a : ↥DI) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) y hy) :
      R)
    ((((0 : (a : ↥DI) → ↥DI →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x hx) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥DI) R) :
          (a : ↥DI) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) y hy) :
      R)
have H : Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: change killingForm R L x y = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
⊢ IsSolvable.{u_2} ↥I
have tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
Tactic: have tf_eq_zero : LieModule.traceForm R DI L = 0 := by
    ext ⟨x, hx⟩ ⟨y, hy⟩
    change killingForm R L x y = 0
    exact h x (LieSubmodule.lie_le_left I I hx) y hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
⊢ IsSolvable.{u_2} ↥I
have module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
Tactic: have module_nilp : LieModule.IsNilpotent (derivedSeries R DI 1) L :=
    LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero tf_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
⊢ LieRing.IsNilpotent.{u_2} ↥DDI
have rw : ∀ (x : ↥DDI), IsNilpotent (R := Module.End R ↥DDI) ((ad R ↥DDI : (a : ↥DDI) → Module.End R ↥DDI) x : Module.End R ↥DDI)
Tactic: rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ IsNilpotent (R := Module.End R ↥DDI)
    ((ad R ↥DDI : (a : ↥DDI) → Module.End R ↥DDI) (Subtype.mk (p := fun (x : L) ↦ x ∈ DDI) x hx) : Module.End R ↥DDI)
have apply : IsNilpotent (R := Module.End R L)
  ((ad R L : (a : L) → Module.End R L) (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ toLieSubalgebra R L DDI) x hx) : L) :
    Module.End R L)
Tactic: apply LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad (DDI : LieSubalgebra R L) (x := ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ IsNilpotent (R := Module.End R L)
    ((ad R L : (a : L) → Module.End R L) (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ toLieSubalgebra R L DDI) x hx) : L) :
      Module.End R L)
have refine : Membership.mem (γ := LieIdeal R ↥DI) (derivedSeries R (↥DI) 1) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x sorry)
Tactic: refine (LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ Membership.mem (γ := LieIdeal R ↥DI) (derivedSeries R (↥DI) 1) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯)
have rwa : Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x sorry ∈ comap DI.incl (derivedSeriesOfIdeal R L 1 DI)
Tactic: rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
rwa : Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯ ∈ comap DI.incl (derivedSeriesOfIdeal R L 1 DI)
⊢ Membership.mem (γ := LieIdeal R ↥DI) (derivedSeries R (↥DI) 1) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯)
have rwa₁ : Membership.mem (α := L) (derivedSeriesOfIdeal R L 1 DI)
  ((DI.incl : (a : ↥DI) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x sorry) : L)
Tactic: rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
⊢ IsSolvable.{u_2} ↥I
have ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
Tactic: have ring_nilp : LieRing.IsNilpotent DDI := by
    rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
    rintro ⟨x, hx⟩
    apply LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad (DDI : LieSubalgebra R L) (x := ⟨x, hx⟩)
    refine (LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩
    rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
⊢ IsSolvable.{u_2} ↥I
have obtain : ∀ (k : ℕ) (hk : Eq.{u_2 + 1} (α := LieIdeal R ↥DDI) (derivedSeries R (↥DDI) k) ⊥), IsSolvable.{u_2} ↥I
Tactic: obtain ⟨k, hk⟩ := IsSolvable.solvable R DDI
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
k : ℕ
hk : Eq.{u_2 + 1} (α := LieIdeal R ↥DDI) (derivedSeries R (↥DDI) k) ⊥
⊢ IsSolvable.{u_2} ↥I
have hk₁ : derivedSeriesOfIdeal R L k DDI = ⊥
Tactic: rw [derivedSeries_eq_bot_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
k : ℕ
hk : derivedSeriesOfIdeal R L k DDI = ⊥
⊢ IsSolvable.{u_2} ↥I
have refine : derivedSeriesOfIdeal R L (k + 2) I = ⊥
Tactic: refine IsSolvable.mk (k := k + 2) ((derivedSeries_eq_bot_iff I (k + 2)).mpr ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
k : ℕ
hk : derivedSeriesOfIdeal R L k DDI = ⊥
⊢ derivedSeriesOfIdeal R L (k + 2) I = ⊥
have rwa : derivedSeriesOfIdeal R L k (derivedSeriesOfIdeal R L 2 I) = ⊥
Tactic: rwa [derivedSeriesOfIdeal_add, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ,
    derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
k : ℕ
hk : derivedSeriesOfIdeal R L k DDI = ⊥
rwa : derivedSeriesOfIdeal R L k (derivedSeriesOfIdeal R L 2 I) = ⊥
⊢ derivedSeriesOfIdeal R L (k + 2) I = ⊥
have rwa₁ : derivedSeriesOfIdeal R L k ⁅derivedSeriesOfIdeal R L 1 I, derivedSeriesOfIdeal R L 1 I⁆ = ⊥
Tactic: rwa [derivedSeriesOfIdeal_add, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ,
    derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h :
  ∀ x ∈ I,
    ∀ y ∈ DI,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
ring_nilp : LieRing.IsNilpotent.{u_2} ↥DDI
k : ℕ
hk : derivedSeriesOfIdeal R L k DDI = ⊥
rwa : derivedSeriesOfIdeal R L k (derivedSeriesOfIdeal R L 2 I) = ⊥
rwa₁ : derivedSeriesOfIdeal R L k ⁅derivedSeriesOfIdeal R L 1 I, derivedSeriesOfIdeal R L 1 I⁆ = ⊥
⊢ derivedSeriesOfIdeal R L (k + 2) I = ⊥
have rwa₂ : derivedSeriesOfIdeal R L k
    ⁅⁅derivedSeriesOfIdeal R L 0 I, derivedSeriesOfIdeal R L 0 I⁆,
      ⁅derivedSeriesOfIdeal R L 0 I, derivedSeriesOfIdeal R L 0 I⁆⁆ =
  ⊥
Tactic: rwa [derivedSeriesOfIdeal_add, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ,
    derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
this : IsSolvable.{u_2} ↥⊤
⊢ IsSolvable L
have rwa : IsSolvable.{u_2} ↥⊤
Tactic: rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ IsSolvable L
have suffices : IsSolvable.{u_2} ↥⊤
Tactic: suffices IsSolvable (⊤ : LieIdeal R L) by
    rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ IsSolvable.{u_2} ↥⊤
have h₁ : ∀ (x : L),
  Membership.mem (γ := LieIdeal R L) ⊤ x →
    ∀ (y : L),
      Membership.mem (γ := LieIdeal R L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) y →
        Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: apply LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
⊢ LE.le (α := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (radical R L)
have rw : IsSolvable.{u_2} ↥(LieIdeal.killingCompl R L ⊤)
Tactic: rw [← LieIdeal.solvable_iff_le_radical]