-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
⊢ ∀ (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)
have 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)
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]
Cleared hypotheses: k