awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
⊢ 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
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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))
⊢ 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
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
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))
⊢ _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)

Tactic:
rw [← IsNilpotent.map_iff hbc_inj, aux, ← toEnd_baseChange]

Premises used: LieModule.toEnd_baseChange, IsNilpotent.map_iff
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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 (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:
nilp_ext ⟨_, hx_ext⟩

Premises used: Subtype.mk, TensorProduct.tmul
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
h :
  ∀ x ∈ I,
    ∀ y ∈ ⁅I, I⁆,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ let DI := ⁅I, I⁆;
  ∀ 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)

Tactic:
set DI : LieIdeal R L := ⁅I, I⁆

Premises used: LieIdeal
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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⁆
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)
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥DI) (LieModule.traceForm R (↥DI) L) 0

Tactic:
ext ⟨x, hx⟩ ⟨y, hy⟩
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
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)
⊢ 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:
change killingForm R L x y = 0

Premises used: killingForm, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
h x (LieSubmodule.lie_le_left I I hx) y hy

Premises used: LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
exact h x (LieSubmodule.lie_le_left I I hx) y hy

Premises used: LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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

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
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
⊢ 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
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
rw :
  ∀ (x : ↥DDI),
    IsNilpotent (R := Module.End R ↥DDI) ((ad R ↥DDI : (a : ↥DDI) → Module.End R ↥DDI) x : Module.End R ↥DDI)
⊢ LieRing.IsNilpotent.{u_2} ↥DDI

Tactic:
rw [LieAlgebra.isNilpotent_iff_forall (R := R)]

Premises used: LieAlgebra.isNilpotent_iff_forall
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
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)
⊢ 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)

Tactic:
apply LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad (DDI : LieSubalgebra R L) (x := ⟨x, hx⟩)

Premises used: LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, LieIdeal.toLieSubalgebra
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)

Tactic:
(LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩

Premises used: Subtype.mk, Iff.mp, LieModule.isNilpotent_iff_forall', LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
refine : Membership.mem (γ := LieIdeal R ↥DI) (derivedSeries R (↥DI) 1) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯)
⊢ 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:
refine (LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩

Premises used: Subtype.mk, Iff.mp, LieModule.isNilpotent_iff_forall', LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (α := L) (derivedSeriesOfIdeal R L 1 DI)
    ((DI.incl : (a : ↥DI) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯) : L)
⊢ Membership.mem (γ := LieIdeal R ↥DI) (derivedSeries R (↥DI) 1) (Subtype.mk (p := fun (x : L) ↦ x ∈ DI) x ⋯)

Tactic:
rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]

Premises used: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, LieIdeal.mem_comap
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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

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]
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
obtain : ∀ (k : ℕ) (hk : Eq.{u_2 + 1} (α := LieIdeal R ↥DDI) (derivedSeries R (↥DDI) k) ⊥), IsSolvable.{u_2} ↥I
⊢ IsSolvable.{u_2} ↥I

Tactic:
obtain ⟨k, hk⟩ := IsSolvable.solvable R DDI

Premises used: Membership.mem, Subtype, LieAlgebra.IsSolvable.solvable
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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) ⊥
⊢ derivedSeriesOfIdeal R L k DDI = ⊥

Tactic:
rw [derivedSeries_eq_bot_iff] at hk

Premises used: LieIdeal.derivedSeries_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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

Tactic:
IsSolvable.mk (k := k + 2) ((derivedSeries_eq_bot_iff I (k + 2)).mpr ?_)

Premises used: Iff.mpr, LieAlgebra.IsSolvable.mk, LieIdeal.derivedSeries_eq_bot_iff, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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 = ⊥
refine : derivedSeriesOfIdeal R L (k + 2) I = ⊥
⊢ IsSolvable.{u_2} ↥I

Tactic:
refine IsSolvable.mk (k := k + 2) ((derivedSeries_eq_bot_iff I (k + 2)).mpr ?_)

Premises used: Iff.mpr, LieAlgebra.IsSolvable.mk, LieIdeal.derivedSeries_eq_bot_iff, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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⁆ = ⊥
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⁆⁆ =
    ⊥
rwa₃ rwa₄ rwa₅ rwa₆ : derivedSeriesOfIdeal R L k ⁅⁅I, I⁆, ⁅I, I⁆⁆ = ⊥
⊢ derivedSeriesOfIdeal R L (k + 2) I = ⊥

Tactic:
rwa [derivedSeriesOfIdeal_add, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ,
    derivedSeriesOfIdeal_zero]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeriesOfIdeal_add, LieAlgebra.derivedSeriesOfIdeal_zero