awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
pos :
  ∀ (h : i = j),
    Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
      (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
⊢ Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
have neg : ∀ (h : ¬i = j),
  Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
⊢ charmatrix (M.map (⇑f : (a : R) → S)) = map M.charmatrix (Polynomial.map f)
have a : ∀ (i j : n) (n_1 : ℕ),
  coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n_1 : ℕ
⊢ coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
have pos : ∀ (h : i = j),
  coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n_1 : ℕ
pos :
  ∀ (h : i = j),
    coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
⊢ coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
have neg : ∀ (h : ¬i = j),
  coeff (charmatrix (M.map (⇑f : (a : R) → S)) i j) n_1 = (map M.charmatrix (Polynomial.map f) i j).coeff n_1
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
      ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
      ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
          (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
        Matrix (m ⊕ n) (m ⊕ n) R[X]) =
    fromBlocks
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
      (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
      (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
have a : ∀ (i j : m) (n_1 : ℕ),
  (HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
              (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
            Matrix (m ⊕ n) (m ⊕ n) R[X])
          (Sum.inl i) (Sum.inl j)).coeff
      n_1 =
    (fromBlocks
          (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
          (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
          (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
          (Sum.inl i) (Sum.inl j)).coeff
      n_1
Tactic: ext (i | i) (j | j) : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
α : Type u_5
inst_3 : Preorder α
M : Matrix n n R
b : n → α
⊢ BlockTriangular (R := R[X]) M.charmatrix b ↔ M.BlockTriangular b
have rw : BlockTriangular (R := R[X]) (M.map (⇑C : (a : R) → R[X])) b ↔ M.BlockTriangular b
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
t : R
⊢ eval t M.charpoly = (HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M).det
have rw : det.{u_1, u_3} (n := m)
    ((RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))) =
  (HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M).det
Tactic: rw [Matrix.charpoly, ← Polynomial.coe_evalRingHom, RingHom.map_det, Matrix.charmatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
t : R
⊢ det.{u_1, u_3} (n := m)
      ((RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
        (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
          ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
          ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))) =
    (HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M).det
have e_M : (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
    (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
      ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
      ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X])) =
  HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
t : R
⊢ (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X])) =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M
have e_M : ∀ (i j : m),
  (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
      i j =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
t : R
i j : m
⊢ (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
      i j =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i j
have e_M : (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
    (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
      ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
      ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
    i i =
  HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i i
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
t : R
i j : m
e_M :
  (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
      i i =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i i
⊢ (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
      i j =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i j
have e_M₁ : ∀ (hij : i ≠ j),
  (RingHom.mapMatrix (evalRingHom t) : (a : Matrix m m R[X]) → Matrix m m R)
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M : Matrix.{u_3, u_3, u_1} m m R[X]))
      i j =
    HSub.hSub (α := Matrix m m R) ((scalar m : (a : R) → Matrix m m R) t : Matrix m m R) M i j
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
e : n ≃ m
M : Matrix n n R
⊢ Eq (α := R[X]) (det.{u_1, u_3} (n := m) (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M)))
    (det M.charmatrix)
have rw : Eq (α := R[X]) (det.{u_1, u_3} (n := m) ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix))
  (det M.charmatrix)
Tactic: rw [charmatrix_reindex, Matrix.det_reindex_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
e : n ≃ m
M : Matrix n n R
rw :
  Eq (α := R[X]) (det.{u_1, u_3} (n := m) ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix))
    (det M.charmatrix)
⊢ Eq (α := R[X]) (det.{u_1, u_3} (n := m) (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M)))
    (det M.charmatrix)
have rw₁ : Eq (α := R[X]) (det M.charmatrix) (det M.charmatrix)
Tactic: rw [charmatrix_reindex, Matrix.det_reindex_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw₁ : (map M.charmatrix (Polynomial.map f)).det = Polynomial.map f M.charpoly
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
rw₁ : (map M.charmatrix (Polynomial.map f)).det = Polynomial.map f M.charpoly
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw₂ : Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
  ((mapRingHom f : (a : R[X]) → S[X]) M.charpoly : S[X])
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
rw₁ : (map M.charmatrix (Polynomial.map f)).det = Polynomial.map f M.charpoly
rw₂ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) M.charpoly : S[X])
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw₃ : Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
  ((mapRingHom f : (a : R[X]) → S[X]) (det M.charmatrix) : S[X])
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
rw₁ : (map M.charmatrix (Polynomial.map f)).det = Polynomial.map f M.charpoly
rw₂ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) M.charpoly : S[X])
rw₃ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) (det M.charmatrix) : S[X])
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw₄ : Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])))
  (det.{u_2, u_4} (n := n) (((mapRingHom f).mapMatrix : (a : Matrix n n R[X]) → Matrix n n S[X]) M.charmatrix))
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : Type u_4
inst_2 : DecidableEq n
inst_3 : Fintype n
M : Matrix n n R
f : R →+* S
rw : det (charmatrix (M.map (⇑f : (a : R) → S))) = Polynomial.map f M.charpoly
rw₁ : (map M.charmatrix (Polynomial.map f)).det = Polynomial.map f M.charpoly
rw₂ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) M.charpoly : S[X])
rw₃ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) (det M.charmatrix) : S[X])
rw₄ :
  Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])))
    (det.{u_2, u_4} (n := n) (((mapRingHom f).mapMatrix : (a : Matrix n n R[X]) → Matrix n n S[X]) M.charmatrix))
