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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
neg : 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:
suffices M.charpoly.coeff i = 0 by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]
-- 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 : 2 < i
neg : natDegree M.charpoly < i
⊢ coeff M.charpoly i = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- 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 : 2 < i
⊢ natDegree M.charpoly < i

Tactic:
simpa [charpoly_natDegree_eq_dim, hn] using hi

Premises used: Matrix.charpoly_natDegree_eq_dim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
M : Matrix (Fin 2) (Fin 2) R
⊢ 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:
M.charpoly_of_card_eq_two <| Fintype.card_fin _

Premises used: Fintype.card_fin, Matrix.charpoly_of_card_eq_two
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
a :
  ∀ (m : ℕ) (i j : n),
    coeff
        ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
          ((RingHom.mapMatrix (↑(expand K k) : K[X] →+* K[X]) : (a : Matrix n n K[X]) → Matrix n n K[X])
            (M ^ k).charmatrix))
        m i j =
      (HSub.hSub (β := (Matrix n n K)[X]) (HPow.hPow (α := (Matrix n n K)[X]) X k)
            ((C : (a : Matrix n n K) → (Matrix n n K)[X]) (M ^ k) : (Matrix n n K)[X])).coeff
        m i j
⊢ (matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
      ((RingHom.mapMatrix (↑(expand K k) : K[X] →+* K[X]) : (a : Matrix n n K[X]) → Matrix n n K[X])
        (M ^ k).charmatrix) =
    HSub.hSub (β := (Matrix n n K)[X]) (HPow.hPow (α := (Matrix n n K)[X]) X k)
      ((C : (a : Matrix n n K) → (Matrix n n K)[X]) (M ^ k) : (Matrix n n K)[X])

Tactic:
ext m i j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
a :
  coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j
⊢ coeff
      ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
        ((RingHom.mapMatrix (↑(expand K k) : K[X] →+* K[X]) : (a : Matrix n n K[X]) → Matrix n n K[X])
          (M ^ k).charmatrix))
      m i j =
    (HSub.hSub (β := (Matrix n n K)[X]) (HPow.hPow (α := (Matrix n n K)[X]) X k)
          ((C : (a : Matrix n n K) → (Matrix n n K)[X]) (M ^ k) : (Matrix n n K)[X])).coeff
      m i j

Tactic:
rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply,
    AlgHom.coe_toRingHom, coeff_X_pow]

Premises used: AlgHom.coe_toRingHom, RingHom.mapMatrix_apply, Polynomial.coeff_X_pow, Matrix.map_apply, Polynomial.coeff_C, Polynomial.coeff_sub, matPolyEquiv_coeff_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
pos :
  ∀ (hij : i = j),
    coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
      HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j
neg :
  ∀ (hij : ¬i = j),
    coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
      HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j
⊢ coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j

Tactic:
by_cases hij : i = j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
pos :
  ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) j j
⊢ coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j

Tactic:
rw [hij, charmatrix_apply_eq, map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, coeff_C]

Premises used: map_sub, Matrix.charmatrix_apply_eq, Polynomial.coeff_X_pow, Polynomial.expand_C, Polynomial.coeff_C, Polynomial.expand_X, Polynomial.coeff_sub
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
pos : ∀ (mp : m = k) (m0 : m = 0), 1 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) j j
neg : ∀ (mp : m = k) (m0 : ¬m = 0), HSub.hSub (α := K) 1 0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 1 0 j j
pos₁ : ∀ (mp : ¬m = k), m = 0 → 0 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) j j
neg₁ : ∀ (mp : ¬m = k), ¬m = 0 → HSub.hSub (α := K) 0 0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 0 0 j j
⊢ ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) j j

Tactic:
split_ifs with mp m0
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : m = 0
⊢ 1 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) j j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : ¬m = 0
⊢ HSub.hSub (α := K) 1 0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 1 0 j j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h : m = 0
⊢ 0 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) j j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h : ¬m = 0
⊢ HSub.hSub (α := K) 0 0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 0 0 j j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
neg :
  (-if m = 0 then (M ^ k) i j else 0) =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j
