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_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 :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n
⊢ φ.natDegree < n

Tactic:
refine lt_of_le_of_lt natDegree_map_le ?_

Premises used: lt_of_le_of_lt, Polynomial.natDegree_map_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
this :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) ≠
    n
⊢ natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    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
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
suffices :
  natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) ≠
    n
⊢ natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n

Tactic:
suffices (finSuccEquiv _ _ F).natDegree ≠ n by 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
hF₀ : F ≠ 0
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
j : ℕ
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
hF :
  F.IsHomogeneous
    (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F))
hnR :
  (↑(natDegree.{u_5} (R := MvPolynomial (Fin N) R)
          ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
      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) <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) +
      1
hin_1 :
  i ≤
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
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)
      (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)))
    0
hin :
  i <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hj :
  i + (j + 1) =
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
⊢ False

Tactic:
leadingCoeff_ne_zero.mpr ?_ hFn

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_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
hF₀ : F ≠ 0
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
j : ℕ
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
hF :
  F.IsHomogeneous
    (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F))
hnR :
  (↑(natDegree.{u_5} (R := MvPolynomial (Fin N) R)
          ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
      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) <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) +
      1
hin_1 :
  i ≤
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
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)
      (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)))
    0
hin :
  i <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hj :
  i + (j + 1) =
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
refine :
  Ne (α := (MvPolynomial (Fin N) R)[X])
    ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F :
      (MvPolynomial (Fin N) R)[X])
    (0 : (MvPolynomial (Fin N) R)[X])
⊢ False

Tactic:
refine leadingCoeff_ne_zero.mpr ?_ hFn

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_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
hF₀ : F ≠ 0
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
j : ℕ
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
hF :
  F.IsHomogeneous
    (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F))
hnR :
  (↑(natDegree.{u_5} (R := MvPolynomial (Fin N) R)
          ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
      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) <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) +
      1
hin_1 :
  i ≤
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
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)
      (natDegree.{u_5} (R := MvPolynomial (Fin N) R)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)))
    0
hin :
  i <
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
hj :
  i + (j + 1) =
    natDegree.{u_5} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
⊢ Ne (α := (MvPolynomial (Fin N) R)[X])
    ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F :
      (MvPolynomial (Fin N) R)[X])
    (0 : (MvPolynomial (Fin N) R)[X])

Tactic:
simpa using (finSuccEquiv R N).injective.ne hF₀

Premises used: Function.Injective.ne, 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
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:
have hφR : φ.natDegree < #R := by
      refine lt_of_lt_of_le ?_ hnR
      norm_cast
      refine lt_of_le_of_lt natDegree_map_le ?_
      suffices (finSuccEquiv _ _ F).natDegree ≠ n by lia
      rintro rfl
      refine leadingCoeff_ne_zero.mpr ?_ hFn
      simpa using (finSuccEquiv R N).injective.ne 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
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
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
⊢ ∃ (r₀ : R), Polynomial.eval r₀ φ ≠ 0

Tactic:
φ.exists_eval_ne_zero_of_natDegree_lt_card hφ₀ hφR

Premises used: Polynomial.exists_eval_ne_zero_of_natDegree_lt_card
-- 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
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
succ :
  ∀ (r₀ : R) (hr₀ : Polynomial.eval r₀ φ ≠ 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 ⟨r₀, hr₀⟩ : ∃ r₀, Polynomial.eval r₀ φ ≠ 0 :=
      φ.exists_eval_ne_zero_of_natDegree_lt_card hφ₀ hφR

Premises used: Polynomial.exists_eval_ne_zero_of_natDegree_lt_card
-- 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
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
h :
  Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin (N + 1)) ↦ R) r₀ 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:
use Fin.cons r₀ r

Premises used: Fin.cons
-- 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
hφR : (↑φ.natDegree : Cardinal.{u_5}) < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
h h₁ h₂ h₃ :
  Polynomial.eval r₀
      (Polynomial.map (eval r)
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) ≠
    0
⊢ Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin (N + 1)) ↦ R) r₀ r) : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R)
    (0 : R)

Tactic:
rwa [eval_eq_eval_mv_eval']

Premises used: MvPolynomial.eval_eq_eval_mv_eval'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
inst_1 : IsDomain R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), Eq.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
hnR : (↑n : Cardinal.{u_5}) ≤ #R
contrapose! : ∀ (h : F ≠ 0), ∃ (r : σ → R), Ne.{u_5 + 1} (α := R) ((eval r : (a : MvPolynomial σ R) → R) F : R) (0 : R)
⊢ F = 0

Tactic:
contrapose! h