-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
mem :
  ∀ (u : L) (hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
        R)
      (0 : R)
zero :
  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 * y) : R)
    (0 : R)
add :
  ∀ (u v : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) u →
      Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) v →
        ∀
          (hu :
            Eq.{u_1 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (HMul.hMul (α := End R M)
                    (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
                R)
              (0 : R))
          (hv :
            Eq.{u_1 + 1} (α := R)
              ((trace R M : (a : M →ₗ[R] M) → R)
                  (HMul.hMul (α := End R M)
                    (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) v : End R M) y) :
                R)
              (0 : R)),
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (HMul.hMul (α := End R M)
                  (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) (u + v) : End R M) y) :
              R)
            (0 : R)
smul :
  ∀ (t : R) (u : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) u →
      ∀
        (hu :
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M)
                  y) :
              R)
            (0 : R)),
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (HMul.hMul (α := End R M)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) (t • u) : End R M) y) :
            R)
          (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) y) :
      R)
    (0 : R)

Tactic:
induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨a, b, rfl⟩ := hu
    obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
    replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
    rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
  | zero => simp
  | add u v _ _ hu hv => simp [add_mul, hu, hv]
  | smul t u _ hu => simp [hu]

Premises used: add_mul, LinearMap.zero_apply, Module.End.mul_eq_comp, LieHom.map_lie, neg_eq_zero, map_neg, LieRing.of_associative_ring_bracket, Module.End.instLieRingModule_eq, LieModule.traceForm_apply_apply, Ring.lie_def, LinearMap.trace_lie_mul_eq, rfl, mul_neg