-- 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
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 : ℕ
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
hB :
  ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
this : HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) (k + 1)
conv_lhs :
  (((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)
⊢ (((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)
have succ : 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) =
  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: 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]