-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
t : R
rw :
  eval t
      (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f)) =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
rw₁ :
  (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
          Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
            f :
          Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)).det =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
rw₂ :
  (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
          Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
            f :
          Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)).det =
    det.{u, v} (n := ChooseBasisIndex R M)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f))
⊢ eval t f.charpoly =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
have rw₃ : (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)).det =
  (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t) :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)).det
Tactic: rw [charpoly, Matrix.eval_charpoly, ← LinearMap.det_toMatrix (chooseBasis R M), map_sub,
    scalar_apply, toMatrix_algebraMap, scalar_apply]