awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
x x_1 : σ →₀ ℕ
⊢ ((x + x_1).sum fun (x : σ) (e : ℕ) ↦ e) =
    HAdd.hAdd (α := ℕ) (x.sum fun (x : σ) (e : ℕ) ↦ e) (x_1.sum fun (x : σ) (e : ℕ) ↦ e)

Tactic:
exact Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) = s.sum fun (x : σ) (e : ℕ) ↦ e

Tactic:
simp [totalDegree, support_monomial, if_neg hc]

Premises used: MvPolynomial.support_monomial, MvPolynomial.totalDegree, if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) = s.sum fun (x : σ) (e : ℕ) ↦ e

Tactic:
classical simp [totalDegree, support_monomial, if_neg hc]

Premises used: MvPolynomial.support_monomial, MvPolynomial.totalDegree, if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c = 0
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id

Tactic:
simp only [hc, map_zero, totalDegree_zero, zero_le]

Premises used: zero_le, map_zero, MvPolynomial.totalDegree_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
rw : LE.le (α := ℕ) (s.sum fun (x : σ) (e : ℕ) ↦ e) (s.sum fun (x : σ) ↦ id)
rw₁ rw₂ : LE.le (α := ℕ) (s.sum fun (x : σ) (e : ℕ) ↦ e) (s.sum fun (x : σ) (e : ℕ) ↦ e)
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id

Tactic:
rw [totalDegree_monomial _ hc, Function.id_def]

Premises used: MvPolynomial.totalDegree_monomial, Function.id_def
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
if :
  ∀ (hc : c = 0),
    totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
if₁ :
  ∀ (hc : ¬c = 0),
    totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
if₂ :
  ∀ (hc : c = 0),
    totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
if₃ if₄ :
  ∀ (hc : ¬c = 0),
    totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id

Tactic:
if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]

Premises used: zero_le, Function.id_def, map_zero, MvPolynomial.totalDegree_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
n : ℕ
⊢ (HPow.hPow (α := MvPolynomial σ R) (X s) n).totalDegree = n

Tactic:
simp [X_pow_eq_monomial, one_ne_zero]

Premises used: MvPolynomial.X_pow_eq_monomial, one_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
l : List (MvPolynomial σ R)
⊢ l.prod.totalDegree ≤ (List.map totalDegree l).sum

Tactic:
l.apply_prod_le_sum_map _ totalDegree_one.le totalDegree_mul

Premises used: List.apply_prod_le_sum_map, Eq.le, MvPolynomial.totalDegree_one, MvPolynomial.totalDegree_mul
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : Multiset (MvPolynomial σ R)
⊢ s.prod.totalDegree ≤ (Multiset.map totalDegree s).sum

Tactic:
s.apply_prod_le_sum_map _ totalDegree_one.le totalDegree_mul

Premises used: Eq.le, Multiset.apply_prod_le_sum_map, MvPolynomial.totalDegree_one, MvPolynomial.totalDegree_mul
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree

Tactic:
s.apply_prod_le_sum_apply _ totalDegree_one.le totalDegree_mul

Premises used: Finset.apply_prod_le_sum_apply, Eq.le, MvPolynomial.totalDegree_one, MvPolynomial.totalDegree_mul
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ (Finset.sum ∅ f).totalDegree ≤ Finset.sup ∅ fun (i : ι) ↦ (f i).totalDegree

Tactic:
zero_le

Premises used: zero_le, Multiset.foldr, Finset.fold, MvPolynomial.totalDegree, Finset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ (Finset.sum ∅ f).totalDegree ≤ Finset.sup ∅ fun (i : ι) ↦ (f i).totalDegree

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
cons : (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun (i : ι) ↦ (f i).totalDegree)
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun (i : ι) ↦ (f i).totalDegree

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Premises used: Finset.sum_cons, Finset.sup_cons
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun (i : ι) ↦ (f i).totalDegree)

Tactic:
(MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

Premises used: le_rfl, MvPolynomial.totalDegree_add, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun (i : ι) ↦ (f i).totalDegree)

Tactic:
exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

