awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 :
  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⁻¹])
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev

Tactic:
apply toLaurent_injective

Premises used: Polynomial.toLaurent_injective
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
suffices : t_inv ^ Fintype.card n * p = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
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⁻¹]))))
⊢ t_inv ^ Fintype.card n * p = (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) q

Tactic:
rw [← det_smul, smul_sub, scalar_apply, ← diagonal_smul, Pi.smul_def, smul_eq_mul, ht,
    diagonal_one, invert.map_det]

Premises used: Matrix.det_smul, Matrix.diagonal_smul, smul_sub, Matrix.diagonal_one, AlgEquiv.map_det, smul_eq_mul, LaurentPolynomial.invert, Matrix.scalar_apply, Pi.smul_def
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
⊢ (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:
simp [t_inv, map_sub, map_one, map_mul, t, smul_eq_diagonal_mul]

Premises used: map_sub, map_mul, map_one, Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 =
    (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:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 * 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⁻¹ * 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]

Premises used: Matrix.det_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 * 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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]) (β := 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)

Tactic:
ac_rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 (α := 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

Tactic:
simp [RingHom.map_det]

Premises used: RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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])
      (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
⊢ 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

Tactic:
rw [mul_sub, ← map_mul]

Premises used: mul_sub, map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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])
      (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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
simp :
  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]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → R[X]))).det) =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      (1 - HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → 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]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      A.charpolyRev

Tactic:
simp [charpolyRev, smul_eq_diagonal_mul]

Premises used: Matrix.charpolyRev, Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 - HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → R[X]))).det) =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      (1 - HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → R[X]))).det

Tactic:
ac_rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
rw :
  Eq.{u + 1} (α := R)
    (det.{u, v} (n := n)
      ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n R[X]) → Matrix n n R)
        (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))
    (det.{u, v} (n := n) 1)
⊢ eval 0 M.charpolyRev = 1

Tactic:
rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]

Premises used: Matrix.charpolyRev, RingHom.map_det, Matrix.det_one, Polynomial.coe_evalRingHom
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
a :
  ∀ (i j : n),
    (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
      1 i j
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) = 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
a :
  ∀ (hij : i = j),
    (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
      1 i j
a₁ :
  ∀ (hij : i ≠ j),
    (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
      1 i j
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j

Tactic:
rcases eq_or_ne i j with hij | hij

Premises used: eq_or_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
hij : i = j
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j

Tactic:
simp [hij, one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
hij : i ≠ j
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j

Tactic:
simp [hij, one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) = 1

Tactic:
have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
    ext i j; rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
this : (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) = 1
⊢ Eq.{u + 1} (α := R)
    (det.{u, v} (n := n)
      ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n R[X]) → Matrix n n R)
        (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))
    (det.{u, v} (n := n) 1)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
inl : IsEmpty n → coeff M.charpolyRev 1 = -M.trace
inr : Nonempty n → coeff M.charpolyRev 1 = -M.trace
⊢ coeff M.charpolyRev 1 = -M.trace

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
h_1 : IsEmpty n
⊢ coeff M.charpolyRev 1 = -M.trace

Tactic:
simp [charpolyRev, coeff_one]

Premises used: Polynomial.coeff_one, Matrix.charpolyRev
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
h_1 : Nonempty n
⊢ coeff M.charpolyRev 1 = -M.trace

Tactic:
simp [trace_eq_neg_charpoly_coeff M, ← M.reverse_charpoly, nextCoeff]

Premises used: Matrix.trace_eq_neg_charpoly_coeff, Matrix.reverse_charpoly, Polynomial.nextCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
hM : IsNilpotent M
obtain : ∀ (k : ℕ) (hk : M ^ k = 0), IsUnit (M := R[X]) M.charpolyRev
⊢ IsUnit (M := R[X]) M.charpolyRev

Tactic:
obtain ⟨k, hk⟩ := hM
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣
    1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k

Tactic:
one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k

Premises used: Polynomial.C, one_sub_dvd_one_sub_pow, Matrix.map, HSMul.hSMul, Polynomial.X, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
h : 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
⊢ 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1

Tactic:
convert! one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k

Premises used: Polynomial.C, one_sub_dvd_one_sub_pow, Matrix.map, HSMul.hSMul, Polynomial.X, DFunLike.coe