-- Module: Mathlib.Algebra.Lie.Basis
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)}
χ : Weight K (↥b.cartan) L
hχ : Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L)) χ
hs :
  (∃ (n : ι → ℕ), n ≠ 0 ∧ Weight.toLinear K (↥b.cartan) L χ = -∑ i : ι, n i • b.baseSupp i) ∨
    ∃ (n : ι → ℕ), n ≠ 0 ∧ Weight.toLinear K (↥b.cartan) L χ = ∑ i : ι, n i • b.baseSupp i
refine_1 :
  (∃ (n : ι → ℕ), n ≠ 0 ∧ Weight.toLinear K (↥b.cartan) L χ = ∑ i : ι, n i • b.baseSupp i) →
    ∀ (n : ι → ℕ) (hn₀ : n ≠ 0) (hn : Weight.toLinear K (↥b.cartan) L χ = ∑ i : ι, n i • b.baseSupp i),
      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 χ)
refine_2 :
  (∃ (n : ι → ℕ), n ≠ 0 ∧ Weight.toLinear K (↥b.cartan) L χ = -∑ i : ι, n i • b.baseSupp i) →
    ∀ (n : ι → ℕ) (hn₀ : n ≠ 0) (hn : Weight.toLinear K (↥b.cartan) L χ = -∑ i : ι, n i • b.baseSupp i),
      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 χ) ∨
    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:
refine hs.symm.imp (fun ⟨n, hn₀, hn⟩ ↦ ?_) (fun ⟨n, hn₀, hn⟩ ↦ ?_)

Premises used: Or.symm, Or.imp