awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (Bracket.bracket (L := L) 0 (b.e i))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i : ι
v w : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v
hy : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) w
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
hw : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅w, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v + w, b.e i⁆

Tactic:
simpa using add_mem hv hw

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i : ι
t : R
v : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅t • v, b.e i⁆

Tactic:
simpa using LieSubalgebra.smul_mem _ t hv

Premises used: LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
i : ι
mem : ∀ (v : L) (hv : v ∈ range b.h), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
mem₁ : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (Bracket.bracket (L := L) 0 (b.e i))
mem₂ :
  ∀ (v w : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v →
      Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) w →
        ∀ (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆)
          (hw : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅w, b.e i⁆),
          Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v + w, b.e i⁆
mem₃ :
  ∀ (t : R) (v : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v →
      ∀ (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅t • v, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆

Tactic:
induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv

Premises used: Set.mem_range_self, zsmul_mem, LieSubalgebra.subset_lieSpan, LieAlgebra.Basis.lie_h_e, rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, 0⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u v : L
hx_1 : 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 (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u + v⁆

Tactic:
simpa using add_mem hu hv

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
t : R
u : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, t • u⁆

Tactic:
simpa using LieSubalgebra.smul_mem _ t hu

Premises used: LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u v : L
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
hv' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆
lie : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆)
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, ⁅u, v⁆⁆

Tactic:
rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]

Premises used: leibniz_lie, neg_add_eq_sub, lie_skew
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u v : L
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
hv' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆)

Tactic:
sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')

Premises used: Set.Mem, sub_mem, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u v : L
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
hv' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆)

Tactic:
exact sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')

Premises used: sub_mem, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) y
mem : ∀ (u : L) (hu : u ∈ range b.e), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, 0⁆
add :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v →
        ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆)
          (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆),
          Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u + v⁆
smul :
  ∀ (t : R) (u : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u →
      ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, t • u⁆
lie :
  ∀ (u v : L) (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u)
    (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v)
    (hu' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆)
    (hv' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, ⁅u, v⁆⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆

Tactic:
induction hy using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    rw [← mem_toSubmodule, coe_cartan_eq_span] at hx
    induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
  | zero => simp
  | add u v _ _ hu hv => simpa using add_mem hu hv
  | smul t u _ hu => simpa using LieSubalgebra.smul_mem _ t hu
  | lie u v hu hv hu' hv' =>
    rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]
    exact sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')

Premises used: leibniz_lie, zsmul_mem, neg_add_eq_sub, LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span, LieSubalgebra.subset_lieSpan, LieAlgebra.Basis.lie_h_e, rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : ↥b.cartan
y : L
hy :
  y ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (toSubmodule (lieSpan R L (range b.e)))))
obtain :
  ∀ (x : L) (hx : x ∈ b.cartan),
    ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx, y⁆ ∈
      AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (toSubmodule (lieSpan R L (range b.e)))))
⊢ ⁅x, y⁆ ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (toSubmodule (lieSpan R L (range b.e)))))

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
y : L
hy :
  y ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (toSubmodule (lieSpan R L (range b.e)))))
x : L
hx : x ∈ b.cartan
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) x hx, y⁆ ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (toSubmodule (lieSpan R L (range b.e)))))

Tactic:
simpa using b.cartan_lie_mem_lieSpan_e hx hy

Premises used: _private.0.LieAlgebra.Basis.cartan_lie_mem_lieSpan_e
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
this : b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤
⊢ iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
suffices : b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤
⊢ iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
suffices b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤ by simpa
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤

Tactic:
eq_top_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
refine :
  ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) ⊤ x),
    x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤

Tactic:
refine eq_top_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) ⊤ x
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x

Tactic:
simp [b.span_ef]

Premises used: LieAlgebra.Basis.span_ef
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
hx : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) ⊤ x
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x

Tactic:
replace hx : x ∈ lieSpan R L (range b.e ∪ range b.f) := by simp [b.span_ef]
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u : L
hu : u ∈ range b.e ∪ range b.f
mem : ∀ (hu : u ∈ range b.e), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
mem₁ : ∀ (hu : u ∈ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rcases (mem_union _ _ _).mpr hu with hu | hu

Premises used: Set.mem_union, Iff.mpr
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u : L
hu_1 : u ∈ range b.e ∪ range b.f
hu : u ∈ range b.e
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
LieSubmodule.mem_sup_right <| subset_lieSpan hu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u : L
hu_1 : u ∈ range b.e ∪ range b.f
hu : u ∈ range b.e
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_right <| subset_lieSpan hu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u : L
hu_1 : u ∈ range b.e ∪ range b.f
hu : u ∈ range b.f
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.subset_lieSpan, LieSubmodule.mem_sup_left
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u : L
hu_1 : u ∈ range b.e ∪ range b.f
hu : u ∈ range b.f
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu

Premises used: LieSubmodule.mem_sup_right, LieSubalgebra.subset_lieSpan, LieSubmodule.mem_sup_left
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
⊢ 0 ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ u + v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
add_mem hu hv

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ u + v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact add_mem hu hv

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ t • u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ t • u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ∃ yc ∈ b.cartan,
    ∃ (yl : L),
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) yl ∧
        ∃ (yu : L), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) yu ∧ yc + yl + yu = u

Tactic:
simpa [LieSubmodule.mem_sup] using hu

Premises used: LieSubmodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hu : u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
lie :
  ∀ (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),
    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),
        ⁅yc + yl + yu, v⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅u, v⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ b.cartan) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using hu

Premises used: LieAlgebra.Basis.e, LieAlgebra.Basis.cartan, LieAlgebra.Basis.f, LieSubalgebra.lieSpan, Set.range, rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x v : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
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 ∈ b.cartan,
    ∃ (zl : L),
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.f)) zl ∧
        ∃ (zu : L), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) zu ∧ zc + zl + zu = v

Tactic:
simpa [LieSubmodule.mem_sup] using hv

Premises used: LieSubmodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x v : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) v
hv : v ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
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
lie :
  ∀ (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),
    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 + yl + yu, zc + zl + zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc + yl + yu, v⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ b.cartan) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using hv

Premises used: LieAlgebra.Basis.e, LieAlgebra.Basis.cartan, LieAlgebra.Basis.f, LieSubalgebra.lieSpan, Set.range, rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
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⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ + ⁅yu, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc + yl + yu, zc + zl + zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
simp only [lie_add, add_lie, ← add_assoc]

Premises used: add_assoc, lie_add, add_lie