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
refine_1 :
  ∀ (n₁ n₂ : (↑{n : ι → ℕ | n ≠ 0} : Type u_1))
    (h :
      Eq (α := (↑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))
              ⋯)
          n₁)
        ((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))
              ⋯)
          n₂)),
    n₁ = n₂
refine_2 :
  ∀ (χ : (↑s : Type (max u_2 u_3))),
    ∃ (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
      (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))
              ⋯)
          a =
        χ
⊢ 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:
refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
-- 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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
refine_1 : ∀ (i : ι), (↑n₁ : ι → ℕ) i = (↑n₂ : ι → ℕ) i
⊢ n₁ = n₂

Tactic:
ext i
-- 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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
i : ι
⊢ LinearIndependent ℕ b.baseSupp

Tactic:
have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
-- 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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
i : ι
this : LinearIndependent ℕ b.baseSupp
⊢ (↑n₁ : ι → ℕ) i = (↑n₂ : ι → ℕ) i

Tactic:
Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i

Premises used: Fintype.linearIndependent_iffₛ, Iff.mp, Subtype.val
-- 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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
i : ι
this : LinearIndependent ℕ b.baseSupp
refine_1 :
  Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i)
    (∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i)
⊢ (↑n₁ : ι → ℕ) i = (↑n₂ : ι → ℕ) i

Tactic:
refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i

Premises used: Fintype.linearIndependent_iffₛ, Iff.mp, Subtype.val
-- 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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
i : ι
this : LinearIndependent ℕ b.baseSupp
refine_1 :
  ∀ (v : ↥b.cartan),
    Eq.{u_2 + 1} (α := R) ((∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
      ((∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
⊢ Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i)
    (∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i)

Tactic:
ext v
-- 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_1 : 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_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)))
    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_1
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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := (↑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)) ⋯)
      n₁)
    ((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)) ⋯)
      n₂)
i : ι
this : LinearIndependent ℕ b.baseSupp
v : ↥b.cartan
refine_1 :
  ∀
    (h :
      Eq (α := ↥b.cartan → R)
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n₁ : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n₂ : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
    (i : ι) (this : LinearIndependent ℕ b.baseSupp) (v : ↥b.cartan),
    Eq.{u_2 + 1} (α := R) ((∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
      ((∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
⊢ Eq.{u_2 + 1} (α := R) ((∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
    ((∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)

Tactic:
rw [Subtype.mk.injEq] at h

Premises used: Subtype.mk.injEq
-- 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_1 : 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_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)))
    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_1
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 : ι → ℕ | n ≠ 0} : Type u_1)
h :
  Eq (α := ↥b.cartan → R)
    (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n₁ : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
    (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) ((↑n₂ : ι → ℕ) i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
i : ι
this : LinearIndependent ℕ b.baseSupp
v : ↥b.cartan
⊢ Eq.{u_2 + 1} (α := R) ((∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)
    ((∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i : (a : ↥b.cartan) → R) v : R)

Tactic:
simpa using congr_fun h v

Premises used: congr_fun
-- 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
χ : (↑s : Type (max u_2 u_3))
h :
  (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)) ⋯)
      (Subtype.mk (p := fun (x : ι → ℕ) ↦ Membership.mem (γ := Set (ι → ℕ)) {n : ι → ℕ | n ≠ 0} x)
        (Exists.choose (p := fun (n : ι → ℕ) ↦
          n ≠ 0 ∧ (↑χ : ↥b.cartan → R) = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
        ⋯) =
    χ
⊢ ∃ (a : (↑{n : ι → ℕ | n ≠ 0} : Type u_1)),
    (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))
            ⋯)
        a =
      χ

Tactic:
use ⟨χ.property.choose, χ.property.choose_spec.1⟩
-- 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
χ : (↑s : Type (max u_2 u_3))
h :
  ∀ (i : ↥b.cartan),
    (↑((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))
                  ⋯)
              (Subtype.mk (p := fun (x : ι → ℕ) ↦ Membership.mem (γ := Set (ι → ℕ)) {n : ι → ℕ | n ≠ 0} x)
                (Exists.choose (p := fun (n : ι → ℕ) ↦
                  n ≠ 0 ∧ (↑χ : ↥b.cartan → R) = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
                ⋯)) :
          ↥b.cartan → R)
        i =
      (↑χ : ↥b.cartan → R) i
⊢ (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)) ⋯)
      (Subtype.mk (p := fun (x : ι → ℕ) ↦ Membership.mem (γ := Set (ι → ℕ)) {n : ι → ℕ | n ≠ 0} x)
        (Exists.choose (p := fun (n : ι → ℕ) ↦
          n ≠ 0 ∧ (↑χ : ↥b.cartan → R) = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
        ⋯) =
    χ

Tactic:
ext i
-- 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
χ : (↑s : Type (max u_2 u_3))
i : ↥b.cartan
⊢ (↑((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))
                ⋯)
            (Subtype.mk (p := fun (x : ι → ℕ) ↦ Membership.mem (γ := Set (ι → ℕ)) {n : ι → ℕ | n ≠ 0} x)
              (Exists.choose (p := fun (n : ι → ℕ) ↦
                n ≠ 0 ∧ (↑χ : ↥b.cartan → R) = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)) ⋯)
              ⋯)) :
        ↥b.cartan → R)
      i =
    (↑χ : ↥b.cartan → R) i

Tactic:
simpa using congr_fun χ.property.choose_spec.2.symm i

Premises used: Exists.choose_spec, And.right, congr_fun, Eq.symm, Subtype.property
-- 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)
    (⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R)))
    u

Tactic:
hu