-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
private
lemma exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux
    {N : ℕ} {F : MvPolynomial (Fin (Nat.succ N)) R} {n : ℕ} (hF : IsHomogeneous F n)
    (hFn : ((finSuccEquiv R N) F).coeff n ≠ 0) :
    ∃ r, eval r F ≠ 0

Proof state:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
  linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]

Result:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ ∃ r, (eval r) F ≠ 0

Proof state:
case neg
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∉ d.support
⊢ d i = 0

Tactic:
simpa using hi

Result:
no goals

Proof state:
case h.a.inr.h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
⊢ d i = 0

Tactic:
by_cases hi : i ∈ d.support

Result:
case pos
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∈ d.support
⊢ d i = 0

case neg
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∉ d.support
⊢ d i = 0

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ (eval (Fin.cons 1 0)) F ≠ 0

Tactic:
simp_rw [eval_eq_eval_mv_eval', eval_one_map, Polynomial.eval_eq_sum_range' hdeg,
  eval_zero, one_pow, mul_one, map_sum, Finset.sum_range_succ, Finset.sum_eq_zero aux, zero_add]

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ constantCoeff (((finSuccEquiv R N) F).coeff n) ≠ 0

Proof state:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : n - i ≠ 0
⊢ 0 ≠ n - i

Tactic:
exact hi.symm

Result:
no goals

Proof state:
case pos
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∈ d.support
this : ∑ x ∈ d.support, d x = 0
⊢ d i = 0

Tactic:
rw [Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ zero_le')] at this

Result:
case pos
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∈ d.support
this : ∀ i ∈ d.support, d i = 0
⊢ d i = 0