-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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⁆
⊢ 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⁆
have mem₂ : ∀ (m₁ m₂ : L),
  Membership.mem (γ := LieSubmodule K (↥H) L)
      (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) m₁ →
    Membership.mem (γ := LieSubmodule K (↥H) L)
        (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) 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 sorry) :
                    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 sorry) :
                    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 sorry) :
                  Submodule K L))))
          ⁅x_χ, m₁ + 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₂
Cleared hypotheses: hm