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
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
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! hv
-- 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
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) (⨆ χ ∈ 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
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)))
    ⁅u, v⁆
have hv₁ : 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
Cleared hypotheses: hv
-- 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
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)
    (⨆ (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 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 χ)
Tactic: convert! mem_biSup_genWeightSpace_of hs hu hv
-- 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
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)
    (⨆ (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 χ)
have 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))
Tactic: rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]
-- 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 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x
⊢ 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
have mem : ∀ (u : L) (hu : u ∈ range b.e),
  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: induction hx using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)
    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]
    exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
  | zero => simp
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    let s : Set (b.cartan → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    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]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
Cleared hypotheses: hx
-- 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 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.e),
    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
⊢ 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
have zero : 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: induction hx using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)
    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]
    exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
  | zero => simp
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    let s : Set (b.cartan → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    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]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
Cleared hypotheses: hx
-- 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
⊢ b.borelUpper ≤
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
have intro : ∀ ⦃x : L⦄,
  x ∈ b.borelUpper →
    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
Tactic: classical
  intro x hx
  replace hx : x ∈ lieSpan R L (range b.e) := by simpa [borelUpper] using hx
  induction hx using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)
    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]
    exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
  | zero => simp
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    let s : Set (b.cartan → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    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]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
-- 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
intro intro₁ :
  ∀ ⦃x : L⦄ (hx : x ∈ b.borelUpper),
    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
⊢ b.borelUpper ≤
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
have intro₂ : ∀ ⦃x : L⦄ (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x),
  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
Tactic: classical
  intro x hx
  replace hx : x ∈ lieSpan R L (range b.e) := by simpa [borelUpper] using hx
  induction hx using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)
    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]
    exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
  | zero => simp
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    let s : Set (b.cartan → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    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]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
i : Fin (Nat.succ 0).succ.succ
⊢ ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] i ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      i
have 0 : ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) ≤
  ![rootSpace b.cartan 0,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
i : Fin (Nat.succ 0).succ.succ
0 :
  ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] i ≤
    ![rootSpace b.cartan 0,
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
        ⨆ (n : ι → ℕ),
          ⨆ (_ : n ≠ 0),
            rootSpace b.cartan
              (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
      i
have 1 : ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) ≤
  ![rootSpace b.cartan 0,
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R)),
      ⨆ (n : ι → ℕ),
        ⨆ (_ : n ≠ 0),
          rootSpace b.cartan
            (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i