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 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⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆
have zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, 0⁆
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')
Cleared hypotheses: hy
-- 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 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⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆
have 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⁆
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')
Cleared hypotheses: hy
-- 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 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⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆
have 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⁆
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')
Cleared hypotheses: hy
-- 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 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⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆
have 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⁆⁆
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')
Cleared hypotheses: hy
-- 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 : ↥b.cartan
y : L
hy :
  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)))))
have 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)))))
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- 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
⊢ iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤
have suffices : b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤
Tactic: suffices b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤ by simpa
-- 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
⊢ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤
have refine : ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) ⊤ x),
  x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: refine eq_top_iff.mpr fun x 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
x : L
hx : Membership.mem (γ := LieSubmodule R (↥b.cartan) L) ⊤ x
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have hx₁ : 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]
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
x u : L
hu : u ∈ range b.e ∪ range b.f
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have mem : ∀ (hu : u ∈ range b.e), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: rcases (mem_union _ _ _).mpr hu with hu | 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
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
⊢ u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have mem₁ : ∀ (hu : u ∈ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: rcases (mem_union _ _ _).mpr hu with hu | 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
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
have 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
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
Cleared hypotheses: u, hx, 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
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
⊢ ⁅yc + yl + yu, v⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have 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
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
Cleared hypotheses: v, hy, 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
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 + yl + yu, zc + zl + zu⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have 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
Tactic: simp only [lie_add, add_lie, ← add_assoc]
-- 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⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅yl, zu⁆ ∈
  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⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ + ⁅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: 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⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ ∈
  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⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅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⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yl, zu⁆ ∈ 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⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅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
lie :
  ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ + ⁅yu, zl⁆ + ⁅yc, zu⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie₁ : ⁅yc, zu⁆ ∈ 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⁆ ∈
    b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
have lie : ⁅yc, zc⁆ + ⁅yl, zc⁆ + ⁅yu, zc⁆ + ⁅yc, zl⁆ + ⁅yl, zl⁆ ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Tactic: apply add_mem