awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep (α := LieSubmodule R (↥b.cartan) L) fun (χ : ↥b.cartan → R) ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace b.cartan 0) (U ⊔ V)
h₁ : Disjoint U (V ⊔ rootSpace b.cartan 0)
⊢ Disjoint V (rootSpace b.cartan 0 ⊔ U)

Tactic:
have h₂ : Disjoint V (rootSpace b.cartan 0 ⊔ U) := by
    convert! key.disjoint_biSup_biSup (Disjoint.union_left hV0 hUV).symm
    rw [iSup_union, hs0', hsU']
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep (α := LieSubmodule R (↥b.cartan) L) fun (χ : ↥b.cartan → R) ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace b.cartan 0) (U ⊔ V)
h₁ : Disjoint U (V ⊔ rootSpace b.cartan 0)
h₂ : Disjoint V (rootSpace b.cartan 0 ⊔ U)
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]

Tactic:
simp [iSupIndep_fin_three, h₀, h₁, h₂]

Premises used: iSupIndep_fin_three
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
⊢ b.cartan.toLieSubmodule = rootSpace b.cartan 0

Tactic:
congr_fun ((b.iSupIndep_rootSpace.le_iff_eq_of_iSup_eq_top
    b.iSup_cartan_borelLower_borelUpper_eq_top).mp b.cartan_borelLower_borelUpper_le) 0

Premises used: Eq.mpr, iInf, Fin.cons, Fin.induction.go, LieAlgebra.Basis.iSupIndep_rootSpace, Fin.induction, iSupIndep.le_iff_eq_of_iSup_eq_top, LieSubalgebra.toLieSubmodule, Iff.mp, Fin.cases, LieModule.genWeightSpace, congr_fun, OfNat.ofNat, _private.0.LieAlgebra.Basis.cartan_borelLower_borelUpper_le, Matrix.vecCons, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
⊢ b.borelLower =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))

Tactic:
congr_fun ((b.iSupIndep_rootSpace.le_iff_eq_of_iSup_eq_top
    b.iSup_cartan_borelLower_borelUpper_eq_top).mp b.cartan_borelLower_borelUpper_le) 1

Premises used: Eq.mpr, iSup, Fin.cons, Fin.induction.go, LieAlgebra.Basis.iSupIndep_rootSpace, LieAlgebra.Basis.borelLower, Fin.induction, iSupIndep.le_iff_eq_of_iSup_eq_top, Iff.mp, Fin.cases, congr_fun, OfNat.ofNat, _private.0.LieAlgebra.Basis.cartan_borelLower_borelUpper_le, Matrix.vecCons, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
⊢ b.borelUpper =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))

Tactic:
congr_fun ((b.iSupIndep_rootSpace.le_iff_eq_of_iSup_eq_top
    b.iSup_cartan_borelLower_borelUpper_eq_top).mp b.cartan_borelLower_borelUpper_le) 2

Premises used: Eq.mpr, iSup, Fin.cons, Fin.induction.go, LieAlgebra.Basis.iSupIndep_rootSpace, Fin.induction, iSupIndep.le_iff_eq_of_iSup_eq_top, Iff.mp, Fin.cases, LieAlgebra.Basis.borelUpper, congr_fun, OfNat.ofNat, _private.0.LieAlgebra.Basis.cartan_borelLower_borelUpper_le, Matrix.vecCons, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
inst_8 : IsNoetherian R L
rw : b.cartan.toLieSubmodule = rootSpace b.cartan 0
rw₁ rw₂ : rootSpace b.cartan 0 = rootSpace b.cartan 0
⊢ b.cartan.IsCartanSubalgebra

Tactic:
rw [← eq_rootSpace_zero_iff_isCartan, b.cartan_eq]

Premises used: LieAlgebra.Basis.cartan_eq, LieAlgebra.eq_rootSpace_zero_iff_isCartan
-- 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
i : ι
refine_1 : Ne (α := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) ⊥
refine_2 :
  Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L))
    { toFun := (⇑(b.baseSupp i) : (a : ↥b.cartan) → K), genWeightSpace_ne_bot' := ⋯ }
⊢ ↥(root : Finset (Weight K (↥b.cartan) L))

Tactic:
refine ⟨⟨b.baseSupp i, ?_⟩, ?_⟩
-- 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
i : ι
refine_1 :
  ∃ (x : L) (_ :
    Membership.mem (γ := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) x),
    ¬x = 0
⊢ Ne (α := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) ⊥

Tactic:
simp only [LieSubmodule.eq_bot_iff, ne_eq, not_forall]

Premises used: ne_eq, Classical.not_forall, LieSubmodule.eq_bot_iff
-- 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
i : ι
x : ↥b.cartan
⊢ Eq (α := L)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := End K L) ((toEnd K (↥b.cartan) L : (a : ↥b.cartan) → End K L) x : End K L)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := End K L) ((b.baseSupp i : (a : ↥b.cartan) → K) x : K) 1))
            1 :
          (a : L) → L)
        (b.e i) :
      L)
    (0 : L)

Tactic:
simp
-- 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
i : ι
⊢ ∃ (x : L) (_ :
    Membership.mem (γ := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) x),
    ¬x = 0

