awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : ℕ
IH :
  ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R),
    eval 0
        ((derivative : (a : R[X]) → R[X])
          (1 +
              HSMul.hSMul (α := R[X]) (β := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) X
                (M.map (⇑C : (a : R) → R[X]))).det) =
      M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
h : Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i
hi : i ≠ 0
j : Fin (n + 1)
⊢ 0 < i

Tactic:
exact lt_of_le_of_ne (Fin.zero_le _) hi.symm

Premises used: Fin.zero_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : ℕ
IH :
  ∀ (M : Matrix (Fin n) (Fin n) R),
    eval 0
        ((derivative : (a : R[X]) → R[X])
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
      M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ 0 ∉ univ →
    (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑0 : ℕ))))
              (eval 0 (1 0 0)) +
            HPow.hPow (α := R) (-1) (↑0 : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 0)) + M 0 0)) *
          eval 0 (det (n := Fin n) (submatrix 1 Fin.succ (Fin.succAbove 0))) +
        HPow.hPow (α := R) (-1) (↑0 : ℕ) * eval 0 (1 0 0) *
          eval 0
            ((derivative : (a : R[X]) → R[X])
              (submatrix 1 Fin.succ (Fin.succAbove 0) +
                  HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                    ((M.submatrix Fin.succ (Fin.succAbove 0)).map (⇑C : (a : R) → R[X]))).det) =
      0

Tactic:
fun H ↦ (H <| Finset.mem_univ _).elim

Premises used: Finset.mem_univ, False.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : ℕ
IH :
  ∀ (M : Matrix (Fin n) (Fin n) R),
    eval 0
        ((derivative : (a : R[X]) → R[X])
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
      M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ 0 ∉ univ →
    (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑0 : ℕ))))
              (eval 0 (1 0 0)) +
            HPow.hPow (α := R) (-1) (↑0 : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 0)) + M 0 0)) *
          eval 0 (det (n := Fin n) (submatrix 1 Fin.succ (Fin.succAbove 0))) +
        HPow.hPow (α := R) (-1) (↑0 : ℕ) * eval 0 (1 0 0) *
          eval 0
            ((derivative : (a : R[X]) → R[X])
              (submatrix 1 Fin.succ (Fin.succAbove 0) +
                  HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                    ((M.submatrix Fin.succ (Fin.succAbove 0)).map (⇑C : (a : R) → R[X]))).det) =
      0

Tactic:
exact fun H ↦ (H <| Finset.mem_univ _).elim
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
rw :
  eval 0
      ((derivative : (a : R[X]) → R[X])
        (det (n := Fin (Fintype.card n))
          ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
              (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
            (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))) =
    M.trace
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
    M.trace

Tactic:
rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)]

Premises used: Polynomial, Fintype.equivFin, Matrix.det_reindexLinearEquiv_self
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ Eq.{u + 1} (α := R)
    (eval 0
      ((derivative : (a : R[X]) → R[X])
        (1 +
            HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
              (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
                (⇑C : (a : R) → R[X]))).det))
    (trace (n := Fin (Fintype.card n))
      ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M))

Tactic:
derivative_det_one_add_X_smul_aux (e M)

