awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : J ⊓ I = ⊥
a : ⁅(↑j : L), y + z⁆ ∈ ⁅J, I⁆
⊢ ⁅(↑j : L), y + z⁆ ∈ J ⊓ I

Tactic:
apply LieSubmodule.lie_le_inf

Premises used: LieSubmodule.lie_le_inf
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : J ⊓ I = ⊥
⊢ ⁅(↑j : L), y + z⁆ ∈ ⁅J, I⁆

Tactic:
LieSubmodule.lie_mem_lie j.2 hx

Premises used: Set.Mem, LieSubmodule.lie_mem_lie, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : J ⊓ I = ⊥
⊢ ⁅(↑j : L), y + z⁆ ∈ ⁅J, I⁆

Tactic:
exact LieSubmodule.lie_mem_lie j.2 hx

Premises used: LieSubmodule.lie_mem_lie, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
inr : J ⊓ I = ⊥
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆

Tactic:
suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
inr : ¬J ⊓ I = J
apply : J ⊓ I ≤ J
⊢ J ⊓ I = ⊥

Tactic:
apply ((hs hJs).le_iff.mp _).resolve_right

Premises used: IsAtom.le_iff, Iff.mp, Or.resolve_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
inr : ∀ (hJI : J ⊓ I = J), J ≤ I
⊢ ¬J ⊓ I = J

Tactic:
contrapose hJI
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
hJI : J ⊓ I = J
inr : J ⊓ I ≤ I
⊢ J ≤ I

Tactic:
rw [← hJI]
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
hJI : J ⊓ I = J
⊢ J ⊓ I ≤ I

Tactic:
inf_le_right

Premises used: Set.Mem, inf_le_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
hJI : J ⊓ I = J
⊢ J ⊓ I ≤ I

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ J ⊓ I ≤ J

Tactic:
inf_le_left

Premises used: Set.Mem, inf_le_left
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ J ⊓ I ≤ J

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
rw : ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
⊢ HasTrivialRadical R L

Tactic:
rw [hasTrivialRadical_iff_no_abelian_ideals]

Premises used: LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
apply : ¬∃ (a : LieIdeal R L), IsAtom a ∧ a ≤ I
⊢ I = ⊥

Tactic:
apply (eq_bot_or_exists_atom_le I).resolve_right

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Or.resolve_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
apply : IsLieAbelian.{u_2} ↥J
⊢ False

Tactic:
apply IsSemisimple.non_abelian_of_isAtom J hJ

Premises used: LieAlgebra.IsSemisimple.non_abelian_of_isAtom
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
trivial : ∀ (x m : ↥J), ⁅x, m⁆ = 0
⊢ IsLieAbelian.{u_2} ↥J

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
trivial : (↑⁅x, y⁆ : L) = (↑0 : L)
⊢ ⁅x, y⁆ = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
trivial : ⁅(↑x : L), (↑y : L)⁆ = 0
⊢ (↑⁅x, y⁆ : L) = (↑0 : L)

Tactic:
simp only [LieIdeal.coe_bracket_of_module, LieSubmodule.coe_bracket, ZeroMemClass.coe_zero]

Premises used: LieIdeal.coe_bracket_of_module, ZeroMemClass.coe_zero, LieSubmodule.coe_bracket
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) ⋯, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) ⋯⁆ = 0

Tactic:
have : (⁅(⟨x, hJ' x.2⟩ : I), ⟨y, hJ' y.2⟩⁆ : I) = 0 := trivial_lie_zero _ _ _ _
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) ⋯, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) ⋯⁆ = 0
⊢ (↑⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) ⋯, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) ⋯⁆ : L) = (↑0 : L)

Tactic:
apply_fun Subtype.val at this

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this :
  (↑⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) ⋯, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) ⋯⁆ : L) = (↑0 : L)
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0

Tactic:
this
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this :
  (↑⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) ⋯, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) ⋯⁆ : L) = (↑0 : L)
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0

Tactic:
exact this
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
sSup_atoms_eq_top : Eq.{u_2 + 1} (α := LieIdeal R L) (sSup {I : LieIdeal R L | IsAtom I}) ⊤
sSupIndep_isAtom : sSupIndep.{u_2} (α := LieIdeal R L) {I : LieIdeal R L | IsAtom I}
non_abelian_of_isAtom : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
⊢ IsSemisimple R L

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ Eq.{u_2 + 1} (α := LieIdeal R L) (sSup {I : LieIdeal R L | IsAtom I}) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ sSupIndep.{u_2} (α := LieIdeal R L) {I : LieIdeal R L | IsAtom I}

Tactic:
simpa using sSupIndep_singleton _

Premises used: sSupIndep_singleton
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : IsAtom I
hI₂ : IsLieAbelian.{u_2} ↥I
non_abelian_of_isAtom : IsLieAbelian L
⊢ False

Tactic:
apply IsSimple.non_abelian (R := R) (L := L)

Premises used: LieAlgebra.IsSimple.non_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : IsAtom I
hI₂ : IsLieAbelian.{u_2} ↥I
⊢ I = ⊤

Tactic:
rw [IsSimple.isAtom_iff_eq_top] at hI₁

Premises used: LieAlgebra.IsSimple.isAtom_iff_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : IsAtom I
hI₂ : IsLieAbelian.{u_2} ↥I
hI₃ : I = ⊤
⊢ IsLieAbelian.{u_2} ↥I

Tactic:
rw [IsSimple.isAtom_iff_eq_top] at hI₁

Premises used: LieAlgebra.IsSimple.isAtom_iff_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian.{u_2} ↥I
non_abelian_of_isAtom : ∀ (hI₂ : IsLieAbelian.{u_2} ↥⊤), IsLieAbelian L
non_abelian_of_isAtom₁ non_abelian_of_isAtom₂ non_abelian_of_isAtom₃ non_abelian_of_isAtom₄ :
  ∀ (hI₂ : IsLieAbelian L), IsLieAbelian L
