-- 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
_x : (s : Finset (LieIdeal R L)) ×' (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id
h :
  ∀
    (y :
      (s : Finset (LieIdeal R L)) ×' (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (s : Finset (LieIdeal R L)) ×'
                (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
          PSigma.casesOn (β := fun (s : Finset (LieIdeal R L)) ↦
            (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) (motive :=
            fun
              (_x :
                (s : Finset (LieIdeal R L)) ×'
                  (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            ℕ) x
            fun (s : Finset (LieIdeal R L))
              (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            PSigma.casesOn (β := fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ↦ I ≤ s.sup id)
              (motive := fun (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦ ℕ)
              a fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) (a_1 : I ≤ s.sup id) ↦ s.card)
        y _x →
      ∃ t ⊆ y.1, I = t.sup id
s : Finset (LieIdeal R L)
a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id
h_1 :
  ∀
    (y :
      (s : Finset (LieIdeal R L)) ×' (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (s : Finset (LieIdeal R L)) ×'
                (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
          PSigma.casesOn (β := fun (s : Finset (LieIdeal R L)) ↦
            (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) (motive :=
            fun
              (_x :
                (s : Finset (LieIdeal R L)) ×'
                  (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            ℕ) x
            fun (s : Finset (LieIdeal R L))
              (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            PSigma.casesOn (β := fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ↦ I ≤ s.sup id)
              (motive := fun (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦ ℕ)
              a fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) (a_1 : I ≤ s.sup id) ↦ s.card)
        y
        (PSigma.mk (β := fun (s : Finset (LieIdeal R L)) ↦
          (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) s a) →
      ∃ t ⊆ y.1, I = t.sup id
h_2 : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
h_3 : I ≤ s.sup id
h_4 :
  ∀
    (y :
      (s : Finset (LieIdeal R L)) ×' (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (s : Finset (LieIdeal R L)) ×'
                (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
          PSigma.casesOn (β := fun (s : Finset (LieIdeal R L)) ↦
            (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) (motive :=
            fun
              (_x :
                (s : Finset (LieIdeal R L)) ×'
                  (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            ℕ) x
            fun (s : Finset (LieIdeal R L))
              (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦
            PSigma.casesOn (β := fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ↦ I ≤ s.sup id)
              (motive := fun (a : (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) ↦ ℕ)
              a fun (a : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) (a_1 : I ≤ s.sup id) ↦ s.card)
        y
        (PSigma.mk (β := fun (s : Finset (LieIdeal R L)) ↦
          (_ : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ×' I ≤ s.sup id) s
          (PSigma.mk (β := fun (hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}) ↦ I ≤ s.sup id) h_2
            h_3)) →
      ∃ t ⊆ y.1, I = t.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
h_5 : J ∈ s ∧ ¬J ≤ I
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
⊢ (s.erase J).card < s.card

Tactic:
exact Finset.card_lt_card hs'

Premises used: Finset.card_lt_card