Premises used: DFunLike.coe, Matrix.derivative_det_one_add_X_smul_aux
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
h :
  (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
        (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
      (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 (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
        (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
          (⇑C : (a : R) → R[X]))
h₁ :
  M.trace =
    trace (n := Fin (Fintype.card n))
      ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (det (n := Fin (Fintype.card n))
          ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
              (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
            (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))) =
    M.trace

Tactic:
convert! derivative_det_one_add_X_smul_aux (e M)

Premises used: DFunLike.coe, Matrix.derivative_det_one_add_X_smul_aux
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
h :
  ∀ (i j : Fin (Fintype.card n)) (n_1 : ℕ),
    coeff
        ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
            (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) i j)
        n_1 =
      (HAdd.hAdd (α := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) 1
            (HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
              (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
                (⇑C : (a : R) → R[X])))
            i j).coeff
        n_1
⊢ (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
        (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
      (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 (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
        (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
          (⇑C : (a : R) → R[X]))

Tactic:
ext
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
i j : Fin (Fintype.card n)
n_1 : ℕ
⊢ coeff
      ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
          (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
        (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) i j)
      n_1 =
    (HAdd.hAdd (α := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) 1
          (HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
            (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
              (⇑C : (a : R) → R[X])))
          i j).coeff
      n_1

Tactic:
simp [map_add, e]

Premises used: map_add
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
h :
  Eq.{u + 1} (α := R)
    (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
    (∑ i : Fin (Fintype.card n),
      diag ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M) i)
⊢ Eq.{u + 1} (α := R) (∑ i : n, M.diag i)
    (∑ i : Fin (Fintype.card n),
      diag ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M) i)

Tactic:
rw [← (Fintype.equivFin n).symm.sum_comp]

Premises used: Equiv.sum_comp, Fintype.equivFin, Equiv.symm
-- 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
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
h :
  Eq.{u + 1} (α := R)
    (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
    (∑ x : Fin (Fintype.card n),
      diag
        ((reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n) :
            (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R)
          M)
        x)
h₁ :
  Eq.{u + 1} (α := R)
    (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
    (∑ x : Fin (Fintype.card n),
      diag
        ((reindex (Fintype.equivFin n) (Fintype.equivFin n) :
            (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R)
          M)
        x)
h₂ :
  Eq.{u + 1} (α := R)
    (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
    (∑ x : Fin (Fintype.card n),
      diag
        (M.submatrix (⇑(Equiv.symm (Fintype.equivFin n)) : (a : Fin (Fintype.card n)) → n)
          (⇑(Equiv.symm (Fintype.equivFin n)) : (a : Fin (Fintype.card n)) → n))
        x)
h₃ :
  Eq.{u + 1} (α := R)
    (∑ x : Fin (Fintype.card n),
      M ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) x)
        ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) x))
    (∑ x : Fin (Fintype.card n),
      M.submatrix (⇑(Equiv.symm (Fintype.equivFin n)) : (a : Fin (Fintype.card n)) → n)
        (⇑(Equiv.symm (Fintype.equivFin n)) : (a : Fin (Fintype.card n)) → n) x x)
⊢ Eq.{u + 1} (α := R)
    (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
    (∑ i : Fin (Fintype.card n),
      diag ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M) i)

Tactic:
simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]

Premises used: Matrix.reindex_apply, Matrix.diag_apply, Matrix.reindexLinearEquiv_apply, Matrix.submatrix_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]))).det.coeff 1 = M.trace

Tactic:
simp only [← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero,
    coeff_derivative, zero_add, Nat.cast_zero, mul_one]

Premises used: Polynomial.coeff_derivative, Polynomial.coeff_zero_eq_eval_zero, Matrix.derivative_det_one_add_X_smul, zero_add, Nat.cast_zero, mul_one
-- 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 :
  (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det =
    (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.divX * X +
      (C : (a : R) → R[X]) 1
⊢ (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det =
    1 + HSMul.hSMul (β := R[X]) M.trace X +
      (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.divX.divX *
        HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
rw [Algebra.smul_def (trace M), ← C_eq_algebraMap, pow_two, ← mul_assoc, add_assoc,
    ← add_mul, ← coeff_det_one_add_X_smul_one, ← coeff_divX, add_comm (C _), divX_mul_X_add,
    add_comm (1 : R[X]), ← C.map_one]

Premises used: add_mul, Polynomial.C, pow_two, add_assoc, mul_assoc, RingHom.map_one, Matrix.trace, Polynomial.C_eq_algebraMap, Polynomial.divX_mul_X_add, add_comm, Matrix.coeff_det_one_add_X_smul_one, Algebra.smul_def, Polynomial.coeff_divX, OfNat.ofNat, 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
⊢ (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det =
    HAdd.hAdd (β := R[X])
      ((1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.divX * X)
      ((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]))).det.coeff 0) :
        R[X])

Tactic:
(divX_mul_X_add _).symm

Premises used: Polynomial.divX_mul_X_add, Eq.symm
-- 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 : 1 = (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.coeff 0
⊢ (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det =
    (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.divX * X +
      (C : (a : R) → R[X]) 1

Tactic:
convert! (divX_mul_X_add _).symm

Premises used: Polynomial.divX_mul_X_add, Eq.symm
-- 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 : 1 = eval 0 (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det
h₁ : Eq.{u + 1} (α := R) 1 (eval 0 (det.{u, v} (n := n) 1))
h₂ : Eq.{u + 1} (α := R) 1 (eval 0 1)
h₃ h₄ : Eq.{u + 1} (α := R) 1 1
⊢ 1 = (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.coeff 0

Tactic:
rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_one]

Premises used: eval_det_add_X_smul, Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_one, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
r : R
M : Matrix n n R
⊢ (1 + r • M).det =
    1 + M.trace * r +
      eval r
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det.divX.divX *
        HPow.hPow (β := ℕ) r 2

Tactic:
simpa [eval_det, ← smul_eq_mul_diagonal] using congr_arg (eval r) (Matrix.det_one_add_X_smul M)

Premises used: Polynomial.eval, Matrix.det_one_add_X_smul, Matrix.smul_eq_mul_diagonal, congr_arg, eval_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
M : Matrix n n R
inst_3 : Nontrivial R
hn : Fintype.card n = 2
rw : 0 < Fintype.card n
⊢ Nonempty n

Tactic:
rw [← Fintype.card_pos_iff]

Premises used: Fintype.card_pos_iff
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
⊢ 0 < Fintype.card n

Tactic:
lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
⊢ Nonempty n

Tactic:
have : Nonempty n := by rw [← Fintype.card_pos_iff]; lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
a :
  ∀ (i : ℕ),
    coeff M.charpoly i =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
            ((C : (a : R) → R[X]) M.det : R[X])).coeff
        i
⊢ M.charpoly =
    HAdd.hAdd (β := R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
      ((C : (a : R) → R[X]) M.det : R[X])

Tactic:
ext i
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
pos :
  ∀ (hi : i ∈ range 3),
    coeff M.charpoly i =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
            ((C : (a : R) → R[X]) M.det : R[X])).coeff
        i
neg :
  ∀ (hi : i ∉ range 3),
    coeff M.charpoly i =
      (HAdd.hAdd (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
            ((C : (a : R) → R[X]) M.det : R[X])).coeff
        i
⊢ coeff M.charpoly i =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      i

Tactic:
by_cases hi : i ∈ Finset.range 3

Premises used: Finset.range, OfNat.ofNat
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∈ range 3
pos :
  coeff M.charpoly 0 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      0
pos₁ :
  coeff M.charpoly 1 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      1
pos₂ :
  coeff M.charpoly 2 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      2
⊢ coeff M.charpoly i =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      i

Tactic:
fin_cases hi
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ coeff M.charpoly 0 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      0

Tactic:
simp [det_eq_sign_charpoly_coeff, hn]

Premises used: Matrix.det_eq_sign_charpoly_coeff
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ coeff M.charpoly 1 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      1

Tactic:
simp [trace_eq_neg_charpoly_coeff, hn]

Premises used: Matrix.trace_eq_neg_charpoly_coeff
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ coeff M.charpoly 2 =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      2

Tactic:
simpa [leadingCoeff, charpoly_natDegree_eq_dim, hn, coeff_X] using
        M.charpoly_monic.leadingCoeff

Premises used: Polynomial.leadingCoeff, Matrix.charpoly_natDegree_eq_dim, Matrix.charpoly_monic, Polynomial.Monic.leadingCoeff, Polynomial.coeff_X
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ 2 < i

Tactic:
rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi

Premises used: Finset.mem_range, not_lt, Nat.succ_le_iff
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this_1 : Nonempty n
i : ℕ
hi : 2 < i
this : coeff M.charpoly i = 0
⊢ i ≠ 2

Tactic:
lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this_1 : Nonempty n
i : ℕ
hi : 2 < i
this : coeff M.charpoly i = 0
⊢ 1 ≠ i

Tactic:
lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this_1 : Nonempty n
i : ℕ
hi : 2 < i
this : coeff M.charpoly i = 0
⊢ i ≠ 0

Tactic:
lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this_1 : Nonempty n
i : ℕ
hi : 2 < i
this : coeff M.charpoly i = 0
⊢ coeff M.charpoly i =
    (HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2 -
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) M.trace : R[X]) X)
          ((C : (a : R) → R[X]) M.det : R[X])).coeff
      i

Tactic:
simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]

Premises used: Polynomial.coeff_C, Polynomial.coeff_X