⊢ IsLieAbelian L

Tactic:
rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂

Premises used: LieIdeal.topEquiv, lie_abelian_iff_equiv_lie_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
h : IsLieAbelian L
⊢ Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊤

Tactic:
rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot] at h

Premises used: LieAlgebra.center_eq_bot, LieAlgebra.isLieAbelian_iff_center_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
h : Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊤
⊢ Subsingleton L

Tactic:
(LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)

Premises used: subsingleton_of_bot_eq_top, Iff.mp, LieSubmodule.subsingleton_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
h : Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊤
⊢ Subsingleton L

Tactic:
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)

Premises used: subsingleton_of_bot_eq_top, Iff.mp, LieSubmodule.subsingleton_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
rw : IsLieAbelian.{u_2} ↥⊥
⊢ IsLieAbelian.{u_2} ↥(radical R L)

Tactic:
rw [HasTrivialRadical.radical_eq_bot]

Premises used: LieAlgebra.HasTrivialRadical.radical_eq_bot
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
⊢ IsLieAbelian.{u_2} ↥⊥

Tactic:
LieIdeal.isLieAbelian_of_trivial ..

Premises used: LieIdeal.isLieAbelian_of_trivial
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
⊢ IsLieAbelian.{u_2} ↥⊥

Tactic:
exact LieIdeal.isLieAbelian_of_trivial ..

Premises used: LieIdeal.isLieAbelian_of_trivial
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
mp : IsLieAbelian.{u_2} ↥(radical R L) → ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
mpr : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I) → IsLieAbelian.{u_2} ↥(radical R L)
⊢ IsLieAbelian.{u_2} ↥(radical R L) ↔ ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h₁ : IsLieAbelian.{u_2} ↥(radical R L)
I : LieIdeal R L
h₂ : IsSolvable.{u_2} ↥I
⊢ I ≤ radical R L

Tactic:
rw [LieIdeal.solvable_iff_le_radical] at h₂

Premises used: LieAlgebra.LieIdeal.solvable_iff_le_radical
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h₁ : IsLieAbelian.{u_2} ↥(radical R L)
I : LieIdeal R L
h₂ : I ≤ radical R L
⊢ IsLieAbelian.{u_2} ↥I

Tactic:
(LieIdeal.inclusion_injective h₂).isLieAbelian h₁

Premises used: Function.Injective.isLieAbelian, LieIdeal.inclusion_injective
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h₁ : IsLieAbelian.{u_2} ↥(radical R L)
I : LieIdeal R L
h₂ : I ≤ radical R L
⊢ IsLieAbelian.{u_2} ↥I

Tactic:
exact (LieIdeal.inclusion_injective h₂).isLieAbelian h₁

Premises used: Function.Injective.isLieAbelian, LieIdeal.inclusion_injective
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h : ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
mpr : IsSolvable.{u_2} ↥(radical R L)
⊢ IsLieAbelian.{u_2} ↥(radical R L)

Tactic:
apply h
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
h : ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → IsLieAbelian.{u_2} ↥I
⊢ IsSolvable.{u_2} ↥(radical R L)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
χ : L → R
x : L
m : M
hm :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
          (⨅ (x : L),
            Module.End.eigenspace
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) (χ x)))))
    m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
          (⨅ (x : L),
            Module.End.eigenspace
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) (χ x)))))
    ⁅x, m⁆

Tactic:
simp_all [smul_comm (χ x)]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
χ : L → R
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (weightSpace M χ) m ↔ ∀ (x : L), ⁅x, m⁆ = χ x • m

Tactic:
simp [weightSpace]

Premises used: LieModule.weightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
m₃ : M₃
simp :
  ∀ (x_1 : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)),
    (g : (a : M₁ ⊗[R] M₂) → M₃)
          ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
              x_1 :
            M₁ ⊗[R] M₂) =
        m₃ →
      ∃ (k : ℕ),
        Eq (α := M₃)
          ((HSub.hSub (α := Module.End R M₃)
                    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                      Module.End R M₃)
                    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
                  k :
                (a : M₃) → M₃)
              m₃ :
            M₃)
          (0 : M₃)
⊢ m₃ ∈
      LinearMap.range (M := TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x))
        ((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ TensorProduct.mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x)) →
    Membership.mem (γ := Submodule R M₃) 𝕎(M₃, χ₁ + χ₂, x) m₃

Tactic:
simp only [TensorProduct.mapIncl, LinearMap.mem_range, LinearMap.coe_comp,
    LieModuleHom.coe_toLinearMap, Function.comp_apply, exists_imp, Module.End.mem_maxGenEigenspace]

Premises used: TensorProduct.mapIncl, LieModuleHom.coe_toLinearMap, LinearMap.coe_comp, LinearMap.mem_range, Module.End.mem_maxGenEigenspace, Function.comp_apply, exists_imp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
⊢ ∃ (k : ℕ),
    Eq (α := M₃)
      ((HSub.hSub (α := Module.End R M₃)
                (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x :
                  Module.End R M₃)
                (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1) ^
              k :
            (a : M₃) → M₃)
          ((g : (a : M₁ ⊗[R] M₂) → M₃)
              ((TensorProduct.map (Submodule.subtype 𝕎(M₁, χ₁, x)) (Submodule.subtype 𝕎(M₂, χ₂, x)) :
                    (a : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)) → M₁ ⊗[R] M₂)
                  t :
                M₁ ⊗[R] M₂) :
            M₃) :
        M₃)
      (0 : M₃)

Tactic:
t.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on