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 ι
i : ι
x : ↥b.cartan
this :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((b.symm.baseSupp i : (a : ↥b.symm.cartan) → R) x : R) (b.symm.e i) =
    ⁅x, b.symm.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((-b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.f i) = ⁅x, b.f i⁆

Tactic:
simp only [symm_cartan, symm_baseSupp, Pi.neg_apply, symm_e] at this

Premises used: LieAlgebra.Basis.symm_e, LieAlgebra.Basis.symm_baseSupp, Pi.neg_apply, LieAlgebra.Basis.symm_cartan
-- 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 ι
i : ι
x : ↥b.cartan
this : HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((-b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.f i) = ⁅x, b.f i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((-b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.f i) = ⁅x, b.f i⁆

Tactic:
this
-- 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 ι
i : ι
x : ↥b.cartan
this : HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((-b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.f i) = ⁅x, b.f i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((-b.baseSupp i : (a : ↥b.cartan) → R) x : R) (b.f i) = ⁅x, b.f i⁆

Tactic:
exact this
-- 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 : L
hx : x ∈ b.borelUpper
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x

Tactic:
simpa [borelUpper] using hx

Premises used: LieAlgebra.Basis.borelUpper
-- 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 : L
hx : x ∈ b.borelUpper
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x

Tactic:
replace hx : x ∈ lieSpan R L (range b.e) := by simpa [borelUpper] using hx
-- 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 : L
hu : u ∈ range b.e
mem :
  ∀ (i : ι),
    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)))
      (b.e i)
⊢ 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

Tactic:
obtain ⟨i, rfl⟩ := hu

Premises used: 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 : L
i : ι
mem :
  Membership.mem (γ := LieSubmodule R (↥b.cartan) L)
    (⨆ (_ : Ne (α := ι → ℕ) (Pi.single (M := fun (j : ι) ↦ ℕ) i 1) 0),
      rootSpace b.cartan
        (∑ i_1 : ι,
          HSMul.hSMul (α := ℕ) (β := (a : ↥b.cartan) → R) (Pi.single (M := fun (j : ι) ↦ ℕ) i 1 i_1 : ℕ)
            (⇑(b.baseSupp i_1) : (a : ↥b.cartan) → R)))
    (b.e i)
⊢ 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)))
    (b.e i)

Tactic:
apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)

Premises used: Pi.single, LieSubmodule.mem_iSup_of_mem, OfNat.ofNat
-- 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 : L
i : ι
mem :
  ∀ (a : L) (b_1 : a ∈ b.cartan),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HSub.hSub (α := End R L) ((LieModule.toEnd R L L : (a : L) → End R L) a : End R L)
                  (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := End R L)
                    (∑ x : ι,
                      HMul.hMul (α := R) (β := R) ((↑(Pi.single (M := fun (j : ι) ↦ ℕ) i 1 x) : R) : R)
                        ((b.baseSupp x : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (a : L) ↦ a ∈ b.cartan) a b_1) : R))
                    1) ^
                k :
              (a : L) → L)
            (b.e i) :
          L)
        (0 : L)
⊢ Membership.mem (γ := LieSubmodule R (↥b.cartan) L)
    (⨆ (_ : Ne (α := ι → ℕ) (Pi.single (M := fun (j : ι) ↦ ℕ) i 1) 0),
      rootSpace b.cartan
        (∑ i_1 : ι,
          HSMul.hSMul (α := ℕ) (β := (a : ↥b.cartan) → R) (Pi.single (M := fun (j : ι) ↦ ℕ) i 1 i_1 : ℕ)
            (⇑(b.baseSupp i_1) : (a : ↥b.cartan) → R)))
    (b.e i)

Tactic:
simp only [ne_eq, Pi.single_eq_zero_iff, one_ne_zero, not_false_eq_true, nsmul_eq_mul, iSup_pos,
      LieModule.mem_genWeightSpace, Finset.sum_apply, Pi.mul_apply, Pi.natCast_apply,
      Subtype.forall, toEnd_mk]

Premises used: Pi.mul_apply, LieModule.mem_genWeightSpace, Finset.sum_apply, LieSubalgebra.toEnd_mk, Subtype.forall, iSup_pos, Pi.natCast_apply, ne_eq, nsmul_eq_mul, Pi.single_eq_zero_iff, one_ne_zero, not_false_eq_true
-- 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 : L
i : ι
y : L
hy : y ∈ b.cartan
⊢ Eq (α := L)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := End R L) ((LieModule.toEnd R L L : (a : L) → End R L) y : End R L)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := End R L)
                (∑ x : ι,
                  HMul.hMul (α := R) (β := R) ((↑(Pi.single (M := fun (j : ι) ↦ ℕ) i 1 x) : R) : R)
                    ((b.baseSupp x : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (a : L) ↦ a ∈ b.cartan) y hy) : R))
                1))
            1 :
          (a : L) → L)
        (b.e i) :
      L)
    (0 : L)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- 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 : L
