awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
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)
⊢ 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)
have 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)
Tactic: simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]
-- 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
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)
⊢ 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)
have 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)
Tactic: simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]
-- 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
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)
⊢ 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)
have 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)
Tactic: simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]
-- 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
⊢ (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
have 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
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]
-- 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
⊢ (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
have 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
Tactic: convert! (divX_mul_X_add _).symm
-- 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
⊢ 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
have 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
Tactic: rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_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
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
⊢ 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
have h₁ : Eq.{u + 1} (α := R) 1 (eval 0 (det.{u, v} (n := n) 1))
Tactic: rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_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
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))
⊢ 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
have h₂ : Eq.{u + 1} (α := R) 1 (eval 0 1)
Tactic: rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_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
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)
⊢ 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
have h₃ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
⊢ Nonempty n
have rw : 0 < Fintype.card n
Tactic: rw [← Fintype.card_pos_iff]
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
⊢ 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])
have this : Nonempty n
Tactic: have : Nonempty n := by rw [← Fintype.card_pos_iff]; lia
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ 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])
have 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
Tactic: ext i
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
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
have 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
Tactic: by_cases hi : i ∈ Finset.range 3
-- 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
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
⊢ 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
have 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
Tactic: by_cases hi : i ∈ Finset.range 3
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
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
have 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
Tactic: fin_cases hi
Cleared hypotheses: i, hi
-- 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
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
⊢ 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
have 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
Tactic: fin_cases hi
Cleared hypotheses: i, hi
-- 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
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
⊢ 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
have 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
Tactic: fin_cases hi
Cleared hypotheses: i, hi
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
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
have hi₁ : 2 < i
Tactic: rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi
Cleared hypotheses: hi
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < 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
have neg : coeff M.charpoly i = 0
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]
-- 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
inst_3 : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
⊢ coeff M.charpoly i = 0
have neg : natDegree M.charpoly < i
Tactic: apply coeff_eq_zero_of_natDegree_lt
-- 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
⊢ (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])
have 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
Tactic: ext m i j
-- 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
⊢ 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
have 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
Tactic: rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply,
    AlgHom.coe_toRingHom, coeff_X_pow]
-- 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
⊢ 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 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
Tactic: by_cases hij : i = j
-- 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
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
⊢ 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 : ∀ (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
Tactic: by_cases hij : i = j
-- 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 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
Tactic: rw [hij, charmatrix_apply_eq, map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, 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 = 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
have pos : ∀ (mp : m = k) (m0 : m = 0), 1 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) j j
Tactic: split_ifs with mp m0
-- 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 : ∀ (mp : m = k) (m0 : m = 0), 1 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 1 (M ^ k) 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
have 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
Tactic: split_ifs with mp m0
-- 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 : ∀ (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
⊢ ((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
have pos₁ : ∀ (mp : ¬m = k), m = 0 → 0 - (M ^ k) j j = HSub.hSub (α := Matrix n n K) 0 (M ^ k) j j
Tactic: split_ifs with mp m0
-- 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 : ∀ (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
⊢ ((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
have 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
Tactic: split_ifs with mp m0