awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
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)
⊢ 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:
dsimp only [φ, F', F, renameEquiv_apply]

Premises used: MvPolynomial.renameEquiv_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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
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)
⊢ 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:
rw [finSuccEquiv_rename_finSuccEquiv, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply, MvPolynomial.finSuccEquiv_rename_finSuccEquiv
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
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 (Polynomial.map (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin k))) p) i : MvPolynomial (Fin k) R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
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
⊢ F ≠ 0

Tactic:
contrapose hFn
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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:
simp [hFn]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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

Tactic:
have hF₀ : F ≠ 0 := by contrapose hFn; simp [hFn]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
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
⊢ 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:
linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]

Premises used: MvPolynomial.natDegree_finSuccEquiv, MvPolynomial.degreeOf_le_totalDegree, MvPolynomial.IsHomogeneous.totalDegree, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_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

Tactic:
have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
    linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_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
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)
⊢ ∃ (r : Fin N.succ → R), Ne (α := R) ((eval r : (a : MvPolynomial (Fin N.succ) R) → R) F : R) (0 : R)

Tactic:
use Fin.cons 1 0

Premises used: Fin.cons, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
⊢ i < n

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
⊢ i + (n - i) = n

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
apply : (Finsupp.degree : (a : Fin N →₀ ℕ) → ℕ) 0 ≠ n - i
⊢ 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:
apply (hF.finSuccEquiv_coeff_isHomogeneous i (n - i) (by lia)).coeff_eq_zero

Premises used: HSub.hSub, MvPolynomial.IsHomogeneous.coeff_eq_zero, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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
⊢ n - i ≠ 0

Tactic:
rw [← Nat.sub_ne_zero_iff_lt] at hi

Premises used: Nat.sub_ne_zero_iff_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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 : n - i ≠ 0
⊢ 0 ≠ n - i

Tactic:
hi.symm

Premises used: Ne.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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 : n - i ≠ 0
⊢ 0 ≠ n - i

Tactic:
exact hi.symm

Premises used: Ne.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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 ∈ 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
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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)
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)
⊢ 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:
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]

Premises used: one_pow, Finset.sum_eq_zero, MvPolynomial.eval_eq_eval_mv_eval', map_sum, zero_add, MvPolynomial.eval_zero, Polynomial.eval_one_map, Polynomial.eval_eq_sum_range', mul_one, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
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)
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
⊢ 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:
contrapose hFn
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
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)
⊢ 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:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
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
⊢ 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:
rw [coeff_zero]

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
⊢ 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:
apply hFn
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg :
  natDegree.{u_3} (R := MvPolynomial (Fin N) R)
      ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) <
    n + 1
aux :
  ∀ i ∈ Finset.range n,
    Eq.{u_3 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
          (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F)
            i) :
        R)
      (0 : R)
hFn :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial (Fin N) R) → R)
        (Polynomial.coeff ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → (MvPolynomial (Fin N) R)[X]) F) n) :
      R)
    (0 : R)
d : Fin N →₀ ℕ
hd : d ≠ 0
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
⊢ 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:
contrapose! hd