i : ι
⊢ ∀ (a : L) (b_1 : a ∈ b.cartan),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HSub.hSub (α := End R L) ((LieModule.toEnd R L L : (a : L) → End R L) a : End R L)
                  (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := End R L)
                    (∑ x : ι,
                      HMul.hMul (α := R) (β := R) ((↑(Pi.single (M := fun (j : ι) ↦ ℕ) i 1 x) : R) : R)
                        ((b.baseSupp x : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (a : L) ↦ a ∈ b.cartan) a b_1) : R))
                    1) ^
                k :
              (a : L) → L)
            (b.e i) :
          L)
        (0 : L)

Tactic:
exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
-- 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 : 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)))
    0

Tactic:
simp
-- 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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) y
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)))
    x_1
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)))
    y
⊢ 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)))
    (x_1 + y)

Tactic:
add_mem hu hv

Premises used: AddMemClass.add_mem
-- 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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) y
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)))
    x_1
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)))
    y
⊢ 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)))
    (x_1 + y)

Tactic:
exact add_mem hu hv

Premises used: AddMemClass.add_mem
-- 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 : L
t : R
x_1 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x_1
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)))
    x_1
⊢ 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)))
    (t • x_1)

Tactic:
SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- 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 : L
t : R
x_1 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x_1
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)))
    x_1
⊢ 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)))
    (t • x_1)

Tactic:
exact SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
⊢ n₁ + n₂ ≠ 0

Tactic:
simp [hn₁]
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
refine :
  HAdd.hAdd (α := ↥b.cartan → R) (⇑(∑ i : ι, n₁ i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n₂ i • b.baseSupp i) : (a : ↥b.cartan) → R) =
    (⇑(∑ i : ι, (n₁ + n₂) i • b.baseSupp i) : (a : ↥b.cartan) → R)
⊢ HAdd.hAdd (α := ↥b.cartan → R) (⇑(∑ i : ι, n₁ i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n₂ i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈
    s

Tactic:
refine ⟨n₁ + n₂, by simp [hn₁], ?_⟩
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
h :
  ∀ (x : ↥b.cartan),
    HAdd.hAdd (α := ↥b.cartan → R) (β := ↥b.cartan → R) (⇑(∑ i : ι, n₁ i • b.baseSupp i) : (a : ↥b.cartan) → R)
        (⇑(∑ i : ι, n₂ i • b.baseSupp i) : (a : ↥b.cartan) → R) x =
      (∑ i : ι, (n₁ + n₂) i • b.baseSupp i : (a : ↥b.cartan) → R) x
⊢ HAdd.hAdd (α := ↥b.cartan → R) (⇑(∑ i : ι, n₁ i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n₂ i • b.baseSupp i) : (a : ↥b.cartan) → R) =
    (⇑(∑ i : ι, (n₁ + n₂) i • b.baseSupp i) : (a : ↥b.cartan) → R)

Tactic:
ext
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
x_1 : ↥b.cartan
⊢ HAdd.hAdd (α := ↥b.cartan → R) (β := ↥b.cartan → R) (⇑(∑ i : ι, n₁ i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n₂ i • b.baseSupp i) : (a : ↥b.cartan) → R) x_1 =
    (∑ i : ι, (n₁ + n₂) i • b.baseSupp i : (a : ↥b.cartan) → R) x_1

Tactic:
simp [add_smul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul
-- 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)}
⊢ ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s

Tactic:
have hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s := by
      rintro - ⟨n₁, hn₁, rfl⟩ - ⟨n₂, hn₂, rfl⟩
      refine ⟨n₁ + n₂, by simp [hn₁], ?_⟩
      ext; simp [add_smul, Finset.sum_add_distrib]
-- 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
n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)
h :
  ∀ (x : ↥b.cartan),
    Eq.{u_2 + 1} (α := R)
      ((∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) x : R)
      ((∑ i : ι, (↑n : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) x : R)
⊢ Eq (α := ↥b.cartan → R)
    (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
    (⇑(∑ i : ι, (↑n : ι → ℕ) i • b.baseSupp i) : (a : ↥b.cartan) → R)

Tactic:
ext
-- 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
n : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)
x_1 : ↥b.cartan
⊢ Eq.{u_2 + 1} (α := R)
    ((∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)) x_1 : R)
    ((∑ i : ι, (↑n : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) x_1 : R)

Tactic:
simp
-- 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
⊢ Bijective (β := (↑s : Type (max u_2 u_3))) 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)) ⋯

Tactic:
⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩

Premises used: And.intro, Function.Bijective