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 ι
i : ι
x : L
t : R
u : L
hu : u ∈ b.cartan
hv' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hx : t • u ∈ b.cartan
smul :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (t • Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₁ :
  HSMul.hSMul (β := R) t
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) •
      b.e i =
    ⁅t • u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆
have smul₂ : t •
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
  ⁅t • u, b.e i⁆
Tactic: rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
-- 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 ι
i : ι
x : L
t : R
u : L
hu : u ∈ b.cartan
hv' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hx : t • u ∈ b.cartan
smul :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (t • Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₁ :
  HSMul.hSMul (β := R) t
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) •
      b.e i =
    ⁅t • u, b.e i⁆
smul₂ :
  t •
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆
have smul₃ : t • ⁅u, b.e i⁆ = ⁅t • u, b.e i⁆
Tactic: rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
-- 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 ι
i : ι
x : L
t : R
u : L
hu : u ∈ b.cartan
hv' :
  ∀ (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
hx : t • u ∈ b.cartan
smul :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (t • Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₁ :
  HSMul.hSMul (β := R) t
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) •
      b.e i =
    ⁅t • u, b.e i⁆
smul₂ :
  t •
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hu) : R) (b.e i) =
    ⁅t • u, b.e i⁆
smul₃ : t • ⁅u, b.e i⁆ = ⁅t • u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆
have smul₄ : t • ⁅u, b.e i⁆ = t • ⁅u, b.e i⁆
Tactic: rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
-- 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 ι
i : ι
x : L
hx : x ∈ b.cartan
hx' : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆
have mem : ∀ (u : L) (hu : u ∈ range b.h) (hx : u ∈ b.cartan),
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
    ⁅u, b.e i⁆
Tactic: induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
Cleared hypotheses: hx, 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 ι
i : ι
x : L
hx : x ∈ b.cartan
hx' : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.h) (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆
have zero : ∀ (hx : 0 ∈ b.cartan),
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) 0 hx) : R) (b.e i) =
    Bracket.bracket (L := L) 0 (b.e i)
Tactic: induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
Cleared hypotheses: hx, 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 ι
i : ι
x : L
hx : x ∈ b.cartan
hx' : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.h) (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
zero :
  ∀ (hx : 0 ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) 0 hx) : R) (b.e i) =
      Bracket.bracket (L := L) 0 (b.e i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆
have add : ∀ (u v : L) (hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u)
  (hv : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v)
  (hu' :
    ∀ (hx : u ∈ b.cartan),
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
          ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
        ⁅u, b.e i⁆)
  (hv' :
    ∀ (hx : v ∈ b.cartan),
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
          ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
        ⁅v, b.e i⁆)
  (hx : u + v ∈ b.cartan),
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
    ⁅u + v, b.e i⁆
Tactic: induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
Cleared hypotheses: hx, 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 ι
i : ι
x : L
hx : x ∈ b.cartan
hx' : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.h) (hx : u ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
      ⁅u, b.e i⁆
zero :
  ∀ (hx : 0 ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) 0 hx) : R) (b.e i) =
      Bracket.bracket (L := L) 0 (b.e i)
add :
  ∀ (u v : L) (hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u)
    (hv : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v)
    (hu' :
      ∀ (hx : u ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
          ⁅u, b.e i⁆)
    (hv' :
      ∀ (hx : v ∈ b.cartan),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R)
            ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) v hx) : R) (b.e i) =
          ⁅v, b.e i⁆)
    (hx : u + v ∈ b.cartan),
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (u + v) hx) : R) (b.e i) =
      ⁅u + v, b.e i⁆
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx) : R) (b.e i) =
    ⁅x, b.e i⁆
have smul : ∀ (t : R) (u : L) (hu : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) u)
  (hv' :
    ∀ (hx : u ∈ b.cartan),
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
          ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) u hx) : R) (b.e i) =
        ⁅u, b.e i⁆)
  (hx : t • u ∈ b.cartan),
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((b.baseSupp i : (a : ↥b.cartan) → R) (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) (t • u) hx) : R) (b.e i) =
    ⁅t • u, b.e i⁆
Tactic: induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]
Cleared hypotheses: hx, hx'
-- 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 ι
i : ι
x : ↥b.cartan
⊢ 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⁆
have 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⁆
Tactic: have := b.symm.baseSupp_apply_smul_e i x
-- 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 ι
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⁆
have 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⁆
Tactic: simp only [symm_cartan, symm_baseSupp, Pi.neg_apply, symm_e] at this
Cleared hypotheses: this
-- 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 : 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
have hx₁ : 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
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 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
have 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)
Tactic: obtain ⟨i, rfl⟩ := hu
Cleared hypotheses: u, 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 : L
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)
have 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)
Tactic: apply LieSubmodule.mem_iSup_of_mem (Pi.single i 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 : L
i : ι
⊢ 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)
have 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)
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]
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
⊢ 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
have 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)
Tactic: refine ⟨n₁ + n₂, by simp [hn₁], ?_⟩
-- 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)}
n₁ : ι → ℕ
hn₁ : n₁ ≠ 0
n₂ : ι → ℕ
hn₂ : n₂ ≠ 0
⊢ 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)
have 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
Tactic: ext
-- 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)}
⊢ 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 hs : ∀ χ₁ ∈ 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]
-- 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 ≠ 0} : Type u_1)
⊢ 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)
have 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)
Tactic: ext