awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu :
  Membership.mem (γ := 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)))
    u
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
h :
  Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ)
    (⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u

Tactic:
convert! hu
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu :
  Membership.mem (γ := 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)))
    u
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
h :
  Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      rootSpace b.cartan
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
⊢ Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ)
    (⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))

Tactic:
rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]

Premises used: iSup_subtype', Equiv.iSup_comp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu :
  Membership.mem (γ := 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)))
    u
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
⊢ Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      rootSpace b.cartan
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu :
  Membership.mem (γ := 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)))
    u
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u

Tactic:
replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
⊢ Membership.mem (γ := 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)))
    v

Tactic:
hv
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
h :
  Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ)
    (⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v

Tactic:
convert! hv
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
h :
  Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      rootSpace b.cartan
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
⊢ Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ)
    (⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))

Tactic:
rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]

Premises used: iSup_subtype', Equiv.iSup_comp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
⊢ Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      rootSpace b.cartan
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hv :
  Membership.mem (γ := 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)))
    v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v

Tactic:
replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
hv : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, LieModule.genWeightSpace L χ) ⁅u, v⁆

Tactic:
mem_biSup_genWeightSpace_of hs hu hv

Premises used: LieAlgebra.mem_biSup_genWeightSpace_of
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
hv : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v
h :
  Eq.{u_3 + 1} (α := 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)))
    (⨆ χ ∈ s, LieModule.genWeightSpace L χ)
⊢ Membership.mem (γ := 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)))
    ⁅u, v⁆

Tactic:
convert! mem_biSup_genWeightSpace_of hs hu hv

Premises used: LieAlgebra.mem_biSup_genWeightSpace_of
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
hv : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v
h :
  Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      LieModule.genWeightSpace L
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))
⊢ Eq.{u_3 + 1} (α := 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)))
    (⨆ χ ∈ s, LieModule.genWeightSpace L χ)

Tactic:
rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]

Premises used: iSup_subtype', Equiv.iSup_comp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
s : Set (↥b.cartan → R) :=
  {χ : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ χ = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : (↑{n : ι → ℕ | n ≠ 0} : Type u_1) ≃ (↑s : Type (max u_2 u_3)) :=
  Equiv.ofBijective
    (fun (n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) ↦
      Subtype.mk (p := fun (x : ↥b.cartan → R) ↦ x ∈ s)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
    ⋯
hu : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) u
hv : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) (⨆ χ ∈ s, rootSpace b.cartan χ) v
⊢ Eq.{u_3 + 1} (α := LieSubmodule R (↥b.cartan) L)
    (⨆ (x : { n : ι → ℕ // n ≠ 0 }),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑x : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
    (⨆ (x : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      LieModule.genWeightSpace L
        (↑((e : (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)) → (↑s : Type (max u_2 u_3))) x) : ↥b.cartan → R))

Tactic:
rfl