-- Mathlib/RingTheory/PowerBasis.lean
theorem dim_le_natDegree_of_root (pb : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0)
    (root : aeval pb.gen p = 0) : pb.dim ≤ p.natDegree

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ ∑ i : Fin pb.dim, (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
refine Fintype.sum_eq_zero _ fun i => ?_

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0
this : ∀ (i : Fin pb.dim), p.coeff ↑i = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
rw [this, monomial_zero_right]

Result:
no goals

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0
this : ∀ (i : Fin pb.dim), p.coeff ↑i = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
⊢ pb.dim ≤ p.natDegree

Tactic:
refine le_of_not_lt fun hlt => ne_zero ?_

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ p = 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ p = 0

Tactic:
rw [p.as_sum_range' _ hlt, Finset.sum_range]

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ ∑ i : Fin pb.dim, (monomial ↑i) (p.coeff ↑i) = 0