awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0
have inr : Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆ ∧ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
Tactic: rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆ ∧
    Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
have inr : Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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), z⁆ ∧
    Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
have inr₁ : Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), z⁆
have inr : ⁅(↑j : L), z⁆ ∈ J ⊓ sSup (↑s' : Set (LieIdeal R L))
Tactic: apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 : L), z⁆ ∈ J ⊓ sSup (↑s' : Set (LieIdeal R L))
have inr : ⁅(↑j : L), z⁆ ∈ ⁅J, sSup (↑s' : Set (LieIdeal R L))⁆
Tactic: apply LieSubmodule.lie_le_inf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 : L), z⁆ ∈ ⁅J, sSup (↑s' : Set (LieIdeal R L))⁆
have inr : z ∈ sSup (↑s' : Set (LieIdeal R L))
Tactic: apply LieSubmodule.lie_mem_lie j.2
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊥
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
have a : ⁅(↑j : L), y + z⁆ ∈ J ⊓ I
Tactic: apply this.le
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
have a : ⁅(↑j : L), y + z⁆ ∈ ⁅J, I⁆
Tactic: apply LieSubmodule.lie_le_inf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ ⁅(↑j : L), y + z⁆
have inr : J ⊓ I = ⊥
Tactic: suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊥
have inr : ¬J ⊓ I = J
Tactic: apply ((hs hJs).le_iff.mp _).resolve_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ J ⊓ I = ⊥
have apply : J ⊓ I ≤ J
Tactic: apply ((hs hJs).le_iff.mp _).resolve_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
have inr : ∀ (hJI : J ⊓ I = J), J ≤ I
Tactic: contrapose hJI
Cleared hypotheses: hJI
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
have inr : J ⊓ I ≤ I
Tactic: rw [← hJI]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
inr inr₁ inr₂ : ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr₃ : let s' := s.erase J;
∀ (hs' : s' ⊂ s), ∃ t ⊆ s, I = t.sup id
Tactic: classical
  let s' := s.erase J
  have hs' : s' ⊂ s := Finset.erase_ssubset hJs
  have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
  -- If we show that `I` is contained in the supremum `K` of the complement of `J` in `s`,
  -- then we are done by recursion.
  set K := s'.sup id
  suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
  -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
  -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
  intro x hx
  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
  -- If we show that `y` is contained in the center of `J`,
  -- then we find `x = z`, and hence `x` is contained in the supremum of `s'`.
  -- Since `x` was arbitrary, we have shown that `I` is contained in the supremum of `s'`.
  suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
  -- To show that `y` is in the center of `J`,
  -- we show that any `j ∈ J` brackets to `0` with `z` and with `x = y + z`.
  -- By a simple computation, that implies `⁅j, y⁆ = 0`, for all `j`, as desired.
  intro j
  suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2
  rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]
  constructor
  -- `j` brackets to `0` with `z`, since `⁅j, z⁆` is contained in `⁅J, K⁆ ≤ J ⊓ K`,
  -- and `J ⊓ K = ⊥` by the independence of the atoms.
  · apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot
    apply LieSubmodule.lie_le_inf
    apply LieSubmodule.lie_mem_lie j.2
    simpa only [K, Finset.sup_id_eq_sSup] using hz
  -- By similar reasoning, `j` brackets to `0` with `x = y + z ∈ I`, if we show `J ⊓ I = ⊥`.
  suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
  -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`.
  apply ((hs hJs).le_iff.mp _).resolve_right
  · contrapose hJI
    rw [← hJI]
    exact inf_le_right
  exact inf_le_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
inr inr₁ inr₂ : ∃ t ⊆ s, I = t.sup id
inr₃ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s), ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr₄ : let s' := s.erase J;
∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S), ∃ t ⊆ s, I = t.sup id
Tactic: classical
  let s' := s.erase J
  have hs' : s' ⊂ s := Finset.erase_ssubset hJs
  have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
  -- If we show that `I` is contained in the supremum `K` of the complement of `J` in `s`,
  -- then we are done by recursion.
  set K := s'.sup id
  suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
  -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
  -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
  intro x hx
  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
  -- If we show that `y` is contained in the center of `J`,
  -- then we find `x = z`, and hence `x` is contained in the supremum of `s'`.
  -- Since `x` was arbitrary, we have shown that `I` is contained in the supremum of `s'`.
  suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
  -- To show that `y` is in the center of `J`,
  -- we show that any `j ∈ J` brackets to `0` with `z` and with `x = y + z`.
  -- By a simple computation, that implies `⁅j, y⁆ = 0`, for all `j`, as desired.
  intro j
  suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2
  rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]
  constructor
  -- `j` brackets to `0` with `z`, since `⁅j, z⁆` is contained in `⁅J, K⁆ ≤ J ⊓ K`,
  -- and `J ⊓ K = ⊥` by the independence of the atoms.
  · apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot
    apply LieSubmodule.lie_le_inf
    apply LieSubmodule.lie_mem_lie j.2
    simpa only [K, Finset.sup_id_eq_sSup] using hz
  -- By similar reasoning, `j` brackets to `0` with `x = y + z ∈ I`, if we show `J ⊓ I = ⊥`.
  suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
  -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`.
  apply ((hs hJs).le_iff.mp _).resolve_right
  · contrapose hJI
    rw [← hJI]
    exact inf_le_right
  exact inf_le_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
inr inr₁ inr₂ : ∃ t ⊆ s, I = t.sup id
inr₃ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s), ∃ t ⊆ s, I = t.sup id
inr₄ inr₅ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S), ∃ t ⊆ s, I = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr₆ : let s' := s.erase J;
∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
  let K := s'.sup id;
  I ≤ K
Tactic: classical
  let s' := s.erase J
  have hs' : s' ⊂ s := Finset.erase_ssubset hJs
  have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
  -- If we show that `I` is contained in the supremum `K` of the complement of `J` in `s`,
  -- then we are done by recursion.
  set K := s'.sup id
  suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
  -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
  -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
  intro x hx
  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
  -- If we show that `y` is contained in the center of `J`,
  -- then we find `x = z`, and hence `x` is contained in the supremum of `s'`.
  -- Since `x` was arbitrary, we have shown that `I` is contained in the supremum of `s'`.
  suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
  -- To show that `y` is in the center of `J`,
  -- we show that any `j ∈ J` brackets to `0` with `z` and with `x = y + z`.
  -- By a simple computation, that implies `⁅j, y⁆ = 0`, for all `j`, as desired.
  intro j
  suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2
  rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]
  constructor
  -- `j` brackets to `0` with `z`, since `⁅j, z⁆` is contained in `⁅J, K⁆ ≤ J ⊓ K`,
  -- and `J ⊓ K = ⊥` by the independence of the atoms.
  · apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot
    apply LieSubmodule.lie_le_inf
    apply LieSubmodule.lie_mem_lie j.2
    simpa only [K, Finset.sup_id_eq_sSup] using hz
  -- By similar reasoning, `j` brackets to `0` with `x = y + z ∈ I`, if we show `J ⊓ I = ⊥`.
  suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
  -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`.
  apply ((hs hJs).le_iff.mp _).resolve_right
  · contrapose hJI
    rw [← hJI]
    exact inf_le_right
  exact inf_le_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ HasTrivialRadical R L
have rw : ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
Tactic: rw [hasTrivialRadical_iff_no_abelian_ideals]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ I = ⊥
have apply : ¬∃ (a : LieIdeal R L), IsAtom a ∧ a ≤ I
Tactic: apply (eq_bot_or_exists_atom_le I).resolve_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ False
have apply : IsLieAbelian.{u_2} ↥J
Tactic: apply IsSemisimple.non_abelian_of_isAtom J hJ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ IsLieAbelian.{u_2} ↥J
have trivial : ∀ (x m : ↥J), ⁅x, m⁆ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ ⁅x, y⁆ = 0
have trivial : (↑⁅x, y⁆ : L) = (↑0 : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ (↑⁅x, y⁆ : L) = (↑0 : L)
have trivial : ⁅(↑x : L), (↑y : L)⁆ = 0
Tactic: simp only [LieIdeal.coe_bracket_of_module, LieSubmodule.coe_bracket, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0
have this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) sorry, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) sorry⁆ = 0
Tactic: have : (⁅(⟨x, hJ' x.2⟩ : I), ⟨y, hJ' y.2⟩⁆ : I) = 0 := trivial_lie_zero _ _ _ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
⊢ ⁅(↑x : L), (↑y : L)⁆ = 0
have this₁ : (↑⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑x : L) sorry, Subtype.mk (p := fun (x : L) ↦ x ∈ I) (↑y : L) sorry⁆ : L) = (↑0 : L)
Tactic: apply_fun Subtype.val at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ IsSemisimple R L
have sSup_atoms_eq_top : Eq.{u_2 + 1} (α := LieIdeal R L) (sSup {I : LieIdeal R L | IsAtom I}) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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}) ⊤
⊢ IsSemisimple R L
have sSupIndep_isAtom : sSupIndep.{u_2} (α := LieIdeal R L) {I : LieIdeal R L | IsAtom I}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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}
⊢ IsSemisimple R L
have non_abelian_of_isAtom : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ False
have non_abelian_of_isAtom : IsLieAbelian L
Tactic: apply IsSimple.non_abelian (R := R) (L := L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
⊢ IsLieAbelian L
have hI₃ : I = ⊤
Tactic: rw [IsSimple.isAtom_iff_eq_top] at hI₁
Cleared hypotheses: hI₁, hI₂