awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
hF.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux hFn

Premises used: _private.0.MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux
-- 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
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)

Tactic:
exact hF.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux hFn

Premises used: _private.0.MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux
-- 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
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
⊢ i = n → i < n

Tactic:
aesop
-- 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
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
⊢ i < n

Tactic:
have hin : i < n := hin.lt_or_eq.elim id <| by aesop
-- 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_1 : i ≤ n
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
hin : i < n
⊢ ∀ (a : ℕ), n = i + a + 1 → i + (a + 1) = n

Tactic:
lia
-- 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_1 : i ≤ n
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
hin : i < n
succ :
  ∀ (j : ℕ) (hj : i + (j + 1) = n),
    ∃ (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 ⟨j, hj⟩ : ∃ j, i + (j + 1) = n := (Nat.exists_eq_add_of_lt hin).imp <| by lia

Premises used: Exists.imp, Nat.exists_eq_add_of_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
hin_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
norm_cast : j + 1 ≤ n
⊢ LE.le.{u_5 + 1} (α := Cardinal.{u_5}) (↑(j + 1) : Cardinal.{u_5}) (↑n : Cardinal.{u_5})

Tactic:
norm_cast
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
⊢ j + 1 ≤ n

Tactic:
lia
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
succ :
  ∀ (r : Fin N → R)
    (hr :
      Ne (α := R)
        ((eval r : (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)),
    ∃ (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 ⟨r, hr⟩ : ∃ r, (eval r) (Polynomial.coeff ((finSuccEquiv R N) F) i) ≠ 0 :=
      IH (hF.finSuccEquiv_coeff_isHomogeneous _ _ hj) hi (.trans (by norm_cast; lia) hnR)

Premises used: LE.le.trans, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
⊢ let φ : R[X] :=
    Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F);
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)

Tactic:
set φ : R[X] := Polynomial.map (eval r) (finSuccEquiv _ _ F) with hφ

Premises used: MvPolynomial.finSuccEquiv, MvPolynomial.eval, Polynomial.map, DFunLike.coe
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ = 0
rw :
  Polynomial.coeff
      (Polynomial.map (eval r)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F))
      i =
    0
rw₁ : φ.coeff i = 0
rw₂ : Eq.{u_5 + 1} (α := R) (Polynomial.coeff 0 i) 0
rw₃ rw₄ : Eq.{u_5 + 1} (α := R) 0 0
⊢ Eq (α := R)
    ((eval r : (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)

Tactic:
rw [← coeff_eval_eq_eval_coeff, ← hφ, hφ₀, Polynomial.coeff_zero]

Premises used: Polynomial.coeff_zero, MvPolynomial.coeff_eval_eq_eval_coeff
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
⊢ φ ≠ 0

Tactic:
have hφ₀ : φ ≠ 0 := fun hφ₀ ↦ hr <| by
      rw [← coeff_eval_eq_eval_coeff, ← hφ, hφ₀, Polynomial.coeff_zero]
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
⊢ (↑φ.natDegree : Cardinal.{u_5}) < #R

Tactic:
lt_of_lt_of_le ?_ hnR

Premises used: lt_of_lt_of_le
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
refine : LT.lt.{u_5 + 1} (α := Cardinal.{u_5}) (↑φ.natDegree : Cardinal.{u_5}) (↑n : Cardinal.{u_5})
⊢ (↑φ.natDegree : Cardinal.{u_5}) < #R

Tactic:
refine lt_of_lt_of_le ?_ hnR

Premises used: lt_of_lt_of_le
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
norm_cast : φ.natDegree < n
⊢ LT.lt.{u_5 + 1} (α := Cardinal.{u_5}) (↑φ.natDegree : Cardinal.{u_5}) (↑n : Cardinal.{u_5})

Tactic:
norm_cast
-- 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_1 : i ≤ n
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
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr :
  Ne (α := R)
    ((eval r : (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)
φ : R[X] :=
  Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ :
  φ = Polynomial.map (eval r) ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hφ₀ : φ ≠ 0
⊢ φ.natDegree < n

Tactic:
lt_of_le_of_lt natDegree_map_le ?_

Premises used: lt_of_le_of_lt, Polynomial.natDegree_map_le