⊢ coeff ((expand K k : (a : K[X]) → K[X]) ((M ^ k).charmatrix i j)) m =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]

Premises used: Matrix.charmatrix_apply_ne, Polynomial.expand_C, map_neg, Polynomial.coeff_C, Polynomial.coeff_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
pos : ∀ (m0 : m = 0) (mp : m = k), -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) i j
neg : ∀ (m0 : m = 0) (mp : ¬m = k), -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) i j
pos₁ : ∀ (m0 : ¬m = 0), m = k → -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 1 0 i j
neg₁ : ∀ (m0 : ¬m = 0), ¬m = k → -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 0 0 i j
⊢ (-if m = 0 then (M ^ k) i j else 0) =
    HSub.hSub (α := Matrix n n K) (if m = k then 1 else 0) (if m = 0 then M ^ k else 0) i j

Tactic:
split_ifs with m0 mp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : m = k
⊢ -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) i j

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : ¬m = k
⊢ -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) i j

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h : m = k
⊢ -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 1 0 i j

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
k : ℕ
inst_2 : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h : ¬m = k
⊢ -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 0 0 i j

Tactic:
simp_all
-- 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
p : R[X]
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) p : Matrix n n R)
    ((aeval M : (a : R[X]) → Matrix n n R) (p %ₘ M.charpoly) : Matrix n n R)

Tactic:
(aeval_modByMonic_eq_self_of_root M.aeval_self_charpoly).symm

Premises used: Polynomial.aeval_modByMonic_eq_self_of_root, Matrix.aeval_self_charpoly, 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
k : ℕ
rw : M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k)
rw₁ : M ^ k = HPow.hPow (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) X : Matrix n n R) k
rw₂ rw₃ : M ^ k = M ^ k
⊢ M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k %ₘ M.charpoly)

Tactic:
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

Premises used: map_pow, Matrix.aeval_eq_aeval_mod_charpoly, Polynomial.aeval_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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
delta : coeff (det M.charmatrix) k ∈ I ^ (Fintype.card n - k)
⊢ coeff M.charpoly k ∈ I ^ (Fintype.card n - k)

Tactic:
delta charpoly

Premises used: Matrix.charpoly
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
rw :
  ∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n, M.charmatrix ((b : (a : n) → n) i) i)).coeff
        k ∈
    I ^ (Fintype.card n - k)
⊢ coeff (det M.charmatrix) k ∈ I ^ (Fintype.card n - k)

Tactic:
rw [Matrix.det_apply, finsetSum_coeff]

Premises used: Matrix.det_apply, Polynomial.finsetSum_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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
h₁ :
  ∀ (c : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) univ c →
      (HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c : ℤˣ)
              (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)).coeff
          k ∈
        I ^ (Fintype.card n - k)
⊢ ∑ b : Equiv.Perm n,
      (HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) b : ℤˣ)
            (∏ i : n, M.charmatrix ((b : (a : n) → n) i) i)).coeff
        k ∈
    I ^ (Fintype.card n - k)

Tactic:
apply sum_mem

Premises used: sum_mem
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
h₁ : coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (Fintype.card n - k)
⊢ (HSMul.hSMul (α := ℤˣ) (β := R[X]) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c : ℤˣ)
          (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)).coeff
      k ∈
    I ^ (Fintype.card n - k)

Tactic:
rw [coeff_smul, Submodule.smul_mem_iff']

Premises used: Polynomial.coeff_smul, Submodule.smul_mem_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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
rw : HSMul.hSMul (β := ℕ) (card.{v} (α := n) univ) 1 = Fintype.card n
rw₁ : HSMul.hSMul (β := ℕ) (Fintype.card n) 1 = Fintype.card n
rw₂ : Fintype.card n * 1 = Fintype.card n
rw₃ rw₄ : Fintype.card n = Fintype.card n
⊢ ∑ x : n, 1 = Fintype.card n

Tactic:
rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]

Premises used: Finset.card_univ, smul_eq_mul, mul_one, Finset.sum_const
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ ∑ x : n, 1 = Fintype.card n

