-- Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.lean
theorem charpoly_leftMulMatrix {S : Type*} [Ring S] [Algebra R S] (h : PowerBasis R S) :
    (leftMulMatrix h.basis h.gen).charpoly = minpoly R h.gen

Proof state:
case inr
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

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

Result:
case inr.hp
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly = 0

case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree → q = 0 ∨ (aeval h.gen) q ≠ 0

Proof state:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : q.degree < ↑h.dim
h0 : ¬q = 0
⊢ (aeval h.gen) q ≠ 0

Tactic:
contrapose! hq

Result:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : (aeval h.gen) q = 0
⊢ ↑h.dim ≤ q.degree

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

case inr
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Proof state:
case inr.hp.a
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (leftMulMatrix h.basis) ((aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly) = 0

Tactic:
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Tactic:
subsingleton

Result:
no goals

Proof state:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : (aeval h.gen) q = 0
⊢ ↑h.dim ≤ q.degree

Tactic:
exact h.dim_le_degree_of_root h0 hq

Result:
no goals

Proof state:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree
h0 : ¬q = 0
⊢ (aeval h.gen) q ≠ 0

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

Result:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : q.degree < ↑h.dim
h0 : ¬q = 0
⊢ (aeval h.gen) q ≠ 0

Proof state:
case inr.hp
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly = 0

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

Result:
case inr.hp.a
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (leftMulMatrix h.basis) ((aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly) = 0

Proof state:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree → q = 0 ∨ (aeval h.gen) q ≠ 0

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

Result:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
hq : q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree
h0 : ¬q = 0
⊢ (aeval h.gen) q ≠ 0