-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
private
lemma exists_eval_ne_zero_of_totalDegree_le_card_aux {N : ℕ} {F : MvPolynomial (Fin N) R} {n : ℕ}
    (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : n ≤ #R) :
    ∃ r, eval r F ≠ 0

Proof state:
case succ.intro.inr.intro.intro.intro
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hφR : ↑φ.natDegree < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
use Fin.cons r₀ r

Result:
case h
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hφR : ↑φ.natDegree < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
⊢ (eval (Fin.cons r₀ r)) F ≠ 0

Proof state:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
⊢ ((finSuccEquiv R N) F).natDegree < n + 1

Tactic:
linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]

Result:
no goals

Proof state:
case succ.intro.inr
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
have hin : i < n := hin.lt_or_eq.elim id <| by aesop

Result:
case succ.intro.inr
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
⊢ ∃ r, (eval r) F ≠ 0

Proof state:
case succ
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
obtain ⟨i, hi⟩ : ∃ i : ℕ, (finSuccEquiv R N F).coeff i ≠ 0 := by
  contrapose! hF₀
  exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using hF₀

Result:
case succ.intro
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Proof state:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
hF₀ : F ≠ 0
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
j : ℕ
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hF : F.IsHomogeneous ((finSuccEquiv R N) F).natDegree
hnR : ↑((finSuccEquiv R N) F).natDegree ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < ((finSuccEquiv R N) F).natDegree + 1
hin✝ : i ≤ ((finSuccEquiv R N) F).natDegree
hFn : ((finSuccEquiv R N) F).coeff ((finSuccEquiv R N) F).natDegree = 0
hin : i < ((finSuccEquiv R N) F).natDegree
hj : i + (j + 1) = ((finSuccEquiv R N) F).natDegree
⊢ False

Tactic:
refine leadingCoeff_ne_zero.mpr ?_ hFn

Result:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
hF₀ : F ≠ 0
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
j : ℕ
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hF : F.IsHomogeneous ((finSuccEquiv R N) F).natDegree
hnR : ↑((finSuccEquiv R N) F).natDegree ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < ((finSuccEquiv R N) F).natDegree + 1
hin✝ : i ≤ ((finSuccEquiv R N) F).natDegree
hFn : ((finSuccEquiv R N) F).coeff ((finSuccEquiv R N) F).natDegree = 0
hin : i < ((finSuccEquiv R N) F).natDegree
hj : i + (j + 1) = ((finSuccEquiv R N) F).natDegree
⊢ (finSuccEquiv R N) F ≠ 0

Proof state:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
this : ((finSuccEquiv R N) F).natDegree ≠ n
⊢ ((finSuccEquiv R N) F).natDegree < n

Tactic:
omega

Result:
no goals