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
i : Fin (Nat.succ 0).succ.succ
0 :
  ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
1 :
  ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] i ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      i
have 2 : ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) ≤
  ![rootSpace b.cartan 0,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
⊢ iSupIndep
    ![rootSpace b.cartan 0,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
have set : let 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))),
  iSupIndep
    ![rootSpace b.cartan 0, U,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
Tactic: set U := ⨆ (n : ι → ℕ) (_ : n ≠ 0), rootSpace b.cartan (∑ i, n i • (-b.baseSupp) i) with hU
-- 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))
⊢ iSupIndep
    ![rootSpace b.cartan 0, U,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
have set : let 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))),
  iSupIndep ![rootSpace b.cartan 0, U, V]
Tactic: set V := ⨆ (n : ι → ℕ) (_ : n ≠ 0), rootSpace b.cartan (∑ i, n i • b.baseSupp i) with hV
-- 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))
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hs0 : let s0 : Set (↥b.cartan → R) := {0};
s0 = {0}
Tactic: set s0 : Set (b.cartan → R) := {0} with hs0
-- 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}
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hsU : let sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)};
sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
Tactic: set sU : Set (b.cartan → R) := {f | ∃ n : ι → ℕ, n ≠ 0 ∧ f = ∑ i, n i • (-b.baseSupp) i} with 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)}
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hsV : let sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)};
sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
Tactic: set sV : Set (b.cartan → R) := {f | ∃ n : ι → ℕ, n ≠ 0 ∧ f = ∑ i, n i • b.baseSupp i} with 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)}
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
Tactic: have hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i := by simp [hs0]
-- 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
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
Tactic: have hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i := by
    simp only [hU, hsU, mem_setOf_eq, iSup_exists, iSup_and, iSup_comm (ι := b.cartan → R),
      iSup_iSup_eq_left, LinearMap.coe_sum, LinearMap.coe_smul]
-- 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
⊢ iSupIndep ![rootSpace b.cartan 0, U, V]
have hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
Tactic: have hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i := by
    simp only [hV, hsV, mem_setOf_eq, iSup_exists, iSup_and, iSup_comm (ι := b.cartan → R),
      iSup_iSup_eq_left, LinearMap.coe_sum, LinearMap.coe_smul]
-- 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
this : ∀ g ∈ sU, g ≠ 0
⊢ Disjoint s0 sU
have refine : ∀ (f : ↥b.cartan → R) (hf : f ∈ s0) (g : ↥b.cartan → R) (hg : g ∈ sU), f ≠ g
Tactic: refine Set.disjoint_iff_forall_ne.mpr fun f hf g hg ↦ ?_
-- 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
this : ∀ g ∈ sU, g ≠ 0
f : ↥b.cartan → R
hf : f ∈ s0
g : ↥b.cartan → R
hg : g ∈ sU
⊢ f ≠ g
have obtain : ∀ (hf : 0 ∈ s0), 0 ≠ g
Tactic: obtain ⟨rfl⟩ : f = 0 := by simpa [hs0] using hf
Cleared hypotheses: f, hf
-- 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
⊢ Disjoint s0 sU
have suffices : ∀ g ∈ sU, g ≠ 0
Tactic: suffices ∀ g ∈ sU, g ≠ 0 by
      refine Set.disjoint_iff_forall_ne.mpr fun f hf g hg ↦ ?_
      obtain ⟨rfl⟩ : f = 0 := by simpa [hs0] using hf
      exact (this _ hg).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
g : ↥b.cartan → R
hg : g ∈ sU
contra : g = 0
⊢ False
have obtain : ∀ (n : ι → ℕ) (hn : n ≠ 0) (hg : -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU)
  (contra : Eq (α := ↥b.cartan → R) (-(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)) 0), False
Tactic: obtain ⟨n, hn, rfl⟩ : ∃ n : ι → ℕ, n ≠ 0 ∧ g = -∑ i, n i • b.baseSupp i := by
      simpa [hsU] using hg
Cleared hypotheses: g, hg, contra