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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yu, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₄ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₄ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₅ : ⁅yu, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₄ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₅ : ⁅yu, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₆ : ⁅yc, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₄ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₅ : ⁅yu, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₆ : ⁅yc, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₇ : ⁅yl, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem
-- 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
x yc : L
hyc : yc ∈ b.cartan
yl : L
hyl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl
yu : L
hyu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (yc + yl + yu)
hu : yc + yl + yu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ b.cartan
zl : L
hzl : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl
zu : L
hzu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) (zc + zl + zu)
hv : zc + zl + zu ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie : ⁅yc, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₁ : ⁅yl, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₂ : ⁅yu, zc⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₃ : ⁅yc, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₄ : ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₅ : ⁅yu, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₆ : ⁅yc, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie₇ : ⁅yl, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₈ : ⁅yu, zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: repeat apply add_mem