-- Mathlib/RingTheory/PowerBasis.lean
theorem leftMulMatrix (pb : PowerBasis A S) : Algebra.leftMulMatrix pb.basis pb.gen =
    @Matrix.of (Fin pb.dim) (Fin pb.dim) _ fun i j =>
      if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0

Proof state:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = 0

Tactic:
convert pb.aeval_minpolyGen

Result:
case h.e'_2
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = (aeval pb.gen) pb.minpolyGen

Proof state:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨↑k + 1, ⋯⟩
⊢ (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0

Tactic:
rw [if_neg, zero_smul]

Result:
case neg.hnc
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨↑k + 1, ⋯⟩
⊢ ¬↑x = ↑k + 1

Proof state:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]

Result:
case neg.hc
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑⟨↑k + 1, ⋯⟩ = ↑k + 1

case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0

Proof state:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

Tactic:
simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]

Result:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = 0

Proof state:
case neg.hnc
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨↑k + 1, ⋯⟩
⊢ ¬↑x = ↑k + 1

Tactic:
apply mt Fin.ext hx

Result:
no goals

Proof state:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]

Result:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.lmul A S) pb.gen =
    (Matrix.toLin pb.basis pb.basis)
      (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)

Proof state:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.lmul A S) pb.gen =
    (Matrix.toLin pb.basis pb.basis)
      (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0)

Tactic:
refine pb.basis.ext fun k => ?_

Result:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ((Algebra.lmul A S) pb.gen) (pb.basis k) =
    ((Matrix.toLin pb.basis pb.basis)
        (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0))
      (pb.basis k)

Proof state:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
split_ifs with h

Result:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x : Fin pb.dim, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Proof state:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ((Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
apply (pow_succ' _ _).symm.trans

Result:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ pb.gen ^ (↑k + 1) =
    ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Proof state:
case h.e'_2
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = (aeval pb.gen) pb.minpolyGen

Tactic:
rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
  pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]

Result:
no goals

Proof state:
case inl
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
subsingleton

Result:
no goals

Proof state:
case neg.hc
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑⟨↑k + 1, ⋯⟩ = ↑k + 1

Tactic:
rfl

Result:
no goals

Proof state:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ((Algebra.lmul A S) pb.gen) (pb.basis k) =
    ((Matrix.toLin pb.basis pb.basis)
        (Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0))
      (pb.basis k)

Tactic:
simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]

Result:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
⊢ ((Algebra.lmul A S) pb.gen) (pb.gen ^ ↑k) =
    ∑ x : Fin pb.dim, (if ↑k + 1 = pb.dim then -pb.minpolyGen.coeff ↑x else if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x