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
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
x : L
hx_1 : x ∈ I
hx : x ∈ J'
a :
  ∀ (y : ↥I) (hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I))
    (hx : Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y : L)),
    Membership.mem (α := ↥I) J
      (Subtype.mk (p := fun (x : L) ↦ x ∈ I) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y) hx : ↥I)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx_1 ∈ J

Tactic:
rcases hx with ⟨y, hy, rfl⟩

Premises used: rfl
-- 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 : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx : Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y : L)
⊢ Membership.mem (α := ↥I) J (Subtype.mk (p := fun (x : L) ↦ x ∈ I) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y) hx : ↥I)

Tactic:
hy

Premises used: Set.Mem
-- 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 : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx : Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y : L)
⊢ Membership.mem (α := ↥I) J (Subtype.mk (p := fun (x : L) ↦ x ∈ I) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y) hx : ↥I)

Tactic:
exact hy
-- 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 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
inl : ∀ (hI : s.sup id ≤ s.sup id), ∃ t ⊆ s, s.sup id = t.sup id
inr : ∀ (hI : I < s.sup id), ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain rfl | hI := hI.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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}
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : s.sup id ≤ s.sup id
⊢ ∃ t ⊆ s, s.sup id = t.sup id

Tactic:
⟨s, Finset.Subset.rfl, rfl⟩

Premises used: Finset.Subset.rfl, And.intro, Exists.intro, rfl
-- 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}
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : s.sup id ≤ s.sup id
⊢ ∃ t ⊆ s, s.sup id = t.sup id

Tactic:
exact ⟨s, Finset.Subset.rfl, rfl⟩
-- 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
by_contra! : ∀ (H : ∀ (J : LieIdeal R L) (_ : J ∈ s), J ≤ I), False
⊢ ∃ J ∈ s, ¬J ≤ I

Tactic:
by_contra! 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 : 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
H : ∀ (J : LieIdeal R L) (_ : J ∈ s), J ≤ I
⊢ False

Tactic:
hI.ne (le_antisymm hI.le (s.sup_le H))

Premises used: LT.lt.le, Finset.sup_le, le_antisymm, LT.lt.ne
-- 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
H : ∀ (J : LieIdeal R L) (_ : J ∈ s), J ≤ I
⊢ False

Tactic:
exact hI.ne (le_antisymm hI.le (s.sup_le H))

Premises used: LT.lt.le, Finset.sup_le, le_antisymm, LT.lt.ne
-- 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
inr : ∀ (J : LieIdeal R L) (hJs : J ∈ s) (hJI : ¬J ≤ I), ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain ⟨J, hJs, hJI⟩ : ∃ J ∈ s, ¬ J ≤ I := by
    by_contra! H
    exact hI.ne (le_antisymm hI.le (s.sup_le 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 : 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
⊢ s' ⊂ s

Tactic:
have hs' : s' ⊂ s := Finset.erase_ssubset hJs
-- 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
⊢ (↑s' : Set (LieIdeal R L)) ⊆ S

Tactic:
have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
-- 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
this : I ≤ K
obtain : ∀ (t : Finset (LieIdeal R L)) (hts' : t ⊆ s') (htI : I = t.sup id), ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I 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
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
this : I ≤ K
t : Finset (LieIdeal R L)
hts' : t ⊆ s'
htI : I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
⟨t, hts'.trans hs'.subset, htI⟩

Premises used: HasSubset.Subset.trans, HasSSubset.SSubset.subset, And.intro, Exists.intro
-- 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
this : I ≤ K
t : Finset (LieIdeal R L)
hts' : t ⊆ s'
htI : I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
exact ⟨t, hts'.trans hs'.subset, htI⟩
-- 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
inr : I ≤ K
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
-- 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
x : L
hx : x ∈ I
rw : x ∈ s.sup id
⊢ ∃ y ∈ id J, ∃ z ∈ K, y + z = x

Tactic:
rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]

Premises used: Finset.sup_insert, LieSubmodule.mem_sup, Finset.insert_erase
-- 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
x : L
hx : x ∈ I
⊢ x ∈ s.sup id

Tactic:
hI.le hx

Premises used: Set.Mem, LT.lt.le
-- 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
x : L
hx : x ∈ I
⊢ x ∈ s.sup id

Tactic:
exact hI.le hx

Premises used: LT.lt.le
-- 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
x : L
hx : x ∈ I
inr : ∀ (y : L) (hy : y ∈ id J) (z : L) (hz : z ∈ K) (hx : y + z ∈ I), y + z ∈ K
⊢ x ∈ K

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y ∈ id J, ∃ z ∈ K, y + z = x := by
    rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]
    exact hI.le hx

Premises used: id, rfl
-- 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
this : Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
⊢ IsSimple.{u_1, u_2} R ↥J

Tactic:
have _inst := isSimple_of_isAtom J (hs hJs)
-- 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
this : Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
_inst : IsSimple.{u_1, u_2} R ↥J
⊢ y + z ∈ K

Tactic:
simp_all
-- 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
inr : Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
⊢ y + z ∈ K

Tactic:
suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
-- 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 : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0
⊢ Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0

Tactic:
rw [lie_add, this.1, add_zero] at this

Premises used: And.left, add_zero, lie_add
-- 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 : Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0
a : (↑⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ : L) = (↑0 : L)
⊢ ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 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
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 : Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0
⊢ (↑⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ : L) = (↑0 : L)

Tactic:
this.2

Premises used: And.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
this : Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0
⊢ (↑⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ : L) = (↑0 : L)

Tactic:
exact this.2

Premises used: And.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 : ⁅(↑j : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0
⊢ ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 0

Tactic:
suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2
-- 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 :
  Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆ ∧
    Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
⊢ ⁅(↑j : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0

Tactic:
rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]

Premises used: LieSubmodule.mem_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 : 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 : Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆
inr₁ : Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆ ∧
    Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆

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
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 : L), z⁆ ∈ J ⊓ sSup (↑s' : Set (LieIdeal R L))
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆

Tactic:
apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot

Premises used: Disjoint.le_bot, sSupIndep.disjoint_sSup, Finset.notMem_erase, LieAlgebra.IsSemisimple.sSupIndep_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
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 : L), z⁆ ∈ ⁅J, sSup (↑s' : Set (LieIdeal R L))⁆
⊢ ⁅(↑j : L), z⁆ ∈ J ⊓ sSup (↑s' : Set (LieIdeal R L))

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
inr : z ∈ sSup (↑s' : Set (LieIdeal R L))
⊢ ⁅(↑j : L), z⁆ ∈ ⁅J, sSup (↑s' : Set (LieIdeal R L))⁆

Tactic:
apply LieSubmodule.lie_mem_lie j.2

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
⊢ z ∈ sSup (↑s' : Set (LieIdeal R L))

Tactic:
simpa only [K, Finset.sup_id_eq_sSup] using hz

Premises used: Finset.sup_id_eq_sSup
-- 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
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆

Tactic:
apply this.le

Premises used: Eq.le