-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
L : Type u_2
inst : LieRing L
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : LieAlgebra K L
H : LieSubalgebra K L
inst_6 : LieRing.IsNilpotent.{u_2} ↥H
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : IsTriangularizable.{u_4, u_2, u_3} K (↥H) M
inst_10 : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
hm :
  Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
    (⨆ (χ : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑χ : (a : ↥H) → K)) m
zero :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          0 :
        M)
      (0 : M)
mem :
  ∀ (χ₂ : Weight.{u_4, u_2, u_3} K (↥H) M) (m₂ : M)
    (hm₂ : Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M) (genWeightSpace M (⇑χ₂ : (a : ↥H) → K)) m₂),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            m₂ :
          M)
        (0 : M)
add :
  ∀ (m₁ m₂ : M)
    (hm₁ :
      Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
        (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₁)
    (hm₂ :
      Membership.mem (γ := LieSubmodule.{u_4, u_2, u_3} K (↥H) M)
        (⨆ (i : Weight.{u_4, u_2, u_3} K (↥H) M), genWeightSpace M (⇑i : (a : ↥H) → K)) m₂)
    (hm₁' :
      ∃ (n : ℕ),
        Eq (α := M)
          ((HPow.hPow (α := End K M)
                  (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
                (a : M) → M)
              m₁ :
            M)
          (0 : M))
    (hm₂' :
      ∃ (n : ℕ),
        Eq (α := M)
          ((HPow.hPow (α := End K M)
                  (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
                (a : M) → M)
              m₂ :
            M)
          (0 : M)),
    ∃ (n : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End K M)
                (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
              (a : M) → M)
            (m₁ + m₂) :
          M)
        (0 : M)
⊢ ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End K M)
              (((toEnd K L M : LieHom.{u_4, u_2, u_3} K L (End K M)) : (a : L) → End K M) x : End K M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)

Tactic:
induction hm using LieSubmodule.iSup_induction' with
  | zero => exact ⟨0, map_zero _⟩
  | mem χ₂ m₂ hm₂ =>
    obtain ⟨n, -, hn⟩ := exists_genWeightSpace_smul_add_eq_bot M χ χ₂ hχ
    use n
    have := toEnd_pow_apply_mem hx hm₂ n
    rwa [hn, LieSubmodule.mem_bot] at this
  | add m₁ m₂ hm₁ hm₂ hm₁' hm₂' =>
    obtain ⟨n₁, hn₁⟩ := hm₁'
    obtain ⟨n₂, hn₂⟩ := hm₂'
    refine ⟨max n₁ n₂, ?_⟩
    rw [map_add, Module.End.pow_map_zero_of_le le_sup_left hn₁,
      Module.End.pow_map_zero_of_le le_sup_right hn₂, add_zero]

Premises used: map_add, LieSubmodule.mem_bot, add_zero