-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
this :
  ∀ (n : ι → ℕ),
    Membership.mem (γ := AddSubmonoid (Dual.{u_2, u_3} K ↥b.cartan))
      (closure
        (image (α := ↥(root : Finset (Weight K (↥b.cartan) L)))
          ((⇑(RootPairing.root (rootSystem b.cartan)) :
              (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan) :
            (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan)
          (range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L)))))
      (∑ i : ι, n i • b.baseSupp i)
s : Set (↥b.cartan → K) :=
  {0} ∪ {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)} ∪
    {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)}
hs : Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L) (⨆ α ∈ s, rootSpace b.cartan α) ⊤
⊢ Membership.mem (α := Dual.{u_2, u_3} K ↥b.cartan) (γ := AddSubmonoid (Dual.{u_2, u_3} K ↥b.cartan))
      (closure
        (image (α := ↥(root : Finset (Weight K (↥b.cartan) L)))
          ((⇑(RootPairing.root (rootSystem b.cartan)) :
              (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan) :
            (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan)
          (range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L)))))
      ((RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan) χ : Dual.{u_2, u_3} K ↥b.cartan) ∨
    Membership.mem (α := Dual.{u_2, u_3} K ↥b.cartan) (γ := AddSubmonoid (Dual.{u_2, u_3} K ↥b.cartan))
      (closure
        (image (α := ↥(root : Finset (Weight K (↥b.cartan) L)))
          ((⇑(RootPairing.root (rootSystem b.cartan)) :
              (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan) :
            (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan)
          (range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L)))))
      (-(RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan) χ : Dual.{u_2, u_3} K ↥b.cartan)
have obtain : ∀ (χ : Weight K (↥b.cartan) L)
  (hχ : Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L)) χ),
  Membership.mem (α := Dual.{u_2, u_3} K ↥b.cartan) (γ := AddSubmonoid (Dual.{u_2, u_3} K ↥b.cartan))
      (closure
        (image (α := ↥(root : Finset (Weight K (↥b.cartan) L)))
          ((⇑(RootPairing.root (rootSystem b.cartan)) :
              (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan) :
            (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan)
          (range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L)))))
      ((RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan)
          (Subtype.mk (p := fun (x : Weight K (↥b.cartan) L) ↦
            Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L)) x) χ hχ) :
        Dual.{u_2, u_3} K ↥b.cartan) ∨
    Membership.mem (α := Dual.{u_2, u_3} K ↥b.cartan) (γ := AddSubmonoid (Dual.{u_2, u_3} K ↥b.cartan))
      (closure
        (image (α := ↥(root : Finset (Weight K (↥b.cartan) L)))
          ((⇑(RootPairing.root (rootSystem b.cartan)) :
              (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan) :
            (a : ↥(root : Finset (Weight K (↥b.cartan) L))) → Dual.{u_2, u_3} K ↥b.cartan)
          (range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L)))))
      (-(RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan)
            (Subtype.mk (p := fun (x : Weight K (↥b.cartan) L) ↦
              Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L)) x) χ hχ) :
        Dual.{u_2, u_3} K ↥b.cartan)
Tactic: obtain ⟨χ, hχ⟩ := χ
Cleared hypotheses: χ