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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]) -
          1).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (-(1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]))).det =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
Tactic: rw [← neg_sub, det_neg, det_one_sub_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
A : Matrix n n R
h : IsUnit A
this : Invertible A
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (-(1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]))).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X]) -
          1).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
have rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])).det) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 -
          HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det)
Tactic: rw [← neg_sub, det_neg, det_one_sub_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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X])
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (1 -
            HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A : Matrix.{v, v, u} n n R[X])).det) =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      A.charpolyRev
have simp : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X])
    (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
      (1 - HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → R[X]))).det) =
  HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
    (1 - HMul.hMul (α := Matrix.{v, v, u} n n R[X]) (diagonal fun (x : n) ↦ X) (A.map (⇑C : (a : R) → R[X]))).det
Tactic: simp [charpolyRev, 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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ A⁻¹.charpoly =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      A.charpolyRev
have _ : (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
      ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (A⁻¹ * A).det : R[X])
    (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det
Tactic: calc
  _ = (scalar n X - C.mapMatrix A⁻¹).det := rfl
  _ = C (A⁻¹ * A).det * (scalar n X - C.mapMatrix A⁻¹).det := by simp
  _ = C A⁻¹.det * C A.det * (scalar n X - C.mapMatrix A⁻¹).det := by rw [det_mul]; simp
  _ = C A⁻¹.det * (C A.det * (scalar n X - C.mapMatrix A⁻¹).det) := by ac_rfl
  _ = C A⁻¹.det * (C.mapMatrix A * (scalar n X - C.mapMatrix A⁻¹)).det := by simp [RingHom.map_det]
  _ = C A⁻¹.det * (C.mapMatrix A * scalar n X - 1).det := by rw [mul_sub, ← map_mul]; simp
  _ = C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - scalar n X * C.mapMatrix A).det) := by
    rw [← neg_sub, det_neg, det_one_sub_mul_comm]
  _ = _ := by simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl
-- 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
A : Matrix n n R
h : IsUnit A
this : Invertible A
_ :
  (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (A⁻¹ * A).det : R[X])
      (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
          ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det
⊢ A⁻¹.charpoly =
    HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) (-1) (Fintype.card n)) ((C : (a : R) → R[X]) A.det⁻¹ʳ : R[X]) *
      A.charpolyRev
have _₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (A⁻¹ * A).det : R[X])
    (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) A⁻¹.det : R[X]) ((C : (a : R) → R[X]) A.det : R[X]) *
    (HSub.hSub (α := Matrix.{v, v, u} n n R[X]) (β := Matrix.{v, v, u} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{v, v, u} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) A⁻¹ : Matrix.{v, v, u} n n R[X])).det
Tactic: calc
  _ = (scalar n X - C.mapMatrix A⁻¹).det := rfl
  _ = C (A⁻¹ * A).det * (scalar n X - C.mapMatrix A⁻¹).det := by simp
  _ = C A⁻¹.det * C A.det * (scalar n X - C.mapMatrix A⁻¹).det := by rw [det_mul]; simp
  _ = C A⁻¹.det * (C A.det * (scalar n X - C.mapMatrix A⁻¹).det) := by ac_rfl
  _ = C A⁻¹.det * (C.mapMatrix A * (scalar n X - C.mapMatrix A⁻¹)).det := by simp [RingHom.map_det]
  _ = C A⁻¹.det * (C.mapMatrix A * scalar n X - 1).det := by rw [mul_sub, ← map_mul]; simp
  _ = C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - scalar n X * C.mapMatrix A).det) := by
    rw [← neg_sub, det_neg, det_one_sub_mul_comm]
  _ = _ := by simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl
-- 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
⊢ eval 0 M.charpolyRev = 1
have rw : Eq.{u + 1} (α := R)
  (det.{u, v} (n := n)
    ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n R[X]) → Matrix n n R)
      (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))
  (det.{u, v} (n := n) 1)
