-- 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
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 α) ⊤
χ : 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)
have change : 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)))))
    (Weight.toLinear K (↥b.cartan) L χ) ∨
  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)))))
    (-Weight.toLinear K (↥b.cartan) L χ)
Tactic: change χ.toLinear ∈ _ ∨ -χ.toLinear ∈ _