awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
i : m
j : n
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.inr 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.inr j)).coeff
      n_1

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
i : n
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.inr 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.inr i) (Sum.inl j)).coeff
      n_1

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
i j : n
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.inr i) (Sum.inr 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.inr i) (Sum.inr j)).coeff
      n_1

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 → α
rw : BlockTriangular (R := R[X]) (M.map (⇑C : (a : R) → R[X])) b ↔ M.BlockTriangular b
⊢ BlockTriangular (R := R[X]) M.charmatrix b ↔ M.BlockTriangular b

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]

Premises used: RingHom.mapMatrix_apply, Matrix.BlockTriangular.sub_iff_right, Matrix.blockTriangular_diagonal, Matrix.charmatrix, Matrix.scalar_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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.map (⇑C : (a : R) → R[X])) b ↔ M.BlockTriangular b

Tactic:
simp [BlockTriangular]

Premises used: Matrix.BlockTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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
⊢ 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

Tactic:
rw [Matrix.charpoly, ← Polynomial.coe_evalRingHom, RingHom.map_det, Matrix.charmatrix]

Premises used: Matrix.charmatrix, RingHom.map_det, Polynomial.coe_evalRingHom, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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
⊢ (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:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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
⊢ (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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 : 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:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
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:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : IsEmpty n
A : Matrix n n R
⊢ Eq (α := R[X]) A.charpoly 1

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ charpoly.{u_1, u_4} (n := n) 0 = HPow.hPow (α := R[X]) X (Fintype.card n)

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
⊢ Eq (α := R[X]) (diagonal d).charpoly
    (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ charpoly.{u_1, u_4} (n := n) 1 = HSub.hSub (α := R[X]) X 1 ^ Fintype.card n

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
k : ℕ
⊢ charpoly.{u_1, u_4} (n := n) (↑k : Matrix n n R) = HSub.hSub (α := R[X]) X (↑k : R[X]) ^ Fintype.card n

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
k : ℕ
inst_3 : k.AtLeastTwo
⊢ charpoly.{u_1, u_4} (n := n) (OfNat.ofNat k) = HSub.hSub (α := R[X]) X (OfNat.ofNat k) ^ Fintype.card n

Tactic:
charpoly_natCast _

Premises used: Matrix.charpoly_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 (α := R[X]) Mᵀ.charpoly M.charpoly

Tactic:
simp [charpoly]

Premises used: Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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)
rw₁ rw₂ : Eq (α := R[X]) (det 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)

Tactic:
rw [charmatrix_reindex, Matrix.det_reindex_self]

Premises used: Matrix.charmatrix_reindex, Matrix.det_reindex_self
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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))
rw₅ 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])))
⊢ charpoly (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]

Premises used: RingHom.mapMatrix_apply, Polynomial.coe_mapRingHom, RingHom.map_det, Matrix.charmatrix_map, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 n m R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = HMul.hMul (α := R[X]) M₁₁.charpoly M₂₂.charpoly

Tactic:
simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero,
    det_fromBlocks_zero₁₂]

Premises used: Matrix.map_zero, Polynomial.C_0, Matrix.charmatrix_fromBlocks, Matrix.det_fromBlocks_zero₁₂, neg_zero, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 n R
⊢ (fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = HMul.hMul (α := R[X]) M₁₁.charpoly M₂₂.charpoly

Tactic:
simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero,
    det_fromBlocks_zero₂₁]

Premises used: Matrix.map_zero, Polynomial.C_0, Matrix.charmatrix_fromBlocks, Matrix.det_fromBlocks_zero₂₁, neg_zero, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 : α
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)
⊢ 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)

Tactic:
ext i j : 1
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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 : α
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:
simp [charmatrix_apply, toSquareBlock_def, diagonal_apply, Subtype.ext_iff]

Premises used: Matrix.toSquareBlock_def, Subtype.ext_iff, Matrix.diagonal_apply, Matrix.charmatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
b : n → α
inst_3 : LinearOrder α
h : M.BlockTriangular b
⊢ Eq (α := R[X]) M.charpoly (∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly)

Tactic:
simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock]

Premises used: Matrix.charmatrix_toSquareBlock, Matrix.BlockTriangular.charmatrix, Matrix.BlockTriangular.det, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : LinearOrder n
M : Matrix n n R
h : M.BlockTriangular id
⊢ Eq (α := R[X]) M.charpoly (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))

Tactic:
simp [charpoly, det_of_upperTriangular h.charmatrix]

Premises used: Matrix.BlockTriangular.charmatrix, Matrix.det_of_upperTriangular, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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)[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

Premises used: matPolyEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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])
⊢ (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

Premises used: Matrix.matPolyEquiv_charmatrix, map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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]))
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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])))
⊢ 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

Premises used: Polynomial.eval_mul_X_sub_C
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
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)) =
    0
⊢ eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0

Tactic:
rw [matPolyEquiv_smul_one, eval_map] at h

Premises used: Polynomial.eval_map, matPolyEquiv_smul_one