Tactic:
have : ∑ x : n, 1 = Fintype.card n := by rw [Finset.sum_const, card_univ, smul_eq_mul, 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
h₁ : coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (∑ x : n, 1 - k)
⊢ coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (Fintype.card n - k)

Tactic:
rw [← this]
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
h₁ :
  ∀ (i : n),
    Membership.mem (γ := Finset n) univ i → ∀ (k : ℕ), coeff (M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (1 - k)
⊢ coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (∑ x : n, 1 - k)

Tactic:
apply coeff_prod_mem_ideal_pow_tsub

Premises used: Polynomial.coeff_prod_mem_ideal_pow_tsub
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
h₁ : M ((c : (a : n) → n) i) i ∈ I
⊢ coeff (M.charmatrix ((c : (a : n) → n) i) i) 0 ∈ I ^ HSub.hSub (α := ℕ) 1 0

Tactic:
rw [tsub_zero, pow_one, charmatrix_apply, coeff_sub, ← smul_one_eq_diagonal, smul_apply,
      smul_eq_mul, coeff_X_mul_zero, coeff_C_zero, zero_sub, neg_mem_iff]

Premises used: neg_mem_iff, Matrix.smul_one_eq_diagonal, Matrix.smul_apply, tsub_zero, Polynomial.coeff_X_mul_zero, Polynomial.coeff_sub, pow_one, Polynomial.coeff_C_zero, smul_eq_mul, Matrix.charmatrix_apply, zero_sub
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ M ((c : (a : n) → n) i) i ∈ I

Tactic:
h (c i) i

Premises used: 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ M ((c : (a : n) → n) i) i ∈ I

Tactic:
exact h (c i) i

Premises used: 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k_1 : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
h₁ : Membership.mem (γ := Ideal R) ⊤ (coeff (M.charmatrix ((c : (a : n) → n) i) i) (1 + k))
⊢ coeff (M.charmatrix ((c : (a : n) → n) i) i) (k + 1) ∈ I ^ (1 - (k + 1))

Tactic:
rw [add_comm, tsub_self_add, pow_zero, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, add_comm, pow_zero, tsub_self_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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k_1 : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
⊢ Membership.mem (γ := Ideal R) ⊤ (coeff (M.charmatrix ((c : (a : n) → n) i) i) (1 + k))

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- 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 : Ideal R
h : ∀ (i j : n), M i j ∈ I
k_1 : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
⊢ Membership.mem (γ := Ideal R) ⊤ (coeff (M.charmatrix ((c : (a : n) → n) i) i) (1 + k))

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- 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
rw : Eq.{u + 1} (α := R[T;T⁻¹]) (T (HAdd.hAdd (α := ℤ) (-1) 1)) 1
rw₁ : Eq.{u + 1} (α := R[T;T⁻¹]) (T 0) 1
rw₂ rw₃ : Eq.{u + 1} (α := R[T;T⁻¹]) 1 1
⊢ t_inv * t = 1

Tactic:
rw [← T_add, neg_add_cancel, T_zero]

Premises used: LaurentPolynomial.T_zero, neg_add_cancel, LaurentPolynomial.T_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
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
⊢ t_inv * t = 1

Tactic:
have ht : t_inv * t = 1 := by rw [← T_add, neg_add_cancel, T_zero]
-- 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
⊢ (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpoly = p

Tactic:
simp [p, t, charpoly, charmatrix, AlgHom.map_det, map_sub]

Premises used: map_sub, Matrix.charmatrix, AlgHom.map_det, Matrix.charpoly
-- 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
⊢ (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpoly = p

Tactic:
have hp : toLaurentAlg M.charpoly = p := by
    simp [p, t, charpoly, charmatrix, AlgHom.map_det, map_sub]
-- 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
⊢ (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev = q

Tactic:
simp [q, t, charpolyRev, AlgHom.map_det, map_sub, smul_eq_diagonal_mul]

Premises used: map_sub, Matrix.charpolyRev, AlgHom.map_det, 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
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
⊢ (toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) M.charpolyRev = q

Tactic:
have hq : toLaurentAlg M.charpolyRev = q := by
    simp [q, t, charpolyRev, AlgHom.map_det, map_sub, smul_eq_diagonal_mul]