Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: 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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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 x1 x2 ↦ x1 < x2)
        (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)
        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
⊢ Module.finrank k ↥A < Module.finrank k L

Tactic:
decreasing_by
  rw [← finrank_top k L]
  apply Submodule.finrank_lt_finrank_of_lt
  exact hA.lt_top

Goal state after: