-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
mem :
  ∀ (u : L) (hu : u ∈ s),
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u ⋯)
zero :
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) 0 ⋯)
add :
  ∀ (u v : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v)
    (hu :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx))
    (hv :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy)),
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) ⋯)
smul :
  ∀ (t : R) (u : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u)
    (hu :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx)),
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) ⋯)
lie :
  ∀ (u v : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v)
    (hu :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx))
    (hv :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy)),
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁅u, v⁆ ⋯)
⊢ Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) x hx)

Tactic:
induction hx using lieSpan_induction with
  | mem u hu => exact subset_lieSpan <| by simpa
  | zero => exact zero_mem _
  | add u v _ _ hu hv => revert hu hv; exact add_mem
  | smul t u _ hu => revert hu; exact LieSubalgebra.smul_mem _ _
  | lie u v _ _ hu hv => revert hu hv; exact LieSubalgebra.lie_mem _

Premises used: LieSubalgebra.subset_lieSpan, AddMemClass.add_mem, ZeroMemClass.zero_mem, LieSubalgebra.smul_mem, LieSubalgebra.lie_mem