awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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 : V ⊔ rootSpace b.cartan 0 = (⨆ x ∈ sV, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ s0, LieModule.genWeightSpace L x
h₁ :
  V ⊔ ⨆ i ∈ s0, LieModule.genWeightSpace L i =
    (⨆ x ∈ sV, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ s0, LieModule.genWeightSpace L x
⊢ V ⊔ rootSpace b.cartan 0 = ⨆ i ∈ sV ∪ s0, LieModule.genWeightSpace L i
have h₂ : Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
  ((⨆ i ∈ sV, LieModule.genWeightSpace L i) ⊔ ⨆ i ∈ s0, LieModule.genWeightSpace L i)
  ((⨆ x ∈ sV, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ s0, LieModule.genWeightSpace L x)
Tactic: rw [iSup_union, hs0', hsV']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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)
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have h₁ : Disjoint U (V ⊔ rootSpace b.cartan 0)
Tactic: have h₁ : Disjoint U (V ⊔ rootSpace b.cartan 0) := by
    convert! key.disjoint_biSup_biSup (hUV.union_right hU0.symm)
    rw [iSup_union, hs0', hsV']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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)
have h : rootSpace b.cartan 0 ⊔ U = ⨆ i ∈ s0 ∪ sU, LieModule.genWeightSpace L i
Tactic: convert! key.disjoint_biSup_biSup (Disjoint.union_left hV0 hUV).symm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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)
⊢ rootSpace b.cartan 0 ⊔ U = ⨆ i ∈ s0 ∪ sU, LieModule.genWeightSpace L i
have h : rootSpace b.cartan 0 ⊔ U = (⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x
Tactic: rw [iSup_union, hs0', hsU']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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 : rootSpace b.cartan 0 ⊔ U = (⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x
⊢ rootSpace b.cartan 0 ⊔ U = ⨆ i ∈ s0 ∪ sU, LieModule.genWeightSpace L i
have h₂ : (⨆ i ∈ s0, LieModule.genWeightSpace L i) ⊔ U =
  (⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x
Tactic: rw [iSup_union, hs0', hsU']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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 : rootSpace b.cartan 0 ⊔ U = (⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x
h₂ :
  (⨆ i ∈ s0, LieModule.genWeightSpace L i) ⊔ U =
    (⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x
⊢ rootSpace b.cartan 0 ⊔ U = ⨆ i ∈ s0 ∪ sU, LieModule.genWeightSpace L i
have h₃ : Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
  ((⨆ i ∈ s0, LieModule.genWeightSpace L i) ⊔ ⨆ i ∈ sU, LieModule.genWeightSpace L i)
  ((⨆ x ∈ s0, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sU, LieModule.genWeightSpace L x)
Tactic: rw [iSup_union, hs0', hsU']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
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)
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have h₂ : 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']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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
⊢ b.cartan.IsCartanSubalgebra
have rw : b.cartan.toLieSubmodule = rootSpace b.cartan 0
Tactic: rw [← eq_rootSpace_zero_iff_isCartan, b.cartan_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
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
⊢ b.cartan.IsCartanSubalgebra
have rw₁ : rootSpace b.cartan 0 = rootSpace b.cartan 0
Tactic: rw [← eq_rootSpace_zero_iff_isCartan, b.cartan_eq]
-- 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
i : ι
⊢ ↥(root : Finset (Weight K (↥b.cartan) L))
have refine_1 : Ne (α := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) ⊥
Tactic: refine ⟨⟨b.baseSupp i, ?_⟩, ?_⟩
-- 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
i : ι
refine_1 : Ne (α := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) ⊥
⊢ ↥(root : Finset (Weight K (↥b.cartan) L))
have 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' := sorry }
Tactic: refine ⟨⟨b.baseSupp i, ?_⟩, ?_⟩
-- 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
i : ι
⊢ Ne (α := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) ⊥
have refine_1 : ∃ (x : L) (_ :
  Membership.mem (γ := LieSubmodule K (↥b.cartan) L) (genWeightSpace L (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)) x),
  ¬x = 0
Tactic: simp only [LieSubmodule.eq_bot_iff, ne_eq, not_forall]
-- 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
e : ι ≃ (↑(range b.baseSupp' : Set ↥(root : Finset (Weight K (↥b.cartan) L))) : Type (max u_2 u_3)) :=
  Equiv.ofInjective b.baseSupp' ⋯
⊢ 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)))
have 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))))
Tactic: rw [LinearIndepOn, ← linearIndependent_equiv e]
-- 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))
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)
have 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)
Tactic: simp_rw [← Submodule.span_nat_eq_addSubmonoidClosure, Submodule.mem_toAddSubmonoid]
-- 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))
⊢ 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 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)
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