Tactic: rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]
-- 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]))).map (eval 0) = 1
have a : ∀ (i j : n),
  (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j
Tactic: ext i j
-- 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 j : n
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j
have a : ∀ (hij : i = j),
  (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j
Tactic: rcases eq_or_ne i j with hij | hij
-- 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 j : n
a :
  ∀ (hij : i = j),
    (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
      1 i j
⊢ (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j
have a₁ : ∀ (hij : i ≠ j),
  (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) i j =
    1 i j
Tactic: rcases eq_or_ne i j with hij | hij
-- 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.{u + 1} (α := R)
    (det.{u, v} (n := n)
      ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix n n R[X]) → Matrix n n R)
        (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))
    (det.{u, v} (n := n) 1)
have this : (1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).map (eval 0) = 1
Tactic: have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
    ext i j; rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]
-- 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
⊢ coeff M.charpolyRev 1 = -M.trace
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
⊢ coeff M.charpolyRev 1 = -M.trace
have inl : IsEmpty n → coeff M.charpolyRev 1 = -M.trace
Tactic: cases isEmpty_or_nonempty n
-- 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
inl : IsEmpty n → coeff M.charpolyRev 1 = -M.trace
⊢ coeff M.charpolyRev 1 = -M.trace
have inr : Nonempty n → coeff M.charpolyRev 1 = -M.trace
Tactic: cases isEmpty_or_nonempty n
-- 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
hM : IsNilpotent M
⊢ IsUnit (M := R[X]) M.charpolyRev
have obtain : ∀ (k : ℕ) (hk : M ^ k = 0), IsUnit (M := R[X]) M.charpolyRev
Tactic: obtain ⟨k, hk⟩ := hM
Cleared hypotheses: hM
-- 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 : ℕ
hk : M ^ k = 0
⊢ 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
have h : 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
Tactic: convert! one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
-- 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 : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h : 1 =
  1 -
    HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
      k
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₁ : 1 =
  1 -
    HPow.hPow (α := R[X]) X k •
      HPow.hPow (α := Matrix.{v, v, u} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₂ : 1 =
  1 -
    HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
h₂ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₃ : 1 =
  1 -
    HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) 0)
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
h₂ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
h₃ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) 0)
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₄ : 1 = 1 - HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k) 0
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
h₂ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
h₃ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) 0)
h₄ : 1 = 1 - HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k) 0
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₅ : 1 = HSub.hSub (α := Matrix.{v, v, u} n n R[X]) 1 0
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
h :
  1 =
    1 -
      HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) ^
        k
h₁ :
  1 =
    1 -
      HPow.hPow (α := R[X]) X k •
        HPow.hPow (α := Matrix.{v, v, u} n n R[X])
          ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M : Matrix.{v, v, u} n n R[X]) k
h₂ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (M ^ k) : Matrix.{v, v, u} n n R[X])
h₃ :
  1 =
    1 -
      HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k)
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) 0)
h₄ : 1 = 1 - HSMul.hSMul (β := Matrix.{v, v, u} n n R[X]) (HPow.hPow (α := R[X]) X k) 0
h₅ : 1 = HSub.hSub (α := Matrix.{v, v, u} n n R[X]) 1 0
⊢ 1 = 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ^ k
have h₆ : Eq (α := Matrix.{v, v, u} n n R[X]) 1 1
Tactic: rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_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
k : ℕ
hk : M ^ k = 0
⊢ IsUnit (M := R[X]) M.charpolyRev
have hk₁ : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
Tactic: replace hk : 1 - (X : R[X]) • M.map C ∣ 1 := by
    convert! one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
    rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]
Cleared hypotheses: hk
-- 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 : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
⊢ IsUnit (M := R[X]) M.charpolyRev
have h : Dvd.dvd (α := R[X]) M.charpolyRev 1
Tactic: apply isUnit_of_dvd_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
k : ℕ
hk : 1 - HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])) ∣ 1
⊢ Dvd.dvd (α := R[X]) M.charpolyRev 1
have h : Dvd.dvd (α := R[X]) M.charpolyRev (det.{u, v} (n := n) 1)
Tactic: rw [← det_one (R := R[X]) (n := n)]
-- 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
hM : IsNilpotent M
⊢ IsNilpotent M.trace
have inl : IsEmpty n → IsNilpotent M.trace
Tactic: cases isEmpty_or_nonempty n
-- 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
hM : IsNilpotent M
inl : IsEmpty n → IsNilpotent M.trace
⊢ IsNilpotent M.trace
have inr : Nonempty n → IsNilpotent M.trace
Tactic: cases isEmpty_or_nonempty n