awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ 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
have 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
Tactic: rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ (-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
have pos : ∀ (m0 : m = 0) (mp : m = k), -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) i j
Tactic: split_ifs with m0 mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ (-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
have neg : ∀ (m0 : m = 0) (mp : ¬m = k), -(M ^ k) i j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) i j
Tactic: split_ifs with m0 mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ (-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
have pos₁ : ∀ (m0 : ¬m = 0), m = k → -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 1 0 i j
Tactic: split_ifs with m0 mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ (-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
have neg₁ : ∀ (m0 : ¬m = 0), ¬m = k → -0 = HSub.hSub (α := Matrix n n K) (β := Matrix n n K) 0 0 i j
Tactic: split_ifs with m0 mp
-- 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
k : ℕ
⊢ M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k %ₘ M.charpoly)
have rw : M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k)
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- 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
k : ℕ
rw : M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k)
⊢ M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k %ₘ M.charpoly)
have rw₁ : M ^ k = HPow.hPow (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) X : Matrix n n R) k
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- 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
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
⊢ M ^ k = (aeval M : (a : R[X]) → Matrix n n R) (HPow.hPow (α := R[X]) X k %ₘ M.charpoly)
have rw₂ : M ^ k = M ^ k
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ coeff M.charpoly k ∈ I ^ (Fintype.card n - k)
have delta : coeff (det M.charmatrix) k ∈ I ^ (Fintype.card n - k)
Tactic: delta charpoly
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ coeff (det M.charmatrix) k ∈ I ^ (Fintype.card n - k)
have 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)
Tactic: rw [Matrix.det_apply, finsetSum_coeff]
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
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)
have 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)
Tactic: apply sum_mem
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ (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)
have h₁ : coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (Fintype.card n - k)
Tactic: rw [coeff_smul, Submodule.smul_mem_iff']
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ ∑ x : n, 1 = Fintype.card n
have rw : HSMul.hSMul (β := ℕ) (card.{v} (α := n) univ) 1 = Fintype.card n
Tactic: rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
-- 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
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
⊢ ∑ x : n, 1 = Fintype.card n
have rw₁ : HSMul.hSMul (β := ℕ) (Fintype.card n) 1 = Fintype.card n
Tactic: rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
-- 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
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
⊢ ∑ x : n, 1 = Fintype.card n
have rw₂ : Fintype.card n * 1 = Fintype.card n
Tactic: rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
-- 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
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
⊢ ∑ x : n, 1 = Fintype.card n
have rw₃ : Fintype.card n = Fintype.card n
Tactic: rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (Fintype.card n - k)
have this : ∑ 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]
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (Fintype.card n - k)
have h₁ : coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (∑ x : n, 1 - k)
Tactic: rw [← this]
-- 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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ coeff (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (∑ x : n, 1 - k)
have h₁ : ∀ (i : n),
  Membership.mem (γ := Finset n) univ i → ∀ (k : ℕ), coeff (M.charmatrix ((c : (a : n) → n) i) i) k ∈ I ^ (1 - k)
Tactic: apply coeff_prod_mem_ideal_pow_tsub
-- 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
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
⊢ coeff (M.charmatrix ((c : (a : n) → n) i) i) 0 ∈ I ^ HSub.hSub (α := ℕ) 1 0
have h₁ : M ((c : (a : n) → n) i) i ∈ I
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]
-- 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
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 : ℕ
⊢ coeff (M.charmatrix ((c : (a : n) → n) i) i) (k + 1) ∈ I ^ (1 - (k + 1))
have h₁ : Membership.mem (γ := Ideal R) ⊤ (coeff (M.charmatrix ((c : (a : n) → n) i) i) (1 + k))
Tactic: rw [add_comm, tsub_self_add, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have a : Nontrivial R
Tactic: nontriviality R
-- 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
⊢ t_inv * t = 1
have rw : Eq.{u + 1} (α := R[T;T⁻¹]) (T (HAdd.hAdd (α := ℤ) (-1) 1)) 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- 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
rw : Eq.{u + 1} (α := R[T;T⁻¹]) (T (HAdd.hAdd (α := ℤ) (-1) 1)) 1
⊢ t_inv * t = 1
have rw₁ : Eq.{u + 1} (α := R[T;T⁻¹]) (T 0) 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- 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
rw : Eq.{u + 1} (α := R[T;T⁻¹]) (T (HAdd.hAdd (α := ℤ) (-1) 1)) 1
rw₁ : Eq.{u + 1} (α := R[T;T⁻¹]) (T 0) 1
⊢ t_inv * t = 1
have rw₂ : Eq.{u + 1} (α := R[T;T⁻¹]) 1 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have ht : t_inv * t = 1
Tactic: have ht : t_inv * t = 1 := by rw [← T_add, neg_add_cancel, T_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have hp : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have hq : (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]
-- 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
⊢ Eq (α := R[X]) (reverse M.charpoly) M.charpolyRev
have 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⁻¹])
Tactic: apply toLaurent_injective
-- 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
⊢ 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⁻¹]) ((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
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
⊢ 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⁻¹]) ((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
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]