Premises used: le_rfl, MvPolynomial.totalDegree_add, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
empty : (Finset.sum ∅ f).totalDegree ≤ Finset.sup ∅ fun (i : ι) ↦ (f i).totalDegree
cons :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree),
    ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun (i : ι) ↦ (f i).totalDegree
⊢ (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree

Tactic:
induction s using Finset.cons_induction with
  | empty => exact zero_le
  | cons a s has hind =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

Premises used: zero_le, Finset.sum_cons, Finset.sup_cons
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
d : ℕ
hf : ∀ i ∈ s, (f i).totalDegree ≤ d
⊢ (s.sum f).totalDegree ≤ d

Tactic:
(totalDegree_finsetSum ..).trans <| Finset.sup_le hf

Premises used: Finset.sup_le, MvPolynomial.totalDegree_finsetSum, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → (d : (a : σ) → ℕ) i ≤ f.totalDegree

Tactic:
lia
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
h : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∀ i ∈ d.support, LE.le (α := ℕ) (0 : ℕ) ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : f.totalDegree < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ f.support
contrapose! : ∀ (h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i), n * Fintype.card σ ≤ f.totalDegree
⊢ ∃ (i : σ), (d : (a : σ) → ℕ) i < n

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
rw : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ • n
rw₁ : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ * n
rw₂ : Fintype.card σ * n = Finset.card.{u_1} (α := σ) Finset.univ * n
rw₃ rw₄ : Fintype.card σ * n = Fintype.card σ * n
⊢ n * Fintype.card σ = ∑ _s : σ, n

Tactic:
rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]

Premises used: Finset.card_univ, Nat.nsmul_eq_mul, mul_comm, Finset.sum_const
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
⊢ LE.le (α := ℕ) (∑ _s : σ, n) (∑ s : σ, (d : (a : σ) → ℕ) s)

Tactic:
Finset.sum_le_sum fun s _ => h s

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
h₁ : ∀ (i : σ), Eq (α := ℕ) 0 0
⊢ LE.le (α := ℕ) (∑ s : σ, (d : (a : σ) → ℕ) s) (d.sum fun (x : σ) (e : ℕ) ↦ e)

Tactic:
rw [Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
i : σ
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ f.totalDegree

Tactic:
le_totalDegree hd

Premises used: MvPolynomial.le_totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
n₁ : n * Fintype.card σ = ∑ _s : σ, n
n₂ : LE.le (α := ℕ) (∑ s : σ, (d : (a : σ) → ℕ) s) (d.sum fun (x : σ) (e : ℕ) ↦ e)
⊢ n * Fintype.card σ ≤ f.totalDegree

Tactic:
calc
    n * Fintype.card σ = ∑ _s : σ, n := by
      rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
    _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
    _ ≤ d.sum fun _ e => e := by
      rw [Finsupp.sum_fintype]
      intros
      rfl
    _ ≤ f.totalDegree := le_totalDegree hd

Premises used: Finsupp.sum, Fintype.card, MvPolynomial.totalDegree, Finset.sum_le_sum, MvPolynomial.le_totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
rw :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₁ :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0

Tactic:
rw [totalDegree, Finset.sup_lt_iff] at h

Premises used: Finset.sup_lt_iff, MvPolynomial.totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ d ∈ f.support → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
specialize h d
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ f.support → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
rw [mem_support_iff] at h

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0

Tactic:
not_not.mp (mt h ?_)

Premises used: Classical.not_not, mt, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
refine : ¬LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0

Tactic:
refine not_not.mp (mt h ?_)

Premises used: Classical.not_not, mt, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ ¬LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
lt_irrefl _

Premises used: lt_irrefl, Finsupp.sum
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ ¬LT.lt (α := ℕ) (d.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
exact lt_irrefl _

Premises used: lt_irrefl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h :
  LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
lt_of_le_of_lt (Nat.zero_le _) h

Premises used: Nat.zero_le, lt_of_le_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h :
  LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)

Tactic:
exact lt_of_le_of_lt (Nat.zero_le _) h

Premises used: Nat.zero_le, lt_of_le_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, (d : (a : σ) → ℕ) i
rw :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₁ :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₂ :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
rw₃ :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₄ :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
rw₅ :
  ∀ (h : ∀ b ∈ f.support, LT.lt (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    coeff d f = 0
rw₆ rw₇ :
  ∀
    (h :
      LT.lt (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
        (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)),
    LT.lt (α := ℕ) ⊥ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i)
⊢ coeff d f = 0

Tactic:
classical
    rw [totalDegree, Finset.sup_lt_iff] at h
    · specialize h d
      rw [mem_support_iff] at h
      refine not_not.mp (mt h ?_)
      exact lt_irrefl _
    · exact lt_of_le_of_lt (Nat.zero_le _) h

Premises used: Nat.zero_le, lt_of_le_of_lt, lt_irrefl, MvPolynomial.mem_support_iff, Finset.sup_lt_iff, MvPolynomial.totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
mp : p.totalDegree = 0 → p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
mpr : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p) → p.totalDegree = 0
⊢ p.totalDegree = 0 ↔ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
mp : ∀ (m : σ →₀ ℕ), coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)

Tactic:
ext m
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
mp : coeff m p = if 0 = m then coeff 0 p else 0
⊢ coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))