Tactic:
exact ⟨b.e i, (mem_genWeightSpace _ _ _).mpr fun x ↦ ⟨1, by simp⟩, (b.sl2 i).e_ne_zero⟩
-- 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
i : ι
⊢ Membership.mem (γ := Finset (Weight K (↥b.cartan) L)) (root : Finset (Weight K (↥b.cartan) L))
    { toFun := (⇑(b.baseSupp i) : (a : ↥b.cartan) → K), genWeightSpace_ne_bot' := ⋯ }

Tactic:
simpa [Weight.IsNonZero, Weight.IsZero] using b.linearIndependent_baseSupp.ne_zero i

Premises used: LinearIndependent.ne_zero, LieModule.Weight.IsNonZero, LieModule.Weight.IsZero, LieAlgebra.Basis.linearIndependent_baseSupp
-- 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
i : ι
⊢ Weight.toLinear K (↥b.cartan) L
      ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
        Weight K (↥b.cartan) L) =
    b.baseSupp i

Tactic:
rfl

Premises used: Multiset.sum, LieAlgebra.Basis.baseSupp, Multiset.foldr, Finset.sum, rfl
-- 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
i j : ι
hij :
  Eq (α := ↥(root : Finset (Weight K (↥b.cartan) L))) (b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L)))
    (b.baseSupp' j : ↥(root : Finset (Weight K (↥b.cartan) L)))
⊢ b.baseSupp i = b.baseSupp j

Tactic:
simpa [baseSupp'] using hij

Premises used: LieAlgebra.Basis.baseSupp'
-- 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
e : ι ≃ (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3)) :=
  Equiv.ofInjective b.baseSupp' ⋯
rw :
  LinearIndependent (ι := ι) K (M := Dual.{u_2, u_3} K ↥b.cartan)
    ((fun (x : (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3))) ↦
        (RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan) (↑x : ↥root)) ∘
      (⇑e : (a : ι) → (↑(range b.baseSupp') : Type (max u_2 u_3))))
⊢ LinearIndepOn (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) K (M := Dual.{u_2, u_3} K ↥b.cartan)
    ((⇑(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)))

Tactic:
rw [LinearIndepOn, ← linearIndependent_equiv e]

Premises used: linearIndependent_equiv, LinearIndepOn
-- 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
e : ι ≃ (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3)) :=
  Equiv.ofInjective b.baseSupp' ⋯
⊢ LinearIndependent (ι := ι) K (M := Dual.{u_2, u_3} K ↥b.cartan)
    ((fun (x : (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3))) ↦
        (RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan) (↑x : ↥root)) ∘
      (⇑e : (a : ι) → (↑(range b.baseSupp') : Type (max u_2 u_3))))

Tactic:
b.linearIndependent_baseSupp

Premises used: Multiset.sum, LieAlgebra.Basis.baseSupp, Multiset.foldr, LieModule.Weight.toLinear, LieAlgebra.Basis.linearIndependent_baseSupp, Finset.sum
-- 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
e : ι ≃ (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3)) :=
  Equiv.ofInjective b.baseSupp' ⋯
⊢ LinearIndependent (ι := ι) K (M := Dual.{u_2, u_3} K ↥b.cartan)
    ((fun (x : (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3))) ↦
        (RootPairing.root (rootSystem b.cartan) : (a : ↥root) → Dual K ↥b.cartan) (↑x : ↥root)) ∘
      (⇑e : (a : ι) → (↑(range b.baseSupp') : Type (max u_2 u_3))))

Tactic:
exact b.linearIndependent_baseSupp

Premises used: LieAlgebra.Basis.linearIndependent_baseSupp
-- 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
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
n : ι → ℕ
simp_rw :
  Membership.mem (γ := Submodule ℕ (Dual.{u_2, u_3} K ↥b.cartan))
    (Submodule.span ℕ
      (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)
⊢ 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)

Tactic:
simp_rw [← Submodule.span_nat_eq_addSubmonoidClosure, Submodule.mem_toAddSubmonoid]

Premises used: Submodule.mem_toAddSubmonoid, Submodule.span_nat_eq_addSubmonoidClosure
-- 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
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
n : ι → ℕ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Membership.mem (γ := Set (Dual.{u_2, u_3} K ↥b.cartan))
    (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))))
    (b.baseSupp i)

Tactic:
simp
-- 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
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
n : ι → ℕ
⊢ Membership.mem (γ := Submodule ℕ (Dual.{u_2, u_3} K ↥b.cartan))
    (Submodule.span ℕ
      (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)

Tactic:
exact Submodule.sum_smul_mem _ _ fun i _ ↦ Submodule.subset_span <| by simp

Premises used: Submodule.sum_smul_mem, Submodule.subset_span
-- 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
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
⊢ ∀ (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)

Tactic:
have (n : ι → ℕ) :
      ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem b.cartan).root '' range b.baseSupp') := by
    simp_rw [← Submodule.span_nat_eq_addSubmonoidClosure, Submodule.mem_toAddSubmonoid]
    exact Submodule.sum_smul_mem _ _ fun i _ ↦ Submodule.subset_span <| by simp
-- 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
χ : ↥(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)}
⊢ iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
have := b.iSup_cartan_borelLower_borelUpper_eq_top
-- 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
χ : ↥(root : Finset (Weight K (↥b.cartan) L))
this_1 :
  ∀ (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)}
this : iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤
⊢ iSup
      ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → K) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → K)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → K) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → K))] =
    ⊤

Tactic:
rw [borelLower_eq, borelUpper_eq, cartan_eq] at this

Premises used: LieAlgebra.Basis.cartan_eq, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.borelLower_eq