-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
mem :
  ∀ (u : L) (hu : u ∈ s),
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
        R)
      (0 : R)
zero :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) 0) :
      R)
    (0 : R)
add :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u →
      Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) v →
        ∀
          (hu :
            Eq.{u_4 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
                R)
              (0 : R))
          (hv :
            Eq.{u_4 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) v : End R M) :
                R)
              (0 : R)),
          Eq.{u_4 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) (u + v) : End R M) :
              R)
            (0 : R)
smul :
  ∀ (t : R) (u : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u →
      ∀
        (hu :
          Eq.{u_4 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
              R)
            (0 : R)),
        Eq.{u_4 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) (t • u) : End R M) :
            R)
          (0 : R)
lie :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u →
      Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) v →
        Eq.{u_4 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
              R)
            (0 : R) →
          Eq.{u_4 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) v : End R M) :
                R)
              (0 : R) →
            Eq.{u_4 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) ⁅u, v⁆ : End R M) :
                R)
              (0 : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
      R)
    (0 : R)

Tactic:
induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu => simpa using hs u hu
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
  | lie u v _ _ _ _ => simp