-- 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
inst_7 : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
hB :
  ∀ (x : L) (m n : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ⁅x, m⁆ : M →ₗ[R] R) : (a : M) → R) n : R)
      (-(((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) ⁅x, n⁆ : R)
m₀ m₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
zero :
  ∀ (m n : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (β := ℕ)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) 0 :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (β := ℕ) (-1) 0)
        ((((B : (a : M) → M →ₗ[R] R)
                  ((HPow.hPow (α := End R M) (β := ℕ)
                        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) 0 :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ (m n : M),
        (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
            ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
                    k :
                  (a : M) → M)
                n :
              M) =
          HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k)
            ((((B : (a : M) → M →ₗ[R] R)
                      ((HPow.hPow (α := End R M)
                            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
                          (a : M) → M)
                        m) :
                    M →ₗ[R] R) :
                  (a : M) → R)
                n :
              R))
    (m n : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
                (k + 1) :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) (k + 1))
        ((((B : (a : M) → M →ₗ[R] R)
                  ((HPow.hPow (α := End R M)
                        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) (k + 1) :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
⊢ ∀ (m n : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k)
        ((((B : (a : M) → M →ₗ[R] R)
                  ((HPow.hPow (α := End R M)
                        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)

Tactic:
induction k with
    | zero => simp
    | succ k ih =>
    intro m n
    replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
    have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ (-1 : R), smul_eq_mul]
    conv_lhs => rw [pow_succ, Module.End.mul_eq_comp, LinearMap.comp_apply, ih, hB,
      ← (φ x).comp_apply, ← Module.End.mul_eq_comp, ← pow_succ', ← smul_assoc, this]

Premises used: Module.End.mul_eq_comp, smul_assoc, pow_succ, LinearMap.comp_apply, pow_succ'