awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → Polynomial (MvPolynomial (Fin N) R)) φ) i))
    0
⊢ (weight 1 : (a : Fin N →₀ ℕ) → ℕ) d = j
have hd₁ : coeff (cons i d) φ ≠ 0
Tactic: rw [finSuccEquiv_coeff_coeff] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ (weight 1 : (a : Fin N →₀ ℕ) → ℕ) d = j
have h' : (weight 1 : (a : Fin (N + 1) →₀ ℕ) → ℕ) (cons i d) = i + j
Tactic: have h' : (weight 1) (Finsupp.cons i d) = i + j := by
    simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
h' : (weight 1 : (a : Fin (N + 1) →₀ ℕ) → ℕ) (cons i d) = i + j
⊢ (weight 1 : (a : Fin N →₀ ℕ) → ℕ) d = j
have simp : ∀ (h' : (d.sum fun (x : Fin N) (e : ℕ) ↦ e) = j), (d.sum fun (i : Fin N) (c : ℕ) ↦ c) = j
Tactic: simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum_cons,
    add_right_inj] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
⊢ (p.coeff i).IsHomogeneous j
have obtain : ∀ (k : ℕ) (e : σ ≃ Fin k), (p.coeff i).IsHomogeneous j
Tactic: obtain ⟨k, ⟨e⟩⟩ := Finite.exists_equiv_fin σ
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
⊢ (p.coeff i).IsHomogeneous j
have hφ : φ.IsHomogeneous n
Tactic: have hφ : φ.IsHomogeneous n := hp.rename_isHomogeneous
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
this :
  IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
⊢ (p.coeff i).IsHomogeneous j
have rwa : IsHomogeneous.{0, u_3} (σ := Fin k) (R := R)
  ((rename (⇑e : (a : σ) → Fin k) : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
Tactic: rwa [← (IsHomogeneous.rename_isHomogeneous_iff e.injective)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
⊢ (p.coeff i).IsHomogeneous j
have suffices : IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
Tactic: suffices IsHomogeneous (F (p.coeff i)) j by
    rwa [← (IsHomogeneous.rename_isHomogeneous_iff e.injective)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
⊢ IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
have h₁ : Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
  ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) : MvPolynomial (Fin k) R)
  (Polynomial.coeff ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R)) φ)
      i :
    MvPolynomial (Fin k) R)
Tactic: convert! hφ.finSuccEquiv_coeff_isHomogeneous i j h using 1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
⊢ Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
    ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) : MvPolynomial (Fin k) R)
    (Polynomial.coeff ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R)) φ)
        i :
      MvPolynomial (Fin k) R)
have h₁ : Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
  ((rename (⇑e : (a : σ) → Fin k) : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) :
    MvPolynomial (Fin k) R)
  (Polynomial.coeff
      ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R))
        ((rename (⇑e' : (a : Option σ) → Fin (k + 1)) : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
          ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)))
      i :
    MvPolynomial (Fin k) R)
Tactic: dsimp only [φ, F', F, renameEquiv_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
⊢ Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
    ((rename (⇑e : (a : σ) → Fin k) : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) :
      MvPolynomial (Fin k) R)
    (Polynomial.coeff
        ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R))
          ((rename (⇑e' : (a : Option σ) → Fin (k + 1)) :
              (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
            ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R)
              p)))
        i :
      MvPolynomial (Fin k) R)
have h₁ : Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
  ((rename (⇑e : (a : σ) → Fin k) : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) :
    MvPolynomial (Fin k) R)
  (Polynomial.coeff (Polynomial.map (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin k))) p) i : MvPolynomial (Fin k) R)
Tactic: rw [finSuccEquiv_rename_finSuccEquiv, AlgEquiv.apply_symm_apply]
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
⊢ F ≠ 0
have contrapose : ∀ (hFn : F = 0),
  Eq.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
Tactic: contrapose hFn
Cleared hypotheses: hFn
-- 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
hFn :
  Ne.{u_3 + 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.succ → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N.succ) R) → R) F : R) (0 : R)
have hF₀ : F ≠ 0
Tactic: have hF₀ : F ≠ 0 := by contrapose hFn; simp [hFn]
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
hF₀ : F ≠ 0
⊢ 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
have linarith : n + 1 ≤
    natDegree.{u_3} (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_3} (R := MvPolynomial (Fin N) R)
                    ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)) :
                ℤ)) +
          HSub.hSub (α := ℤ)
            (↑(natDegree.{u_3} (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_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
hF₀ : F ≠ 0
⊢ ∃ (r : Fin N.succ → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N.succ) R) → R) F : R) (0 : R)
have 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
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_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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
⊢ ∃ (r : Fin N.succ → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N.succ) R) → R) F : R) (0 : R)
have h : Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin N.succ) ↦ R) 1 0) : (a : MvPolynomial (Fin N.succ) R) → R) F : R)
  (0 : R)
Tactic: use Fin.cons 1 0
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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
i : ℕ
hi : 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)
have hi₁ : i < n
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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
i : ℕ
hi : i < 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)
have apply : (Finsupp.degree : (a : Fin N →₀ ℕ) → ℕ) 0 ≠ n - i
Tactic: apply (hF.finSuccEquiv_coeff_isHomogeneous i (n - i) (by lia)).coeff_eq_zero
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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
i : ℕ
hi : i < n
⊢ 0 ≠ n - i
have hi₁ : n - i ≠ 0
Tactic: rw [← Nat.sub_ne_zero_iff_lt] at hi
Cleared hypotheses: hi
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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
⊢ Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin N.succ) ↦ R) 1 0) : (a : MvPolynomial (Fin N.succ) R) → R) F : R)
    (0 : R)
have 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)
Tactic: have aux : ∀ i ∈ Finset.range n, constantCoeff ((finSuccEquiv R N F).coeff i) = 0 := by
    intro i hi
    rw [Finset.mem_range] at hi
    apply (hF.finSuccEquiv_coeff_isHomogeneous i (n - i) (by lia)).coeff_eq_zero
    simp only [map_zero]
    rw [← Nat.sub_ne_zero_iff_lt] at hi
    exact hi.symm
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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)
⊢ Ne (α := R) ((eval (Fin.cons (α := fun (a : Fin N.succ) ↦ R) 1 0) : (a : MvPolynomial (Fin N.succ) R) → R) F : R)
    (0 : R)
have h : Ne.{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)
Tactic: simp_rw [eval_eq_eval_mv_eval', eval_one_map, Polynomial.eval_eq_sum_range' hdeg,
    eval_zero, one_pow, mul_one, map_sum, Finset.sum_range_succ, Finset.sum_eq_zero aux, zero_add]
-- 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
hFn :
  Ne.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
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)
⊢ Ne.{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)
have h : ∀
  (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)),
  Eq.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
Tactic: contrapose hFn
Cleared hypotheses: hFn
-- 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)
⊢ Eq.{u_3 + 1} (α := MvPolynomial (Fin N) R)
    (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) 0
have h : ∀ (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))
    (coeff d 0)
Tactic: ext 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 →₀ ℕ
⊢ 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))
    (coeff d 0)
have h : 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: rw [coeff_zero]