-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
χ : Weight K (↥H) L
x_χ : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
mem :
  ∀ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }) (m_α : L)
    (hm_α : m_α ∈ sl2SubmoduleOfRoot ⋯),
    Membership.mem (γ := Set L)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
            (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
              Submodule K L))))
      ⁅x_χ, m_α⁆
mem₁ :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, 0⁆
mem₂ :
  ∀ (m₁ m₂ : L),
    Membership.mem (γ := LieSubmodule K (↥H) L)
        (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) m₁ →
      Membership.mem (γ := LieSubmodule K (↥H) L)
          (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) m₂ →
        ∀
          (ih₁ :
            Membership.mem (γ := Set L)
              (AddSubsemigroup.carrier
                (AddSubmonoid.toAddSubsemigroup
                  (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
                    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
                          sl2SubmoduleOfRoot ⋯) :
                      Submodule K L))))
              ⁅x_χ, m₁⁆)
          (ih₂ :
            Membership.mem (γ := Set L)
              (AddSubsemigroup.carrier
                (AddSubmonoid.toAddSubsemigroup
                  (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
                    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
                          sl2SubmoduleOfRoot ⋯) :
                      Submodule K L))))
              ⁅x_χ, m₂⁆),
          Membership.mem (γ := Set L)
            (AddSubsemigroup.carrier
              (AddSubmonoid.toAddSubsemigroup
                (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
                  (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
                        sl2SubmoduleOfRoot ⋯) :
                    Submodule K L))))
            ⁅x_χ, m₁ + m₂⁆
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m⁆

Tactic:
induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂

Premises used: SetLike.mem_coe, lie_zero, ZeroMemClass.zero_mem, Submodule.carrier_eq_coe, lie_add