-- 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
_ :
  (HSub.hSub (α := 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⁻¹ * A).det : R[X])
      (HSub.hSub (α := 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⁻¹ * A).det : R[X])
      (HSub.hSub (α := 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]) (β := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X]) ((C : (a : R) → R[X]) A.det : R[X]) *
      (HSub.hSub (α := 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]) (β := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X]) ((C : (a : R) → R[X]) A.det : R[X]) *
      (HSub.hSub (α := 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 (α := R[X]) ((C : (a : R) → R[X]) A.det : R[X])
        (HSub.hSub (α := 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 (α := R[X]) ((C : (a : R) → R[X]) A.det : R[X])
        (HSub.hSub (α := 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])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
          (HSub.hSub (α := 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])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
          (HSub.hSub (α := 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])
      (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)
⊢ A⁻¹.charpoly =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      A.charpolyRev
have _₆ : 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]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
    A.charpolyRev
Tactic: calc
  _ = (scalar n X - C.mapMatrix A⁻¹).det := rfl
  _ = C (A⁻¹ * A).det * (scalar n X - C.mapMatrix A⁻¹).det := by simp
  _ = C A⁻¹.det * C A.det * (scalar n X - C.mapMatrix A⁻¹).det := by rw [det_mul]; simp
  _ = C A⁻¹.det * (C A.det * (scalar n X - C.mapMatrix A⁻¹).det) := by ac_rfl
  _ = C A⁻¹.det * (C.mapMatrix A * (scalar n X - C.mapMatrix A⁻¹)).det := by simp [RingHom.map_det]
  _ = C A⁻¹.det * (C.mapMatrix A * scalar n X - 1).det := by rw [mul_sub, ← map_mul]; simp
  _ = C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - scalar n X * C.mapMatrix A).det) := by
    rw [← neg_sub, det_neg, det_one_sub_mul_comm]
  _ = _ := by simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl