awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 α) ⊤
have this₁ : iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤
Tactic: have := b.iSup_cartan_borelLower_borelUpper_eq_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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] = ⊤
⊢ Eq.{u_3 + 1} (α := LieSubmodule K (↥b.cartan) L) (⨆ α ∈ s, rootSpace b.cartan α) ⊤
have 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))] =
  ⊤
Tactic: rw [borelLower_eq, borelUpper_eq, cartan_eq] at this
Cleared hypotheses: this
-- 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_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) (⨆ α ∈ s, rootSpace b.cartan α) ⊤
have 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)
  ⊤
Tactic: rw [iSup_union, iSup_union]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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)}
⊢ 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 hs : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 (γ := 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 χ)
have hs₁ : (⇑χ : (a : ↥b.cartan) → K) ∈ s
Tactic: replace hs : ⇑χ ∈ s :=
    (iSupIndep_genWeightSpace K b.cartan L).mem_of_biSup_eq_top hs χ.genWeightSpace_ne_bot
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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
have hχ' : ¬χ.IsZero
Tactic: have hχ' : ¬ χ.IsZero := by simpa using hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 ∧ 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
have 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)
Tactic: simp only [hχ', s, singleton_union, mem_union, mem_insert_iff, Weight.coe_eq_zero_iff,
      mem_setOf_eq, false_or] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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
⊢ 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 χ)
have 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
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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)
⊢ coroot (↑(↑((b.baseSupportEquiv : (a : ι) → ↥b.base.support) i) : ↥root) : Weight K (↥b.cartan) L) = b.h' i
have _i : IsAddTorsionFree L
Tactic: have _i : IsAddTorsionFree L := .of_isTorsionFree K L
-- 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
i : ι
⊢ coroot (↑(↑((b.baseSupportEquiv : (a : ι) → ↥b.base.support) i) : ↥root) : Weight K (↥b.cartan) L) = b.h' i
have suffices : 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)
Tactic: suffices b.h' i ∈ corootSpace (b.baseSupp' i) by
    have _i : IsAddTorsionFree L := .of_isTorsionFree K L
    exact (eq_coroot_of_mem_corootSpace_of_two (b.baseSupp' i).val this (by simp [baseSupp'])).symm
-- 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
i : ι
⊢ ⁅b.e i, b.f i⁆ ∈ b.cartan
have rw : Membership.mem (γ := LieSubalgebra K L) (lieSpan K L (range b.h)) (b.h i)
Tactic: rw [(b.sl2 i).lie_e_f, b.cartan_eq_lieSpan]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 : ι
⊢ 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)
have h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
Tactic: have h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan := by
    rw [(b.sl2 i).lie_e_f, b.cartan_eq_lieSpan]
    exact subset_lieSpan <| mem_range_self i
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
⊢ 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)
have h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
Tactic: have h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩ := by simp [(b.sl2 i).lie_e_f, h']
-- 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
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
⊢ 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)
have rw : 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))
  (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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 : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
⊢ 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))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)
have he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
Tactic: have he : b.e i ∈ rootSpace b.cartan (b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp⟩