-- 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
inr₆ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := s'.sup id;
    I ≤ K
inr₇ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := s'.sup id;
    ∀ ⦃x : L⦄ (hx : x ∈ I), x ∈ K
inr₈ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := s'.sup id;
    ∀ (y : L) (hy : y ∈ id J) (z : L) (hz : z ∈ K) (hx : y + z ∈ I), y + z ∈ K
inr₉ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := s'.sup id;
    ∀ (y : L) (hy : y ∈ id J) (z : L) (hz : z ∈ K) (hx : y + z ∈ I),
      Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
inr₁₀ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := s'.sup id;
    ∀ (y : L) (hy : y ∈ id J) (z : L) (hz : z ∈ K) (hx : y + z ∈ I) (j : ↥J),
      ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 0
inr₁₁ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := 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
inr₁₂ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := 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⁆
inr₁₃ :
  let s' := s.erase J;
  ∀ (hs' : s' ⊂ s) (hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S),
    let K := 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⁆
⊢ ∃ 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;
  ∀ (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⁆
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