awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
      ![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))] =
    ⊤
rw :
  Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L)
    (((⨆ (x : ↥b.cartan → K), ⨆ (_ : Membership.mem (γ := Set (↥b.cartan → K)) {0} x), rootSpace b.cartan x) ⊔
        ⨆ (x : ↥b.cartan → K),
          ⨆ (_ :
            Membership.mem (γ := Set (↥b.cartan → K))
              {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)}
              x),
            rootSpace b.cartan x) ⊔
      ⨆ (x : ↥b.cartan → K),
        ⨆ (_ :
          Membership.mem (γ := Set (↥b.cartan → K))
            {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)} x),
          rootSpace b.cartan x)
    ⊤
⊢ Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L) (⨆ α ∈ s, rootSpace b.cartan α) ⊤

Tactic:
rw [iSup_union, iSup_union]

Premises used: iSup_union
-- 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
      ![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))] =
    ⊤
⊢ Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L)
    (((⨆ (x : ↥b.cartan → K), ⨆ (_ : Membership.mem (γ := Set (↥b.cartan → K)) {0} x), rootSpace b.cartan x) ⊔
        ⨆ (x : ↥b.cartan → K),
          ⨆ (_ :
            Membership.mem (γ := Set (↥b.cartan → K))
              {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)}
              x),
            rootSpace b.cartan x) ⊔
      ⨆ (x : ↥b.cartan → K),
        ⨆ (_ :
          Membership.mem (γ := Set (↥b.cartan → K))
            {f : ↥b.cartan → K | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)} x),
          rootSpace b.cartan x)
    ⊤

Tactic:
simpa [iSup_and, iSup_comm (ι := b.cartan → K)] using this

Premises used: iSup_comm, iSup_and
-- 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)}
⊢ Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L) (⨆ α ∈ s, rootSpace b.cartan α) ⊤

Tactic:
have hs : ⨆ α ∈ s, rootSpace b.cartan α = ⊤ := by
    have := b.iSup_cartan_borelLower_borelUpper_eq_top
    rw [borelLower_eq, borelUpper_eq, cartan_eq] at this
    rw [iSup_union, iSup_union]
    simpa [iSup_and, iSup_comm (ι := b.cartan → K)] using this
-- 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)}
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)) χ
⊢ (⇑χ : (a : ↥b.cartan) → K) ∈ s

Tactic:
replace hs : ⇑χ ∈ s :=
    (iSupIndep_genWeightSpace K b.cartan L).mem_of_biSup_eq_top hs χ.genWeightSpace_ne_bot
-- 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 : (⇑χ : (a : ↥b.cartan) → K) ∈ s
⊢ ¬χ.IsZero

Tactic:
simpa using hχ
-- 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 : (⇑χ : (a : ↥b.cartan) → K) ∈ s
⊢ ¬χ.IsZero

Tactic:
have hχ' : ¬ χ.IsZero := by simpa using hχ
-- 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 : (⇑χ : (a : ↥b.cartan) → K) ∈ s
hχ' : ¬χ.IsZero
⊢ (∃ (n : ι → ℕ),
      n ≠ 0 ∧
        Eq (α := ↥b.cartan → K) (⇑χ : (a : ↥b.cartan) → K) (-(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K))) ∨
    ∃ (n : ι → ℕ),
      n ≠ 0 ∧ Eq (α := ↥b.cartan → K) (⇑χ : (a : ↥b.cartan) → K) (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)

Tactic:
simp only [hχ', s, singleton_union, mem_union, mem_insert_iff, Weight.coe_eq_zero_iff,
      mem_setOf_eq, false_or] at hs

Premises used: Set.mem_union, Set.singleton_union, LieModule.Weight.coe_eq_zero_iff, Set.mem_setOf_eq, false_or, Set.mem_insert_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
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)) χ
hχ' : ¬χ.IsZero
hs :
  (∃ (n : ι → ℕ),
      n ≠ 0 ∧
        Eq (α := ↥b.cartan → K) (⇑χ : (a : ↥b.cartan) → K) (-(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K))) ∨
    ∃ (n : ι → ℕ),
      n ≠ 0 ∧ Eq (α := ↥b.cartan → K) (⇑χ : (a : ↥b.cartan) → K) (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → K)
⊢ (∃ (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

Tactic:
simpa only [← LinearMap.coe_neg, ← Weight.coe_coe, LinearMap.coe_injective.eq_iff] using hs

Premises used: LieModule.Weight.coe_coe, Function.Injective.eq_iff, LinearMap.coe_neg, LinearMap.coe_injective
-- 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 : (⇑χ : (a : ↥b.cartan) → K) ∈ s
⊢ (∃ (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

Tactic:
replace hs : (∃ n : ι → ℕ, n ≠ 0 ∧ χ.toLinear = -∑ i, n i • b.baseSupp i) ∨
               (∃ n : ι → ℕ, n ≠ 0 ∧ χ.toLinear = ∑ i, n i • b.baseSupp i) := by
    have hχ' : ¬ χ.IsZero := by simpa using hχ
    simp only [hχ', s, singleton_union, mem_union, mem_insert_iff, Weight.coe_eq_zero_iff,
      mem_setOf_eq, false_or] at hs
    simpa only [← LinearMap.coe_neg, ← Weight.coe_coe, LinearMap.coe_injective.eq_iff] using hs
-- 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
⊢ 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:
hs.symm.imp (fun ⟨n, hn₀, hn⟩ ↦ ?_) (fun ⟨n, hn₀, hn⟩ ↦ ?_)

Premises used: Or.symm, Or.imp
-- 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
h : ∃ (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 χ)

Tactic:
simpa [hn] using this n
-- 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
h : ∃ (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 χ)

Tactic:
simpa [hn] using this n
-- 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 : ι
⊢ Weight.toLinear K (↥b.cartan) L
      (↑(↑((b.baseSupportEquiv : (a : ι) → ↥b.base.support) i) : ↥root) : 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 : ι
this :
  Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(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) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (b.h' i)
⊢ IsAddTorsionFree L

Tactic:
have _i : IsAddTorsionFree L := .of_isTorsionFree K L