awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have obtain : ∀ (χ : Dual.{u_1, u_2} k ↥(radical k L)) (hχ : Nontrivial.{u_3} ↥(weightSpace M (⇑χ : (a : ↥(radical k L)) → k))),
  HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
Tactic: obtain ⟨χ, hχ⟩ : ∃ χ : Module.Dual k (radical k L), Nontrivial (weightSpace M χ) :=
    exists_nontrivial_weightSpace_of_isSolvable k (radical k L) M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
hχ : Nontrivial.{u_3} ↥(weightSpace M (⇑χ : (a : ↥(radical k L)) → k))
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have hχ₁ : Nontrivial.{u_3} ↥N
Tactic: replace hχ : Nontrivial N := hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ : Nontrivial.{u_3} ↥N
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have hχ₁ : N = ⊤
Tactic: replace hχ : N = ⊤ := N.eq_top_of_isIrreducible k L M
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
⊢ ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
      ((χ : (a : ↥(radical k L)) → k)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
        k)
      LinearMap.id
have h : ∀ (m : M),
  Eq (α := M)
    (((((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) : (a : M) → M) m : M)
    ((HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
            ((χ : (a : ↥(radical k L)) → k)
                (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
              k)
            LinearMap.id :
          (a : M) → M)
        m :
      M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
m : M
⊢ Eq (α := M)
    (((((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) : (a : M) → M) m : M)
    ((HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
            ((χ : (a : ↥(radical k L)) → k)
                (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
              k)
            LinearMap.id :
          (a : M) → M)
        m :
      M)
have hm : ∀ (y : L) (hy : Membership.mem (γ := LieIdeal k L) (radical k L) y),
  ⁅y, m⁆ =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k)
      ((χ : (a : ↥(radical k L)) → k)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) y hy) :
        k)
      m
Tactic: have hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m := by
      simpa [N, weightSpaceOfIsLieTower, mem_weightSpace] using (hχ ▸ mem_top _ : m ∈ N)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ : N = ⊤
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have hχ₁ : ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
  ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
      ((χ : (a : ↥(radical k L)) → k)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
        k)
      LinearMap.id
Tactic: replace hχ (x : L) (hx : x ∈ radical k L) : toEnd k _ M x = χ ⟨x, hx⟩ • LinearMap.id := by
    ext m
    have hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m := by
      simpa [N, weightSpaceOfIsLieTower, mem_weightSpace] using (hχ ▸ mem_top _ : m ∈ N)
    simpa using hm x hx
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
⊢ Eq (α := LieIdeal k L) (radical k L) (center k L)
have refine : ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule k L L) (radical k L) x) (x_1 : L), ⁅x_1, x⁆ = 0
Tactic: refine le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
Tactic: have aux : radical k L = center k L := by
    refine le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)
    intro y
    simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), LieHom.map_lie, hχ _ hx, lie_smul,
      (toEnd k L M y).commute_id_right.lie_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have refine_1 : ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (center k L) x),
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
Tactic: refine ⟨⟨aux⟩, fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ (mem_maxTrivSubmodule k L L x).mpr fun y ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (center k L) x),
    Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
      (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have refine_2 : ∀ (x : L)
  (hx :
    Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
      (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M))
  (y : L), ⁅y, x⁆ = 0
Tactic: refine ⟨⟨aux⟩, fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ (mem_maxTrivSubmodule k L L x).mpr fun y ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx : Membership.mem (γ := LieIdeal k L) (center k L) x
⊢ Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have hx₁ : Membership.mem (γ := LieIdeal k L) (radical k L) x
Tactic: rw [← aux] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
y : L
⊢ ⁅y, x⁆ = 0
have refine_2 : ∀ (t : k)
  (ht :
    HSMul.hSMul (β := End k M) t LinearMap.id =
      ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x),
  ⁅y, x⁆ = 0
Tactic: obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
⊢ HasTrivialRadical k L
have this : finrank k M ≠ 0
Tactic: have : finrank k M ≠ 0 := (finrank_pos_iff.mpr <| nontrivial_of_isIrreducible k L M).ne'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
⊢ HasTrivialRadical k L
have _i : HasCentralRadical k L
Tactic: obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
⊢ HasTrivialRadical k L
have h' : ∀ (x : L),
  Membership.mem (γ := LieIdeal k L) (center k L) x ↔
    Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
      (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
Tactic: obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
⊢ HasTrivialRadical k L
have rw : ∀ (m : L), Membership.mem (γ := LieSubmodule k L L) (center k L) m → m = 0
Tactic: rw [hasTrivialRadical_iff, (hasCentralRadical_iff k L).mp inferInstance, LieSubmodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (center k L) x
⊢ x = 0
have h₁ : Eq.{u_1 + 1} (α := k)
  ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
      (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
    k)
  (0 : k)
Tactic: specialize h x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (center k L) x
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
⊢ x = 0
have hx₁ : Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
  (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
Tactic: rw [h' x] at hx
Cleared hypotheses: hx, h