⊢ charpoly (M.map (⇑f : (a : R) → S)) = Polynomial.map f M.charpoly
have rw₅ : Eq.{u_2 + 1} (α := S[X]) (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])))
  (det (map (α := R[X]) M.charmatrix (⇑(mapRingHom f) : (a : R[X]) → S[X])))
Tactic: rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
    RingHom.mapMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
α : Type u_5
inst_3 : DecidableEq α
b : n → α
a : α
⊢ Eq (α := Matrix.{u_4, u_4, u_1} { a_1 : n // b a_1 = a } { a_1 : n // b a_1 = a } R[X])
    (M.toSquareBlock b a).charmatrix (toSquareBlock M.charmatrix b a)
have a₁ : ∀ (i j : { a_1 : n // b a_1 = a }),
  Eq (α := R[X]) ((M.toSquareBlock b a).charmatrix i j) (toSquareBlock M.charmatrix b a i j)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)
have h : HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1 =
  HMul.hMul (α := Matrix.{u_4, u_4, u_1} n n R[X]) (adjugate M.charmatrix) M.charmatrix
Tactic: have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M :=
    (adjugate_mul _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h :
  HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1 =
    HMul.hMul (α := Matrix.{u_4, u_4, u_1} n n R[X]) (adjugate M.charmatrix) M.charmatrix
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)
have h₁ : Eq (α := (Matrix n n R)[X])
  ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1) :
    (Matrix n n R)[X])
  ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
      (HMul.hMul (α := Matrix.{u_4, u_4, u_1} n n R[X]) (adjugate M.charmatrix) M.charmatrix) :
    (Matrix n n R)[X])
Tactic: apply_fun matPolyEquiv at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h :
  Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1) :
      (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        (HMul.hMul (α := Matrix.{u_4, u_4, u_1} n n R[X]) (adjugate M.charmatrix) M.charmatrix) :
      (Matrix n n R)[X])
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)
have h₁ : (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
    (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1) =
  HMul.hMul (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (adjugate M.charmatrix) : (Matrix n n R)[X])
    (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
      ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X]))
Tactic: simp only [map_mul, matPolyEquiv_charmatrix] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h :
  (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1) =
    HMul.hMul (α := (Matrix n n R)[X])
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (adjugate M.charmatrix) : (Matrix n n R)[X])
      (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
        ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X]))
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)
have h₁ : eval M
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1)) =
  eval M
    (HMul.hMul (α := (Matrix n n R)[X])
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (adjugate M.charmatrix) : (Matrix n n R)[X])
      (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
        ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])))
Tactic: apply_fun fun p => p.eval M at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h :
  eval M
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1)) =
    eval M
      (HMul.hMul (α := (Matrix n n R)[X])
        ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (adjugate M.charmatrix) : (Matrix n n R)[X])
        (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])))
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)
have h₁ : eval M
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1)) =
  0
Tactic: rw [eval_mul_X_sub_C] at h
Cleared hypotheses: h