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
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)) ⋯
have 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))
            sorry)
        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))
            sorry)
        n₂)),
  n₁ = n₂
Tactic: refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
-- 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
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₂
⊢ 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)) ⋯
have 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))
            sorry)
        a =
      χ
Tactic: refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
-- 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
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₂)
⊢ n₁ = n₂
have refine_1 : ∀ (i : ι), (↑n₁ : ι → ℕ) i = (↑n₂ : ι → ℕ) i
Tactic: ext i
-- 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
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 : ι
⊢ (↑n₁ : ι → ℕ) i = (↑n₂ : ι → ℕ) i
have this : LinearIndependent ℕ b.baseSupp
Tactic: have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
-- 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
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
have refine_1 : Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i)
  (∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i)
Tactic: refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ 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
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
⊢ Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, (↑n₁ : ι → ℕ) i • b.baseSupp i)
    (∑ i : ι, (↑n₂ : ι → ℕ) i • b.baseSupp i)
have 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)
Tactic: ext v
-- 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
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
⊢ 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)
have 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)
Tactic: rw [Subtype.mk.injEq] at h
Cleared hypotheses: h, i, this, v
-- 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
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))
⊢ ∃ (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 =
      χ
have 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)) sorry)
    (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)) sorry)
      sorry) =
  χ
Tactic: use ⟨χ.property.choose, χ.property.choose_spec.1⟩
-- 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
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))
⊢ (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)) ⋯)
        ⋯) =
    χ
have 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))
                sorry)
            (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)) sorry)
              sorry)) :
        ↥b.cartan → R)
      i =
    (↑χ : ↥b.cartan → R) i
Tactic: ext 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
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
have 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)))
Tactic: convert! 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
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) (⨆ χ ∈ 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)))
have 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)))
Tactic: rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]
-- 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
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, v⁆
have hu₁ : 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
Cleared hypotheses: hu