-- 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
M : Matrix n n R
h : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] :=
  (HSub.hSub (α := Matrix.{v, v, u} n n R[T;T⁻¹]) (β := Matrix.{v, v, u} n n R[T;T⁻¹])
      ((scalar n : (a : R[T;T⁻¹]) → Matrix n n R[T;T⁻¹]) t : Matrix.{v, v, u} n n R[T;T⁻¹])
      (M.map (⇑LaurentPolynomial.C : (a : R) → R[T;T⁻¹]))).det
q : R[T;T⁻¹] :=
  (1 -
      HMul.hMul (α := Matrix.{v, v, u} n n R[T;T⁻¹]) (β := Matrix.{v, v, u} n n R[T;T⁻¹])
        ((scalar n : (a : R[T;T⁻¹]) → Matrix n n R[T;T⁻¹]) t : Matrix.{v, v, u} n n R[T;T⁻¹])
        (M.map (⇑LaurentPolynomial.C : (a : R) → R[T;T⁻¹]))).det
ht : t_inv * t = 1
hp : (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpoly = p
hq : (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) M.charpoly) : R[T;T⁻¹])
      (T (↑(natDegree M.charpoly) : ℤ)) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev
a₁ :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpoly) : R[T;T⁻¹])
      (T (↑(natDegree M.charpoly) : ℤ)) =
    (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev
a₂ :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) p : R[T;T⁻¹])
      (T (↑(natDegree M.charpoly) : ℤ)) =
    (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev
a₃ :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) p : R[T;T⁻¹])
      (T (↑(natDegree M.charpoly) : ℤ)) =
    q
a₄ :
  Eq (α := R[T;T⁻¹])
    ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) p : R[T;T⁻¹])
          (T (↑(natDegree M.charpoly) : ℤ))) :
      R[T;T⁻¹])
    ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q : R[T;T⁻¹])
a₅ :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) p) : R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T (↑(natDegree M.charpoly) : ℤ)) : R[T;T⁻¹]) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a₆ :
  HMul.hMul (β := R[T;T⁻¹]) p ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T (↑(natDegree M.charpoly) : ℤ)) : R[T;T⁻¹]) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a₇ :
  HMul.hMul (β := R[T;T⁻¹]) p ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T (↑(Fintype.card n) : ℤ)) : R[T;T⁻¹]) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a₈ :
  HMul.hMul (β := R[T;T⁻¹]) p
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T (HMul.hMul (α := ℤ) (↑(Fintype.card n) : ℤ) 1)) : R[T;T⁻¹]) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a₉ :
  HMul.hMul (β := R[T;T⁻¹]) p
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (HPow.hPow (α := R[T;T⁻¹]) (T 1) (Fintype.card n)) : R[T;T⁻¹]) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
a₁₀ :
  p * HPow.hPow (α := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T 1) : R[T;T⁻¹]) (Fintype.card n) =
    (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (reverse M.charpoly) : R[T;T⁻¹])
    ((toLaurent : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev : R[T;T⁻¹])
have a₁₁ : p * HPow.hPow (α := R[T;T⁻¹]) (T (-1)) (Fintype.card n) = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
Tactic: rwa [toLaurent_reverse, ← coe_toLaurentAlg, hp, hq, ← involutive_invert.injective.eq_iff,
      map_mul, involutive_invert p, charpoly_natDegree_eq_dim,
      ← mul_one (Fintype.card n : ℤ), ← T_pow, map_pow, invert_T, mul_comm]