-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (-(1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]))).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])).det) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]) -
          1).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
have rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
Tactic: rw [← neg_sub, det_neg, det_one_sub_mul_comm]