awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq.{u_2 + 1} (α := Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        0 :
      Module.End R M)
⊢ Eq.{u_2 + 1} (α := Module.End R M)
    (((aeval
              ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
                  (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
                A) :
            AlgHom.{u_3, u_3, u_2} R R[X] (Module.End R M)) :
          (a : R[X]) → Module.End R M)
        (↑A : Matrix (↥s) (↥s) R).charpoly :
      Module.End R M)
    (0 : Module.End R M)

Tactic:
rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]

Premises used: map_zero, Matrix.isRepresentation.toEnd, Polynomial.aeval_algHom_apply, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq (α := ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly :
      ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (0 : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
⊢ Eq.{u_2 + 1} (α := Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Module.End R M)
    ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        0 :
      Module.End R M)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Matrix (↥s) (↥s) R)
    (↑0 : Matrix (↥s) (↥s) R)
⊢ Eq (α := ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly :
      ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (0 : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((aeval (↑A : Matrix (↥s) (↥s) R) : (a : R[X]) → Matrix (↥s) (↥s) R) (↑A : Matrix (↥s) (↥s) R).charpoly :
      Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((↑0 : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
inr₁ : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) 0 (↑0 : Matrix (↥s) (↥s) R)
inr₂ inr₃ : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) 0 0
⊢ Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Matrix (↥s) (↥s) R)
    (↑0 : Matrix (↥s) (↥s) R)

Tactic:
rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]

Premises used: Polynomial.aeval_subalgebra_coe, Subalgebra.coe_zero, Matrix.aeval_self_charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
⊢ range f ≤ HSMul.hSMul.{u_3, u_2, u_2} (α := Ideal R) (β := Submodule R M) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
        (0 : Module.End R M)

Tactic:
(LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero R f).imp
    fun _ h => h.imp_right And.right

Premises used: LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero, Exists.imp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Eq (α := R[X])
    (minpoly R (B := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R))
    (minpoly R M)

Tactic:
minpoly.algEquiv_eq (toLinAlgEquiv' : Matrix n n R ≃ₐ[R] _) M

Premises used: minpoly.algEquiv_eq, Matrix.toLinAlgEquiv'
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
b : Basis n R N
M : Matrix n n R
⊢ Eq (α := R[X]) (minpoly.{u, w} R (B := N →ₗ[R] N) ((toLin b b : (a : Matrix n n R) → N →ₗ[R] N) M : N →ₗ[R] N))
    (minpoly R M)

Tactic:
minpoly.algEquiv_eq (toLinAlgEquiv b : Matrix n n R ≃ₐ[R] _) M

Premises used: minpoly.algEquiv_eq, Matrix.toLinAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ IsIntegral R M

Tactic:
⟨M.charpoly, ⟨charpoly_monic M, aeval_self_charpoly M⟩⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, Matrix.aeval_self_charpoly, Matrix.charpoly_monic, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_1
inst_2 : Field K
M : Matrix n n K
⊢ Dvd.dvd (α := K[X]) (minpoly K M) M.charpoly

Tactic:
minpoly.dvd _ _ (aeval_self_charpoly M)

Premises used: minpoly.dvd, Matrix.aeval_self_charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] n → R
⊢ Eq (α := R[X])
    (minpoly R (B := Matrix n n R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R))
    (minpoly R f)

Tactic:
minpoly.algEquiv_eq (toMatrixAlgEquiv' : _ ≃ₐ[R] Matrix n n R) f

Premises used: LinearMap.toMatrixAlgEquiv', minpoly.algEquiv_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
b : Basis n R N
f : N →ₗ[R] N
⊢ Eq (α := R[X]) (minpoly R (B := Matrix n n R) ((toMatrix b b : (a : N →ₗ[R] N) → Matrix n n R) f : Matrix n n R))
    (minpoly R f)

Tactic:
minpoly.algEquiv_eq (toMatrixAlgEquiv b : _ ≃ₐ[R] Matrix n n R) f

Premises used: minpoly.algEquiv_eq, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
inl :
  Subsingleton R →
    Eq (α := R[X])
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
      (minpoly R h.gen)
inr :
  Nontrivial R →
    Eq (α := R[X])
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
      (minpoly R h.gen)
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Subsingleton R
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)

Tactic:
subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  Eq.{u_1 + 1} (α := S)
    ((aeval h.gen : (a : R[X]) → S)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      S)
    (0 : S)
inr₁ :
  ∀ (q : R[X]),
    q.degree <
        degree.{u} (R := R)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen)) →
      q = 0 ∨ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)

Tactic:
apply minpoly.unique' R h.gen (charpoly_monic _)

Premises used: PowerBasis.gen, Matrix.charpoly_monic, minpoly.unique'
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        ((aeval h.gen : (a : R[X]) → S)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen))) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)
⊢ Eq.{u_1 + 1} (α := S)
    ((aeval h.gen : (a : R[X]) → S)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      S)
    (0 : S)

Tactic:
apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp
      (leftMulMatrix_injective h.basis)

Premises used: Algebra.leftMulMatrix_injective, PowerBasis.basis, Algebra.leftMulMatrix, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((aeval
              (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                  (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
                h.gen) :
            R[X] →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
          (a : R[X]) → Matrix (Fin h.dim) (Fin h.dim) R)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)
inr₁ inr₂ : Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R) 0 0
⊢ Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        ((aeval h.gen : (a : R[X]) → S)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen))) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)

Tactic:
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]

