-- 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 (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) x
mem : ∀ (u : L) (hu : u ∈ range b.e ∪ range b.f), u ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zero : 0 ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
add :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u →
      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
smul :
  ∀ (t : R) (u : L),
    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
lie :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) u →
      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
⊢ x ∈ b.cartan.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    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
    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
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

Premises used: LieSubmodule.mem_sup_right, neg_mem_iff, LieAlgebra.Basis.e, add_assoc, LieAlgebra.Basis.cartan, LieAlgebra.Basis.f, lie_skew, LieSubalgebra.lieSpan, AddMemClass.add_mem, LieSubmodule.mem_sup_left, Set.range, rfl, lie_add, add_lie