awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
h : ∀ (i : Fin N), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) ((0 : (a : Fin N) → ℕ) i : ℕ)
⊢ d = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
pos : ∀ (hi : i ∈ d.support), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
neg : ∀ (hi : i ∉ d.support), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
by_cases hi : i ∈ d.support

Premises used: Finsupp.support
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∈ d.support
⊢ Eq (α := ℕ) ((weight 1 : (a : Fin N →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)

Tactic:
have := hF.finSuccEquiv_coeff_isHomogeneous n 0 (add_zero _) hd
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∈ d.support
this : Eq (α := ℕ) ((weight 1 : (a : Fin N →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (∑ x ∈ d.support, (d : (a : Fin N) → ℕ) x) 0

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum] at this

Premises used: Pi.one_apply, Finsupp.sum, smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∈ d.support
this : Eq (α := ℕ) (∑ x ∈ d.support, (d : (a : Fin N) → ℕ) x) 0
⊢ ∀ i ∈ d.support, Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)

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

Premises used: Finset.sum_eq_zero_iff_of_nonneg, zero_le'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∈ d.support
this : ∀ i ∈ d.support, Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
this i hi
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∈ d.support
this : ∀ i ∈ d.support, Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
exact this i hi
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
i : Fin N
hi : i ∉ d.support
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simpa using hi
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
h : Ne (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
⊢ ∃ (r : Fin 0 → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)

Tactic:
use 0
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
h : ∀ (hF₀ : Eq (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)), F = 0
⊢ Ne (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)

Tactic:
contrapose hF₀
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hF₀ : Eq (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
h : ∀ (d : Fin 0 →₀ ℕ), coeff d F = coeff d 0
⊢ F = 0

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hF₀ : Eq (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
d : Fin 0 →₀ ℕ
⊢ coeff d F = coeff d 0

Tactic:
simpa only [Subsingleton.elim d 0, eval_zero, coeff_zero] using hF₀

Premises used: MvPolynomial.eval_zero, MvPolynomial.coeff_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
linarith :
  n + 1 ≤
      natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) →
    -1 +
              (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 -
                (↑(natDegree.{u_5} (R := MvPolynomial (Fin N) R)
                      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
                  ℤ)) +
            HSub.hSub (α := ℤ)
              (↑(natDegree.{u_5} (R := MvPolynomial (Fin N) R)
                    ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
                ℤ)
              (↑(degreeOf 0 F) : ℤ) +
          HSub.hSub (α := ℤ) (↑(degreeOf 0 F) : ℤ) (↑F.totalDegree : ℤ) +
        HSub.hSub (α := ℤ) (↑F.totalDegree : ℤ) (↑n : ℤ) =
      0
⊢ natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1

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

Premises used: MvPolynomial.natDegree_finSuccEquiv, MvPolynomial.degreeOf_le_totalDegree, MvPolynomial.IsHomogeneous.totalDegree, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
⊢ natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1

Tactic:
have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
      linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
contrapose! :
  ∀
    (hF₀ :
      ∀ (i : ℕ),
        Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i)
          0),
    F = 0
⊢ ∃ (i : ℕ),
    Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0

Tactic:
contrapose! hF₀
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
hF₀ :
  ∀ (i : ℕ),
    Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
⊢ ∀ (n : ℕ),
    Eq (α := MvPolynomial (Fin N) R)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) 0) n)

Tactic:
simpa using hF₀
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
hF₀ :
  ∀ (i : ℕ),
    Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
⊢ F = 0

Tactic:
exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using hF₀

Premises used: Polynomial.ext, MvPolynomial.finSuccEquiv, AlgEquiv.injective
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
succ :
  ∀ (i : ℕ)
    (hi :
      Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i)
        0),
    ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)

Tactic:
obtain ⟨i, hi⟩ : ∃ i : ℕ, (finSuccEquiv R N F).coeff i ≠ 0 := by
      contrapose! hF₀
      exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using hF₀
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
contrapose! :
  ∀ (hi : n < i),
    Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
⊢ i ≤ n

Tactic:
contrapose! hi
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi : n < i
⊢ Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0

Tactic:
coeff_eq_zero_of_natDegree_lt <| (Nat.le_of_lt_succ hdeg).trans_lt hi

Premises used: Nat.le_of_lt_succ, Polynomial.coeff_eq_zero_of_natDegree_lt, LE.le.trans_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi : n < i
⊢ Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| (Nat.le_of_lt_succ hdeg).trans_lt hi

Premises used: Nat.le_of_lt_succ, Polynomial.coeff_eq_zero_of_natDegree_lt, LE.le.trans_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
⊢ i ≤ n

Tactic:
have hin : i ≤ n := by
      contrapose! hi
      exact coeff_eq_zero_of_natDegree_lt <| (Nat.le_of_lt_succ hdeg).trans_lt hi
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
N : ℕ
IH :
  ∀ {F : MvPolynomial (Fin N) R} {n : ℕ} (hF : F.IsHomogeneous n) (hF₀ : F ≠ 0) (hnR : (↑n : Cardinal.{u_5}) ≤ #R),
    ∃ (r : Fin N → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N) R) → R) F : R) (0 : R)
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : (↑n : Cardinal.{u_5}) ≤ #R
hdeg :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
i : ℕ
hi :
  Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) i) 0
hin : i ≤ n
succ :
  ∀
    (hFn :
      Ne.{u_5 + 1} (α := MvPolynomial (Fin N) R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n)
        0),
    ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
succ₁ :
  ∀
    (hFn :
      Eq.{u_5 + 1} (α := MvPolynomial (Fin N) R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n)
        0),
    ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)

Tactic:
obtain hFn | hFn := ne_or_eq ((finSuccEquiv R N F).coeff n) 0

Premises used: ne_or_eq, MvPolynomial.finSuccEquiv, Polynomial.coeff, OfNat.ofNat, DFunLike.coe