-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
refine_1 :
  ∀ (x : L) (h : Membership.mem (γ := Set L) {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m} x),
    (fun (x : L)
          (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
            R)
          (0 : R))
      x ⋯
refine_2 :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) 0) : R) (0 : R)
refine_3 :
  ∀ (u v : L) (x : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) u)
    (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) v)
    (hu :
      (fun (x : L)
            (x_2 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
              R)
            (0 : R))
        u x)
    (hv :
      (fun (x : L)
            (x_2 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
              R)
            (0 : R))
        v x_1),
    (fun (x : L)
          (x_2 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
            R)
          (0 : R))
      (u + v) ⋯
refine_4 :
  ∀ (t : R) (u : L)
    (x : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) u)
    (hu :
      (fun (x : L)
            (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
              R)
            (0 : R))
        u x),
    (fun (x : L)
          (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
            R)
          (0 : R))
      (t • u) ⋯
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
      R)
    (0 : R)

Tactic:
refine Submodule.span_induction (p := fun x _ ↦ trace R _ (toEnd R L M x) = 0)
    ?_ ?_ (fun u v _ _ hu hv ↦ ?_) (fun t u _ hu ↦ ?_) hx

Premises used: Submodule.span_induction