awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
d : σ →₀ ℕ
hd : d ∈ p.support
a :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees

Tactic:
rw [Multiset.disjoint_iff_ne] at h

Premises used: Multiset.disjoint_iff_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
a : ∀ (hd : 0 ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
a₁ : ∀ (h0 : d ≠ 0), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees

Tactic:
obtain rfl | h0 := eq_or_ne d 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ 0 ≤ (p + q).degrees

Tactic:
apply Multiset.zero_le

Premises used: Multiset.zero_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees

Tactic:
Finset.le_sup_of_le (b := d) ?_ le_rfl

Premises used: le_rfl, Finset.le_sup_of_le, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
a : d ∈ (p + q).support
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees

Tactic:
refine Finset.le_sup_of_le (b := d) ?_ le_rfl

Premises used: le_rfl, Finset.le_sup_of_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
a : coeff d p + coeff d q ≠ 0
⊢ d ∈ (p + q).support

Tactic:
rw [mem_support_iff, coeff_add]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.coeff_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
rwa : coeff d p + 0 ≠ 0
rwa₁ : coeff d p ≠ 0
rwa₂ : Ne.{u + 1} (α := R) ((p : (a : σ →₀ ℕ) → R) d : R) (0 : R)
rwa₃ rwa₄ rwa₅ rwa₆ : d ∈ p.support
⊢ coeff d p + coeff d q ≠ 0

Tactic:
rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, MvPolynomial.coeff, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
a : coeff d q = 0
⊢ coeff d p + coeff d q ≠ 0

Tactic:
suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0

Premises used: Ne, Finset.nonempty_iff_ne_empty, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d.support.Nonempty
a : ∀ (j : σ) (hj : j ∈ d.support), coeff d q = 0
⊢ coeff d q = 0

Tactic:
obtain ⟨j, hj⟩ := h0
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
j : σ
hj : j ∈ d.support
a : ∀ (h : coeff d q ≠ 0), ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
⊢ coeff d q = 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ p.support
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : ∀ (hd : coeff d p ≠ 0) (j : σ) (hj : j ∈ d.support) (h : coeff d q ≠ 0), ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b

Tactic:
rw [mem_support_iff] at hd

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b

Tactic:
⟨j, ?_, j, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : j ∈ p.degrees
a₁ : j ∈ q.degrees
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b

Tactic:
refine ⟨j, ?_, j, ?_, rfl⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ j ∈ d.support
⊢ j ∈ p.degrees

Tactic:
rw [mem_degrees]

Premises used: MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ j ∈ d.support

Tactic:
⟨d, ?_, hj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : coeff d p ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ j ∈ d.support

Tactic:
refine ⟨d, ?_, hj⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d p ≠ 0

Tactic:
assumption
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : ∃ (d : σ →₀ ℕ), coeff d q ≠ 0 ∧ j ∈ d.support
⊢ j ∈ q.degrees

Tactic:
rw [mem_degrees]

Premises used: MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d q ≠ 0 ∧ j ∈ d.support

Tactic:
⟨d, ?_, hj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h a : coeff d q ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d q ≠ 0 ∧ j ∈ d.support

Tactic:
refine ⟨d, ?_, hj⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0

Tactic:
assumption
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
a a₁ : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
a₂ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
a₃ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (hd : 0 ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
a₄ a₅ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support) (h0 : d ≠ 0),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
⊢ p.degrees ≤ (p + q).degrees

Tactic:
classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption

Premises used: Finsupp.toMultiset_zero, MvPolynomial.mem_support_iff, Ne, Finset.nonempty_iff_ne_empty, Finset.sup_le, MvPolynomial.coeff_add, Finsupp.support_eq_empty, MvPolynomial.mem_degrees, Multiset.zero_le, rfl, Multiset.disjoint_iff_ne
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ q.degrees ≤ (p + q).degrees

Tactic:
simpa [add_comm] using le_degrees_add_left h.symm

Premises used: add_comm, Disjoint.symm, MvPolynomial.le_degrees_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.degrees q.degrees
⊢ (p + q).degrees = p.degrees ∪ q.degrees

Tactic:
degrees_add_le.antisymm <| Multiset.union_le (le_degrees_add_left h) (le_degrees_add_right h)

Premises used: LE.le.antisymm, Multiset.union_le, MvPolynomial.degrees_add_le, MvPolynomial.le_degrees_add_right, MvPolynomial.le_degrees_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
⊢ degrees.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) ≤ p.degrees

Tactic:
Finset.sup_mono <| support_map_subset ..

Premises used: MvPolynomial.support_map_subset, Finset.sup_mono, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
⊢ degrees.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) ≤ p.degrees

Tactic:
exact Finset.sup_mono <| support_map_subset ..

Premises used: MvPolynomial.support_map_subset, Finset.sup_mono
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
⊢ degrees.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) ≤ p.degrees

