-- Mathlib/Algebra/Lie/LieTheorem.lean
private lemma exists_forall_lie_eq_smul_of_isSolvable_of_finite
    (L : Type*) [LieRing L] [LieAlgebra k L] [LieRingModule L V] [LieModule k L V]
    [IsSolvable L] [LieModule.IsTriangularizable k L V] [Module.Finite k L] :
    ∃ χ : Module.Dual k L, Nontrivial (weightSpace V χ)

Proof state:
case hst
k : Type u_1
inst✝¹⁸ : Field k
V : Type u_3
inst✝¹⁷ : AddCommGroup V
inst✝¹⁶ : Module k V
inst✝¹⁵ : CharZero k
inst✝¹⁴ : Module.Finite k V
inst✝¹³ : Nontrivial V
x✝ :
  (L : Type u_4) ×'
    (inst : LieRing L) ×'
      (inst_1 : LieAlgebra k L) ×'
        (inst_2 : LieRingModule L V) ×'
          (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝⁷ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
L : Type u_4
inst✝¹² :
  (inst : LieRing L) ×'
    (inst_1 : LieAlgebra k L) ×'
      (inst_2 : LieRingModule L V) ×'
        (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝⁶ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, inst✝¹²⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝¹¹ : LieRing L
inst✝¹⁰ :
  (inst : LieAlgebra k L) ×'
    (inst_1 : LieRingModule L V) ×'
      (inst_2 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝⁵ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, inst✝¹⁰⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝⁹ : LieAlgebra k L
inst✝⁸ :
  (inst : LieRingModule L V) ×'
    (inst_1 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝⁴ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, ⟨inst✝⁹, inst✝⁸⟩⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝⁷ : LieRingModule L V
inst✝⁶ : (inst : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝³ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, ⟨inst✝⁹, ⟨inst✝⁷, inst✝⁶⟩⟩⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝⁵ : LieModule k L V
inst✝⁴ : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝² :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, ⟨inst✝⁹, ⟨inst✝⁷, ⟨inst✝⁵, inst✝⁴⟩⟩⟩⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝³ : IsSolvable L
inst✝² : (_ : IsTriangularizable k L V) ×' Module.Finite k L
a✝¹ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, ⟨inst✝⁹, ⟨inst✝⁷, ⟨inst✝⁵, ⟨inst✝³, inst✝²⟩⟩⟩⟩⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
a✝ :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst : LieRing L) ×'
          (inst_1 : LieAlgebra k L) ×'
            (inst_2 : LieRingModule L V) ×'
              (inst_3 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    (invImage
            (fun x =>
              PSigma.casesOn x fun L inst =>
                PSigma.casesOn inst fun inst inst_1 =>
                  PSigma.casesOn inst_1 fun inst_2 inst_3 =>
                    PSigma.casesOn inst_3 fun inst_4 inst_5 =>
                      PSigma.casesOn inst_5 fun inst_6 inst_7 =>
                        PSigma.casesOn inst_7 fun inst_8 inst_9 =>
                          PSigma.casesOn inst_9 fun inst_10 inst_11 => Module.finrank k L)
            instWellFoundedRelationOfSizeOf).1
        y ⟨L, ⟨inst✝¹¹, ⟨inst✝⁹, ⟨inst✝⁷, ⟨inst✝⁵, ⟨inst✝³, ⟨inst✝¹, inst✝⟩⟩⟩⟩⟩⟩⟩ →
      ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
h✝² : ∃ a, IsCoatom a ∧ ↑(derivedSeries k L 1) ≤ a
A✝¹ : Submodule k L
h✝¹ : IsCoatom A✝¹ ∧ ↑(derivedSeries k L 1) ≤ A✝¹
hA✝¹ : IsCoatom A✝¹
hAL✝¹ : ↑(derivedSeries k L 1) ≤ A✝¹
A✝ : LieSubmodule k L L
h✝ : ↑A✝ = A✝¹
hA✝ : IsCoatom ↑A✝
hAL✝ : ↑(derivedSeries k L 1) ≤ ↑A✝
A : LieIdeal k L
hA : IsCoatom ↑A
hAL : ↑(derivedSeries k L 1) ≤ ↑A
⊢ ↑A < ⊤

Tactic:
exact hA.lt_top

Result:
no goals