awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 →₀ ℕ
⊢ Eq.{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
have h : Eq.{u_3 + 1} (α := R)
  (coeff (σ := Fin N) 0
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
  0
Tactic: obtain rfl | hd := eq_or_ne d 0
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 →₀ ℕ
h :
  Eq.{u_3 + 1} (α := R)
    (coeff (σ := Fin N) 0
      (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n))
    0
⊢ Eq.{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
have h₁ : ∀ (hd : d ≠ 0),
  Eq.{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
Tactic: obtain rfl | hd := eq_or_ne d 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 : d ≠ 0
⊢ Eq.{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
have h : ∀
  (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),
  d = 0
Tactic: contrapose! hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ d = 0
have h : ∀ (i : Fin N), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) ((0 : (a : Fin N) → ℕ) i : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
have pos : ∀ (hi : i ∈ d.support), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
Tactic: by_cases hi : i ∈ d.support
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
have neg : ∀ (hi : i ∉ d.support), Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
Tactic: by_cases hi : i ∈ d.support
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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 : ℕ)
have this : Eq (α := ℕ) ((weight 1 : (a : Fin N →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)
Tactic: have := hF.finSuccEquiv_coeff_isHomogeneous n 0 (add_zero _) hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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 (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
have this₁ : ∀ i ∈ d.support, Eq (α := ℕ) ((d : (a : Fin N) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ zero_le')] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ ∃ (r : Fin 0 → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
have h : Ne (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ Ne (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)
have h : ∀ (hF₀ : Eq (α := R) ((eval 0 : (a : MvPolynomial (Fin 0) R) → R) F : R) (0 : R)), F = 0
Tactic: contrapose hF₀
Cleared hypotheses: hF₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ F = 0
have h : ∀ (d : Fin 0 →₀ ℕ), coeff d F = coeff d 0
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
have 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
Tactic: linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have 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
Tactic: have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
      linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 : ℕ),
    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
have 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
Tactic: contrapose! hF₀
Cleared hypotheses: hF₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have 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)
Tactic: obtain ⟨i, hi⟩ : ∃ i : ℕ, (finSuccEquiv R N F).coeff i ≠ 0 := by
      contrapose! hF₀
      exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using hF₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
have 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
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have hin : 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have 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)
Tactic: obtain hFn | hFn := ne_or_eq ((finSuccEquiv R N F).coeff n) 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have 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)
Tactic: obtain hFn | hFn := ne_or_eq ((finSuccEquiv R N F).coeff n) 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ ∃ (r : Fin (N + 1) → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin (N + 1)) R) → R) F : R) (0 : R)
have hin₁ : i < n
Tactic: have hin : i < n := hin.lt_or_eq.elim id <| by aesop