-- 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
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (χ : Weight K (↥H) L), genWeightSpace L (⇑χ : (a : ↥H) → K)) x
mem :
  ∀ (χ : Weight K (↥H) L) (x_χ : L)
    (hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ),
    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⁆
zero :
  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))))
    (Bracket.bracket (L := L) 0 m)
add :
  ∀ (x₁ x₂ : L),
    Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₁ →
      Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₂ →
        ∀
          (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₁ + 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⁆

Tactic:
induction hx using LieSubmodule.iSup_induction' with
    | mem χ x_χ hx_χ =>
      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₂
    | zero =>
      simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]
    | add x₁ x₂ _ _ ih₁ ih₂ =>
      simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
      exact add_mem ih₁ ih₂

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