-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
_x :
  (L : Type u_4) ×'
    (inst_19 : LieRing L) ×'
      (inst_20 : LieAlgebra k L) ×'
        (inst_21 : LieRingModule L V) ×'
          (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y _x →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
L : Type u_4
inst_6 :
  (inst_19 : LieRing L) ×'
    (inst_20 : LieAlgebra k L) ×'
      (inst_21 : LieRingModule L V) ×'
        (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_1 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L inst_6) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_7 : LieRing L
inst_8 :
  (inst_19 : LieAlgebra k L) ×'
    (inst_20 : LieRingModule L V) ×'
      (inst_21 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_2 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7 inst_8)) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_9 : LieAlgebra k L
inst_10 :
  (inst_19 : LieRingModule L V) ×'
    (inst_20 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_3 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7
            (PSigma.mk (β := fun [LieAlgebra k L] ↦
              (inst_20 : LieRingModule L V) ×'
                (inst_21 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              inst_9 inst_10))) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_11 : LieRingModule L V
inst_12 : (inst_19 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_4 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7
            (PSigma.mk (β := fun [LieAlgebra k L] ↦
              (inst_20 : LieRingModule L V) ×'
                (inst_21 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              inst_9
              (PSigma.mk (β := fun [LieRingModule L V] ↦
                (inst_20 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                inst_11 inst_12)))) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_13 : LieModule k L V
inst_14 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_5 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7
            (PSigma.mk (β := fun [LieAlgebra k L] ↦
              (inst_20 : LieRingModule L V) ×'
                (inst_21 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              inst_9
              (PSigma.mk (β := fun [LieRingModule L V] ↦
                (inst_20 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                inst_11
                (PSigma.mk (β := fun [LieModule k L V] ↦
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) inst_13 inst_14))))) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_15 : IsSolvable L
inst_16 : (_ : IsTriangularizable k L V) ×' Module.Finite k L
h_6 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7
            (PSigma.mk (β := fun [LieAlgebra k L] ↦
              (inst_20 : LieRingModule L V) ×'
                (inst_21 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              inst_9
              (PSigma.mk (β := fun [LieRingModule L V] ↦
                (inst_20 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                inst_11
                (PSigma.mk (β := fun [LieModule k L V] ↦
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) inst_13
                  (PSigma.mk (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L) inst_15
                    inst_16)))))) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
inst_17 : IsTriangularizable k L V
inst_18 : Module.Finite k L
h_7 :
  ∀
    (y :
      (L : Type u_4) ×'
        (inst_19 : LieRing L) ×'
          (inst_20 : LieAlgebra k L) ×'
            (inst_21 : LieRingModule L V) ×'
              (inst_22 : LieModule k L V) ×' (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun
            (x :
              (L : Type u_4) ×'
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
          PSigma.casesOn (β := fun (L : Type u_4) ↦
            (inst_19 : LieRing L) ×'
              (inst_20 : LieAlgebra k L) ×'
                (inst_21 : LieRingModule L V) ×'
                  (inst_22 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            (motive :=
            fun
              (_x :
                (L : Type u_4) ×'
                  (inst_19 : LieRing L) ×'
                    (inst_20 : LieAlgebra k L) ×'
                      (inst_21 : LieRingModule L V) ×'
                        (inst_22 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            ℕ) x
            fun (L : Type u_4)
              (inst_19 :
                (inst_19 : LieRing L) ×'
                  (inst_20 : LieAlgebra k L) ×'
                    (inst_21 : LieRingModule L V) ×'
                      (inst_22 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
            PSigma.casesOn (β := fun [LieRing L] ↦
              (inst_21 : LieAlgebra k L) ×'
                (inst_22 : LieRingModule L V) ×'
                  (inst_23 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              (motive :=
              fun
                (inst :
                  (inst_20 : LieRing L) ×'
                    (inst_21 : LieAlgebra k L) ×'
                      (inst_22 : LieRingModule L V) ×'
                        (inst_23 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              ℕ) inst_19
              fun (inst_20 : LieRing L)
                (inst_21 :
                  (inst_21 : LieAlgebra k L) ×'
                    (inst_22 : LieRingModule L V) ×'
                      (inst_23 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
              PSigma.casesOn (β := fun [LieAlgebra k L] ↦
                (inst_23 : LieRingModule L V) ×'
                  (inst_24 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                (motive :=
                fun
                  (inst :
                    (inst_22 : LieAlgebra k L) ×'
                      (inst_23 : LieRingModule L V) ×'
                        (inst_24 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                ℕ) inst_21
                fun (inst_22 : LieAlgebra k L)
                  (inst_23 :
                    (inst_23 : LieRingModule L V) ×'
                      (inst_24 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                PSigma.casesOn (β := fun [LieRingModule L V] ↦
                  (inst_25 : LieModule k L V) ×'
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                  (motive :=
                  fun
                    (inst :
                      (inst_24 : LieRingModule L V) ×'
                        (inst_25 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  ℕ) inst_23
                  fun (inst_24 : LieRingModule L V)
                    (inst_25 :
                      (inst_25 : LieModule k L V) ×'
                        (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                  PSigma.casesOn (β := fun [LieModule k L V] ↦
                    (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) (motive :=
                    fun
                      (inst :
                        (inst_26 : LieModule k L V) ×'
                          (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    ℕ) inst_25
                    fun (inst_26 : LieModule k L V)
                      (inst_27 : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                    PSigma.casesOn (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                      (motive :=
                      fun (inst : (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ)
                      inst_27
                      fun (inst_28 : IsSolvable L) (inst_29 : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦
                      PSigma.casesOn (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) (motive :=
                        fun (inst : (_ : IsTriangularizable k L V) ×' Module.Finite k L) ↦ ℕ) inst_29
                        fun (inst_30 : IsTriangularizable k L V) (inst_31 : Module.Finite k L) ↦ Module.finrank k L)
        y
        (PSigma.mk (β := fun (L : Type u_4) ↦
          (inst_19 : LieRing L) ×'
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
          L
          (PSigma.mk (β := fun [LieRing L] ↦
            (inst_20 : LieAlgebra k L) ×'
              (inst_21 : LieRingModule L V) ×'
                (inst_22 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
            inst_7
            (PSigma.mk (β := fun [LieAlgebra k L] ↦
              (inst_20 : LieRingModule L V) ×'
                (inst_21 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
              inst_9
              (PSigma.mk (β := fun [LieRingModule L V] ↦
                (inst_20 : LieModule k L V) ×'
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L)
                inst_11
                (PSigma.mk (β := fun [LieModule k L V] ↦
                  (_ : IsSolvable L) ×' (_ : IsTriangularizable k L V) ×' Module.Finite k L) inst_13
                  (PSigma.mk (β := fun [IsSolvable L] ↦ (_ : IsTriangularizable k L V) ×' Module.Finite k L) inst_15
                    (PSigma.mk (β := fun [IsTriangularizable k L V] ↦ Module.Finite k L) inst_17 inst_18))))))) →
      ∃ (χ : Module.Dual.{u_1, u_4} k y.1), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : y.1) → k))
h_8 : ∃ (a : Submodule k L), IsCoatom a ∧ (↑(derivedSeries k L 1) : Submodule k L) ≤ a
A_1 : Submodule k L
h_9 : IsCoatom A_1 ∧ (↑(derivedSeries k L 1) : Submodule k L) ≤ A_1
hA_1 : IsCoatom A_1
hAL_1 : (↑(derivedSeries k L 1) : Submodule k L) ≤ A_1
A : LieSubmodule k L L
h_10 : (↑A : Submodule k L) = A_1
hA : IsCoatom (↑A : Submodule k L)
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)
rw rw₁ rw₂ : Module.finrank.{u_1, u_4} k ↥A < Module.finrank.{u_1, u_4} k ↥⊤
⊢ Module.finrank.{u_1, u_4} k ↥A < Module.finrank k L
have hst : (↑A : Submodule k L) < ⊤
Tactic: decreasing_by
  rw [← finrank_top k L]
  apply Submodule.finrank_lt_finrank_of_lt
  exact hA.lt_top