Premises used: Matrix.aeval_self_charpoly, Polynomial.aeval_algHom_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
⊢ ∀ (q : R[X]),
    q.degree <
        degree.{u} (R := R)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen)) →
      q = 0 ∨ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)

Tactic:
fun q hq => or_iff_not_imp_left.2 fun h0 => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  ∀ (q : R[X])
    (hq :
      q.degree <
        degree.{u} (R := R)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen)))
    (h0 : ¬q = 0), Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
⊢ ∀ (q : R[X]),
    q.degree <
        degree.{u} (R := R)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen)) →
      q = 0 ∨ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)

Tactic:
refine fun q hq => or_iff_not_imp_left.2 fun h0 => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
hq :
  q.degree <
    degree.{u} (R := R)
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
h0 : ¬q = 0
⊢ q.degree < (↑h.dim : WithBot ℕ)

Tactic:
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq

Premises used: Fintype.card_fin, Matrix.charpoly_degree_eq_dim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
hq :
  q.degree <
    degree.{u} (R := R)
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
h0 : ¬q = 0
hq₁ : q.degree < (↑h.dim : WithBot ℕ)
⊢ ¬q = 0

Tactic:
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq

Premises used: Fintype.card_fin, Matrix.charpoly_degree_eq_dim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
hq : q.degree < (↑h.dim : WithBot ℕ)
h0 : ¬q = 0
inr : ∀ (hq : Eq.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)), (↑h.dim : WithBot ℕ) ≤ q.degree
⊢ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)

Tactic:
contrapose! hq
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : Eq.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
⊢ (↑h.dim : WithBot ℕ) ≤ q.degree

Tactic:
h.dim_le_degree_of_root h0 hq

Premises used: PowerBasis.dim_le_degree_of_root
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : Eq.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
⊢ (↑h.dim : WithBot ℕ) ≤ q.degree

Tactic:
exact h.dim_le_degree_of_root h0 hq

Premises used: PowerBasis.dim_le_degree_of_root
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
rw :
  Eq (α := Polynomial S) (map (mvPolynomialX n n R) (eval₂ f M)).charpoly
    (map (mvPolynomialX n n R)
        (eval₂ f fun (p : n × n) ↦ (of : (a : n → n → S) → Matrix n n S) (Function.curry M) p.1 p.2)).charpoly
⊢ Polynomial.map (eval₂Hom f M) (univ R n) =
    charpoly.{u_2, u_3} (n := n) ((of : (a : n → n → S) → Matrix n n S) (Function.curry M))

Tactic:
rw [univ, ← charpoly_map, coe_eval₂Hom, ← mvPolynomialX_map_eval₂ f (Matrix.of M.curry)]

Premises used: Matrix.charpoly_map, Matrix.charpoly.univ, Matrix.of, MvPolynomial.coe_eval₂Hom, Function.curry, Matrix.mvPolynomialX_map_eval₂, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
⊢ Eq (α := Polynomial S) (map (mvPolynomialX n n R) (eval₂ f M)).charpoly
    (map (mvPolynomialX n n R)
        (eval₂ f fun (p : n × n) ↦ (of : (a : n → n → S) → Matrix n n S) (Function.curry M) p.1 p.2)).charpoly

Tactic:
simp only [of_apply, Function.curry_apply, Prod.mk.eta]

Premises used: Matrix.of_apply, Function.curry_apply, Prod.mk.eta
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
rw :
  Eq (α := Polynomial (MvPolynomial.{u_3, u_2} (n × n) S))
    (charpoly (n := n)
      ((of : (a : n → n → MvPolynomial (n × n) S) → Matrix n n (MvPolynomial (n × n) S))
        (Function.curry MvPolynomial.X)))
    (univ S n)
⊢ Polynomial.map (MvPolynomial.map f) (univ R n) = univ S n

Tactic:
rw [MvPolynomial.map_eq_eval₂Hom_C_comp, univ_map_eval₂Hom]

Premises used: Matrix.charpoly.univ_map_eval₂Hom, MvPolynomial.map_eq_eval₂Hom_C_comp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
⊢ Eq (α := Polynomial (MvPolynomial.{u_3, u_2} (n × n) S))
    (charpoly (n := n)
      ((of : (a : n → n → MvPolynomial (n × n) S) → Matrix n n (MvPolynomial (n × n) S))
        (Function.curry MvPolynomial.X)))
    (univ S n)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
rw :
  (MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) =
    (Polynomial.map (MvPolynomial.eval₂Hom f M) (univ R n)).coeff i
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
    ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
    (Polynomial.coeff (charpoly.{u_2, u_3} (n := n) ((of : (a : n → n → S) → Matrix n n S) (Function.curry M))) i : S)

Tactic:
rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]

Premises used: Polynomial.coeff_map, Matrix.charpoly.univ_map_eval₂Hom
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Polynomial.Monic (R := MvPolynomial.{u_3, u_1} (n × n) R) (univ R n)

Tactic:
charpoly_monic (mvPolynomialX n n R)

Premises used: Matrix.charpoly_monic, Matrix.mvPolynomialX
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nontrivial R
⊢ Polynomial.natDegree (R := MvPolynomial.{u_3, u_1} (n × n) R) (univ R n) = Fintype.card n

Tactic:
charpoly_natDegree_eq_dim (mvPolynomialX n n R)

Premises used: Matrix.charpoly_natDegree_eq_dim, Matrix.mvPolynomialX