-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
/--
In a semisimple Lie algebra,
Lie ideals that are contained in the supremum of a finite collection of atoms
are themselves the supremum of a finite subcollection of those atoms.

By a compactness argument, this statement can be extended to arbitrary sets of atoms.
See `atomistic`.

The proof is by induction on the finite set of atoms.
-/
private
lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal R L | IsAtom I} →
    ∀ I : LieIdeal R L, I ≤ s.sup id → ∃ t ⊆ s, I = t.sup id

Proof state:
case inr.intro.intro.intro.intro.intro.intro.left.a.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ 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, z⁆ ∈ ⁅J, sSup ↑s'⁆

Tactic:
apply LieSubmodule.lie_mem_lie j.2

Result:
case inr.intro.intro.intro.intro.intro.intro.left.a.a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ 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'

Proof state:
case inr.intro.intro.intro.intro.intro.intro.right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ 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

Tactic:
rw [← hJI]

Result:
case inr.intro.intro.intro.intro.intro.intro.right
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ 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

Proof state:
case inr.intro.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs

Result:
case inr.intro.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ S
⊢ ∃ t ⊆ s, I = t.sup id

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
x✝ : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id
a✝⁶ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id),
    (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      ∃ t ⊆ y.1, y.2.2.1 = t.sup id
s : Finset (LieIdeal R L)
a✝⁵ : (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id
a✝⁴ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id),
    (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card)
            instWellFoundedRelationOfSizeOf).1
        y ⟨s, a✝⁵⟩ →
      ∃ t ⊆ y.1, y.2.2.1 = t.sup id
a✝³ : ↑s ⊆ {I | IsAtom I}
I✝ : (I : LieIdeal R L) ×' I ≤ s.sup id
a✝² :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id),
    (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card)
            instWellFoundedRelationOfSizeOf).1
        y ⟨s, ⟨a✝³, I✝⟩⟩ →
      ∃ t ⊆ y.1, y.2.2.1 = t.sup id
I : LieIdeal R L
a✝¹ : I ≤ s.sup id
a✝ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id),
    (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card)
            instWellFoundedRelationOfSizeOf).1
        y ⟨s, ⟨a✝³, ⟨I, a✝¹⟩⟩⟩ →
      ∃ t ⊆ y.1, y.2.2.1 = t.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
h✝ : J ∈ s ∧ ¬J ≤ I
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
this : I ≤ K
⊢ (s.erase J).card < s.card

Tactic:
exact Finset.card_lt_card hs'

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
this : ⟨y, hy⟩ ∈ center R ↥J
_inst : IsSimple R ↥J
⊢ y + z ∈ K

Tactic:
rw [center_eq_bot R J, LieSubmodule.mem_bot] at this

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
this : ⟨y, hy⟩ = 0
_inst : IsSimple R ↥J
⊢ y + z ∈ K

Proof state:
case intro.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | 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' ⊆ 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, Finset.Subset.trans hts' hs'.subset, htI⟩

Result:
no goals