Tactic:
rw [coeff_C]

Premises used: MvPolynomial.coeff_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
pos : ∀ (hm : 0 = m), coeff m p = coeff 0 p
neg : ∀ (hm : ¬0 = m), coeff m p = 0
⊢ coeff m p = if 0 = m then coeff 0 p else 0

Tactic:
split_ifs with hm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
pos pos₁ : coeff 0 p = coeff 0 p
⊢ coeff m p = coeff 0 p

Tactic:
rw [← hm]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
neg : ∀ (hm : ¬0 = m), coeff m p = 0
⊢ coeff m p = coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))

Tactic:
classical rw [coeff_C]; split_ifs with hm; · rw [← hm]

Premises used: MvPolynomial.coeff_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
neg : p.totalDegree < ∑ i ∈ m.support, (m : (a : σ) → ℕ) i
⊢ coeff m p = 0

Tactic:
apply coeff_eq_zero_of_totalDegree_lt

Premises used: MvPolynomial.coeff_eq_zero_of_totalDegree_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
neg : LT.lt (α := ℕ) 0 (∑ i ∈ m.support, (m : (a : σ) → ℕ) i)
⊢ p.totalDegree < ∑ i ∈ m.support, (m : (a : σ) → ℕ) i

Tactic:
rw [h]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ LT.lt (α := ℕ) 0 (∑ i ∈ m.support, (m : (a : σ) → ℕ) i)

Tactic:
Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.sum_pos, Ne.symm, Finsupp.support_nonempty_iff, Nat.pos_of_ne_zero, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ LT.lt (α := ℕ) 0 (∑ i ∈ m.support, (m : (a : σ) → ℕ) i)

Tactic:
exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.sum_pos, Ne.symm, Finsupp.support_nonempty_iff, Nat.pos_of_ne_zero, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
mpr : totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p)) = 0
mpr₁ mpr₂ : Eq (α := ℕ) 0 0
⊢ p.totalDegree = 0

Tactic:
rw [h, totalDegree_C]

Premises used: MvPolynomial.totalDegree_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h :
  Membership.mem (γ := Finset (τ →₀ ℕ))
    (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b
⊢ b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)

Tactic:
rw [rename_eq] at h

Premises used: MvPolynomial.rename_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ b ∈ Finset.image (Finsupp.mapDomain f) p.support

Tactic:
have h' := Finsupp.mapDomain_support h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ ∃ a ∈ p.support, Finsupp.mapDomain f a = b

Tactic:
rw [Finset.mem_image] at h'

Premises used: Finset.mem_image
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b
rcases :
  ∀ (s : σ →₀ ℕ) (hs : s ∈ p.support) (h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)),
    ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
rcases h' with ⟨s, hs, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
(sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Premises used: Finsupp.sum_mapDomain_index, Eq.trans_le, MvPolynomial.le_totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Premises used: Finsupp.sum_mapDomain_index, Eq.trans_le