Tactic:
classical exact Finset.sup_mono <| support_map_subset ..

Premises used: MvPolynomial.support_map_subset, Finset.sup_mono
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
rw :
  (∃ (d : τ →₀ ℕ),
      Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
    ∃ a ∈ φ.degrees, f a = i
⊢ Membership.mem (γ := Multiset τ)
      (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
    i ∈ Multiset.map f φ.degrees

Tactic:
rw [mem_degrees, Multiset.mem_map]

Premises used: Multiset.mem_map, MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : i ∈ d.support
obtain :
  ∀ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd

Premises used: MvPolynomial.coeff_rename_ne_zero, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi

Premises used: Finsupp.mem_support_iff, Finsupp.mapDomain
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0

Tactic:
rw [sum_apply, Finsupp.sum] at hi

Premises used: Finsupp.sum, Finsupp.sum_apply
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
contrapose! :
  ∀ (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
    Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
contrapose! hi
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i
rw :
  ∀ x_1 ∈ x.support,
    Eq (α := ℕ) (((Finsupp.single (f x_1) ((x : (a : σ) → ℕ) x_1) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0

Tactic:
rw [Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i
j : σ
hj : j ∈ x.support
⊢ ∀ (a : σ) (_ : ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ a ∈ d.support), f a ≠ i

Tactic:
simp only [mem_degrees] at hi

Premises used: MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ) (_ : ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ a ∈ d.support), f a ≠ i
⊢ f j ≠ i

Tactic:
specialize hi j ⟨x, hx, hj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
rw : Eq (α := ℕ) (if f j = i then (x : (a : σ) → ℕ) j else 0 : ℕ) (0 : ℕ)
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
rw [Finsupp.single_apply, if_neg hi]

Premises used: Finsupp.single_apply, if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ degrees.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) = p.degrees

Tactic:
simp only [degrees, MvPolynomial.support_map_of_injective _ hf]

Premises used: MvPolynomial.support_map_of_injective, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
simp :
  p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = Multiset.map f p.degrees

Tactic:
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]

Premises used: Finsupp.toMultiset, MvPolynomial.support_rename_of_injective, MvPolynomial.support, Multiset.map_finset_sup, Finset.sup_image, DFunLike.coe, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))

Tactic:
Finset.sup_congr rfl fun x _ => ?_

Premises used: Finset.sup_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
refine :
  ∀ x ∈ p.support,
    ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
      (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x
⊢ p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))

Tactic:
refine Finset.sup_congr rfl fun x _ => ?_

Premises used: Finset.sup_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
h_1 : x ∈ p.support
⊢ ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
    (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x

Tactic:
(Finsupp.toMultiset_map _ _).symm

Premises used: Multiset.map, Eq.symm, Finsupp.toMultiset_map
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
h_1 : x ∈ p.support
⊢ ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
    (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x

Tactic:
exact (Finsupp.toMultiset_map _ _).symm

Premises used: Eq.symm, Finsupp.toMultiset_map
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
simp :
  p.support.sup ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) =
    p.support.sup (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ))
simp₁ :
  ∀ x ∈ p.support,
    ((fun (s : τ →₀ ℕ) ↦ (toMultiset : (a : τ →₀ ℕ) → Multiset τ) s) ∘ Finsupp.mapDomain f) x =
      (Multiset.map f ∘ (⇑toMultiset : (a : σ →₀ ℕ) → Multiset σ)) x
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = Multiset.map f p.degrees

Tactic:
classical
  simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]
  refine Finset.sup_congr rfl fun x _ => ?_
  exact (Finsupp.toMultiset_map _ _).symm

Premises used: Finset.sup_image, Finset.sup_congr, Eq.symm, MvPolynomial.degrees, Finsupp.toMultiset_map, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw :
  Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n

Tactic:
rw [degreeOf_def, degrees, Multiset.count_finset_sup]

Premises used: MvPolynomial.degreeOf_def, Multiset.count_finset_sup, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
e_f :
  Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
⊢ Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
e_f : ∀ (x : σ →₀ ℕ), Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) x) = (x : (a : σ) → ℕ) n
⊢ Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
x : σ →₀ ℕ
⊢ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) x) = (x : (a : σ) → ℕ) n

Tactic:
simp only [count_toMultiset]

Premises used: Finsupp.count_toMultiset
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
rw : Multiset.count n f.degrees = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₁ :
  Multiset.count n (f.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) =
    f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
rw₂ rw₃ rw₄ :
  Eq (α := ℕ) (f.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
e_f :
  Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (a : σ →₀ ℕ) ↦ Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n
e_f₁ : ∀ (x : σ →₀ ℕ), Multiset.count n ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) x) = (x : (a : σ) → ℕ) n
⊢ degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n

Tactic:
classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]

Premises used: MvPolynomial.degreeOf_def, Finsupp.count_toMultiset, Multiset.count_finset_sup, MvPolynomial.degrees