awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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₂ : 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
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]
-- 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
⊢ 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₃ : 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
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]
-- 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
⊢ 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₄ : 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⁻¹])
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]
-- 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⁻¹])
⊢ 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₅ : 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
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]
-- 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
⊢ 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₆ : 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
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]
-- 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
⊢ 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₇ : 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
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]
-- 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
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have suffices : t_inv ^ Fintype.card n * p = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
Tactic: suffices t_inv ^ Fintype.card n * p = invert q by
    apply toLaurent_injective
    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]
-- 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
⊢ t_inv ^ Fintype.card n * p = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
have rw : (1 - HSMul.hSMul (β := Matrix.{v, v, u} n n R[T;T⁻¹]) t_inv (M.map (⇑LaurentPolynomial.C : (a : R) → R[T;T⁻¹]))).det =
  det.{u, v} (n := n)
    ((AlgEquiv.mapMatrix invert : (a : Matrix n n R[T;T⁻¹]) → Matrix n n 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⁻¹]))))
Tactic: rw [← det_smul, smul_sub, scalar_apply, ← diagonal_smul, Pi.smul_def, smul_eq_mul, ht,
    diagonal_one, invert.map_det]
-- 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
⊢ 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 have : ∀ (this : Invertible A),
  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
Tactic: have : Invertible A := h.invertible
-- 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
⊢ 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
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (A⁻¹.det * 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
Tactic: rw [det_mul]
-- 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
⊢ 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
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HSub.hSub (β := Matrix.{v, v, u} n n 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]))
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (A * 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
Tactic: rw [mul_sub, ← map_mul]