[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ degrees p = Finset.sup (support p) fun s => ↑toMultiset s
[PROOFSTEP]
rw [degrees]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => ↑toMultiset s) = Finset.sup (support p) fun s => ↑toMultiset s
[PROOFSTEP]
convert rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
⊢ degrees (↑(monomial s) a) ≤ ↑toMultiset s
[PROOFSTEP]
classical
refine' Finset.sup_le fun t h => _
have := Finsupp.support_single_subset h
rw [Finset.mem_singleton] at this
rw [this]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
⊢ degrees (↑(monomial s) a) ≤ ↑toMultiset s
[PROOFSTEP]
refine' Finset.sup_le fun t h => _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
⊢ ↑toMultiset t ≤ ↑toMultiset s
[PROOFSTEP]
have := Finsupp.support_single_subset h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t ∈ {s}
⊢ ↑toMultiset t ≤ ↑toMultiset s
[PROOFSTEP]
rw [Finset.mem_singleton] at this
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t = s
⊢ ↑toMultiset t ≤ ↑toMultiset s
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ degrees (↑(monomial s) a) = ↑toMultiset s
[PROOFSTEP]
classical
refine' le_antisymm (degrees_monomial s a) <| Finset.le_sup <| _
rw [support_monomial, if_neg ha, Finset.mem_singleton]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ degrees (↑(monomial s) a) = ↑toMultiset s
[PROOFSTEP]
refine' le_antisymm (degrees_monomial s a) <| Finset.le_sup <| _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ s ∈ support (↑(monomial s) a)
[PROOFSTEP]
rw [support_monomial, if_neg ha, Finset.mem_singleton]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ degrees 0 = 0
[PROOFSTEP]
rw [← C_0]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ degrees (↑C 0) = 0
[PROOFSTEP]
exact degrees_C 0
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ degrees (p + q) ≤ degrees p ⊔ degrees q
[PROOFSTEP]
classical
simp_rw [degrees_def]
refine' Finset.sup_le fun b hb => _
have := Finsupp.support_add hb; rw [Finset.mem_union] at this
cases' this with h h
· exact le_sup_of_le_left (Finset.le_sup h)
· exact le_sup_of_le_right (Finset.le_sup h)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ degrees (p + q) ≤ degrees p ⊔ degrees q
[PROOFSTEP]
simp_rw [degrees_def]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (Finset.sup (support (p + q)) fun s => ↑toMultiset s) ≤
    (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
refine' Finset.sup_le fun b hb => _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
have := Finsupp.support_add hb
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∪ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
rw [Finset.mem_union] at this
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∨ b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
cases' this with h h
[GOAL]
case inl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ p.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
exact le_sup_of_le_left (Finset.le_sup h)
[GOAL]
case inr
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
[PROOFSTEP]
exact le_sup_of_le_right (Finset.le_sup h)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
[PROOFSTEP]
classical
refine' s.induction _ _
· simp only [Finset.sum_empty, Finset.sup_empty, degrees_zero]
  exact le_rfl
· intro i s his ih
  rw [Finset.sup_insert, Finset.sum_insert his]
  exact le_trans (degrees_add _ _) (sup_le_sup_left ih _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
[PROOFSTEP]
refine' s.induction _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in ∅, f i) ≤ Finset.sup ∅ fun i => degrees (f i)
[PROOFSTEP]
simp only [Finset.sum_empty, Finset.sup_empty, degrees_zero]
[GOAL]
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 ≤ ⊥
[PROOFSTEP]
exact le_rfl
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      (degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)) →
        degrees (∑ i in insert a s, f i) ≤ Finset.sup (insert a s) fun i => degrees (f i)
[PROOFSTEP]
intro i s his ih
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (∑ i in insert i s, f i) ≤ Finset.sup (insert i s) fun i => degrees (f i)
[PROOFSTEP]
rw [Finset.sup_insert, Finset.sum_insert his]
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (f i + ∑ x in s, f x) ≤ degrees (f i) ⊔ Finset.sup s fun i => degrees (f i)
[PROOFSTEP]
exact le_trans (degrees_add _ _) (sup_le_sup_left ih _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
⊢ degrees (p * q) ≤ degrees p + degrees q
[PROOFSTEP]
classical
refine' Finset.sup_le fun b hb => _
have := support_mul p q hb
simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
rw [Finsupp.toMultiset_add]
exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
⊢ degrees (p * q) ≤ degrees p + degrees q
[PROOFSTEP]
refine' Finset.sup_le fun b hb => _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
⊢ ↑toMultiset b ≤ degrees p + degrees q
[PROOFSTEP]
have := support_mul p q hb
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : b ∈ Finset.biUnion (support p) fun a => Finset.biUnion (support q) fun b => {a + b}
⊢ ↑toMultiset b ≤ degrees p + degrees q
[PROOFSTEP]
simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : ∃ a, a ∈ support p ∧ ∃ a_1, a_1 ∈ support q ∧ b = a + a_1
⊢ ↑toMultiset b ≤ degrees p + degrees q
[PROOFSTEP]
rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset (a₁ + a₂) ≤ degrees p + degrees q
[PROOFSTEP]
rw [Finsupp.toMultiset_add]
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset a₁ + ↑toMultiset a₂ ≤ degrees p + degrees q
[PROOFSTEP]
exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
[PROOFSTEP]
classical
refine' s.induction _ _
· simp only [Finset.prod_empty, Finset.sum_empty, degrees_one, le_refl]
· intro i s his ih
  rw [Finset.prod_insert his, Finset.sum_insert his]
  exact le_trans (degrees_mul _ _) (add_le_add_left ih _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
[PROOFSTEP]
refine' s.induction _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∏ i in ∅, f i) ≤ ∑ i in ∅, degrees (f i)
[PROOFSTEP]
simp only [Finset.prod_empty, Finset.sum_empty, degrees_one, le_refl]
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i) →
        degrees (∏ i in insert a s, f i) ≤ ∑ i in insert a s, degrees (f i)
[PROOFSTEP]
intro i s his ih
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (∏ i in insert i s, f i) ≤ ∑ i in insert i s, degrees (f i)
[PROOFSTEP]
rw [Finset.prod_insert his, Finset.sum_insert his]
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (f i * ∏ x in s, f x) ≤ degrees (f i) + ∑ x in s, degrees (f x)
[PROOFSTEP]
exact le_trans (degrees_mul _ _) (add_le_add_left ih _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ degrees (p ^ 0) ≤ 0 • degrees p
[PROOFSTEP]
rw [pow_zero, degrees_one]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ 0 ≤ 0 • degrees p
[PROOFSTEP]
exact Multiset.zero_le _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
n : ℕ
⊢ degrees (p ^ (n + 1)) ≤ (n + 1) • degrees p
[PROOFSTEP]
rw [pow_succ, add_smul, add_comm, one_smul]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
n : ℕ
⊢ degrees (p * p ^ n) ≤ degrees p + n • degrees p
[PROOFSTEP]
exact le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow _ n) _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
i : σ
⊢ i ∈ degrees p ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support
[PROOFSTEP]
classical simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
i : σ
⊢ i ∈ degrees p ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support
[PROOFSTEP]
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)
[PROOFSTEP]
classical
apply Finset.sup_le
intro d hd
rw [Multiset.disjoint_iff_ne] at h
rw [Multiset.le_iff_count]
intro i
rw [degrees, Multiset.count_finset_sup]
simp only [Finsupp.count_toMultiset]
by_cases h0 : d = 0
· simp only [h0, zero_le, Finsupp.zero_apply]
· refine' @Finset.le_sup _ _ _ _ (p + q).support (fun a => a i) d _
  rw [mem_support_iff, coeff_add]
  suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
  rw [← Finsupp.support_eq_empty, ← Ne.def, ← 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
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)
[PROOFSTEP]
apply Finset.sup_le
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → ↑toMultiset b ≤ degrees (p + q)
[PROOFSTEP]
intro d hd
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
[PROOFSTEP]
rw [Multiset.disjoint_iff_ne] at h
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
[PROOFSTEP]
rw [Multiset.le_iff_count]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ∀ (a : σ), Multiset.count a (↑toMultiset d) ≤ Multiset.count a (degrees (p + q))
[PROOFSTEP]
intro i
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Multiset.count i (degrees (p + q))
[PROOFSTEP]
rw [degrees, Multiset.count_finset_sup]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Finset.sup (support (p + q)) fun a => Multiset.count i (↑toMultiset a)
[PROOFSTEP]
simp only [Finsupp.count_toMultiset]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
[PROOFSTEP]
by_cases h0 : d = 0
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
[PROOFSTEP]
simp only [h0, zero_le, Finsupp.zero_apply]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
[PROOFSTEP]
refine' @Finset.le_sup _ _ _ _ (p + q).support (fun a => a i) d _
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ d ∈ support (p + q)
[PROOFSTEP]
rw [mem_support_iff, coeff_add]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d p + coeff d q ≠ 0
[PROOFSTEP]
suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
this : coeff d q = 0
⊢ coeff d p + coeff d q ≠ 0
[PROOFSTEP]
rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d q = 0
[PROOFSTEP]
rw [← Finsupp.support_eq_empty, ← Ne.def, ← Finset.nonempty_iff_ne_empty] at h0
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : Finset.Nonempty d.support
⊢ coeff d q = 0
[PROOFSTEP]
obtain ⟨j, hj⟩ := h0
[GOAL]
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
⊢ coeff d q = 0
[PROOFSTEP]
contrapose! h
[GOAL]
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
[PROOFSTEP]
rw [mem_support_iff] at hd
[GOAL]
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
[PROOFSTEP]
refine' ⟨j, _, j, _, rfl⟩
[GOAL]
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees p
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees q
[PROOFSTEP]
all_goals rw [mem_degrees]; refine' ⟨d, _, hj⟩; assumption
[GOAL]
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees p
[PROOFSTEP]
rw [mem_degrees]
[GOAL]
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d p ≠ 0 ∧ j ∈ d.support
[PROOFSTEP]
refine' ⟨d, _, hj⟩
[GOAL]
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d p ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees q
[PROOFSTEP]
rw [mem_degrees]
[GOAL]
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support
[PROOFSTEP]
refine' ⟨d, _, hj⟩
[GOAL]
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0
[PROOFSTEP]
assumption
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees (p + q) = degrees p ∪ degrees q
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees (p + q) ≤ degrees p ∪ degrees q
[PROOFSTEP]
apply degrees_add
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ∪ degrees q ≤ degrees (p + q)
[PROOFSTEP]
apply Multiset.union_le
[GOAL]
case a.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)
[PROOFSTEP]
apply le_degrees_add h
[GOAL]
case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (p + q)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (q + p)
[PROOFSTEP]
apply le_degrees_add h.symm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ degrees (↑(map f) p) ⊆ degrees p
[PROOFSTEP]
classical
dsimp only [degrees]
apply Multiset.subset_of_le
apply Finset.sup_mono
apply MvPolynomial.support_map_subset
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ degrees (↑(map f) p) ⊆ degrees p
[PROOFSTEP]
dsimp only [degrees]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ⊆ Finset.sup (support p) fun s => ↑toMultiset s
[PROOFSTEP]
apply Multiset.subset_of_le
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ (Finset.sup (support (↑(map f) p)) fun s => ↑toMultiset s) ≤ Finset.sup (support p) fun s => ↑toMultiset s
[PROOFSTEP]
apply Finset.sup_mono
[GOAL]
case a.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ support (↑(map f) p) ⊆ support p
[PROOFSTEP]
apply MvPolynomial.support_map_subset
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
⊢ degrees (↑(rename f) φ) ⊆ Multiset.map f (degrees φ)
[PROOFSTEP]
classical
intro i
rw [mem_degrees, Multiset.mem_map]
rintro ⟨d, hd, hi⟩
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
rw [sum_apply, Finsupp.sum] at hi
contrapose! hi
rw [Finset.sum_eq_zero]
intro j hj
simp only [exists_prop, mem_degrees] at hi
specialize hi j ⟨x, hx, hj⟩
rw [Finsupp.single_apply, if_neg hi]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
⊢ degrees (↑(rename f) φ) ⊆ Multiset.map f (degrees φ)
[PROOFSTEP]
intro i
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ i ∈ degrees (↑(rename f) φ) → i ∈ Multiset.map f (degrees φ)
[PROOFSTEP]
rw [mem_degrees, Multiset.mem_map]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d (↑(rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
rintro ⟨d, hd, hi⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d (↑(rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ↑(sum x fun a => Finsupp.single (f a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
rw [sum_apply, Finsupp.sum] at hi
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∑ a in x.support, ↑(Finsupp.single (f a) (↑x a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
contrapose! hi
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∑ x_1 in x.support, ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
[PROOFSTEP]
rw [Finset.sum_eq_zero]
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∀ (x_1 : σ), x_1 ∈ x.support → ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
j : σ
hj : j ∈ x.support
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
[PROOFSTEP]
simp only [exists_prop, mem_degrees] at hi
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
[PROOFSTEP]
specialize hi j ⟨x, hx, hj⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
[PROOFSTEP]
rw [Finsupp.single_apply, if_neg hi]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
hf : Injective ↑f
⊢ degrees (↑(map f) p) = degrees p
[PROOFSTEP]
simp only [degrees, MvPolynomial.support_map_of_injective _ hf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees (↑(rename f) p) = Multiset.map f (degrees p)
[PROOFSTEP]
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
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees (↑(rename f) p) = Multiset.map f (degrees p)
[PROOFSTEP]
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h, support_rename_of_injective h,
  Finset.sup_image]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ Finset.sup (support p) ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) =
    Finset.sup (support p) (Multiset.map f ∘ ↑toMultiset)
[PROOFSTEP]
refine' Finset.sup_congr rfl fun x _ => _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
x✝ : x ∈ support p
⊢ ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) x = (Multiset.map f ∘ ↑toMultiset) x
[PROOFSTEP]
exact (Finsupp.toMultiset_map _ _).symm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ vars p = Multiset.toFinset (degrees p)
[PROOFSTEP]
rw [vars]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ Multiset.toFinset (degrees p) = Multiset.toFinset (degrees p)
[PROOFSTEP]
convert rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ vars 0 = ∅
[PROOFSTEP]
classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ vars 0 = ∅
[PROOFSTEP]
rw [vars_def, degrees_zero, Multiset.toFinset_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : r ≠ 0
⊢ vars (↑(monomial s) r) = s.support
[PROOFSTEP]
classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : r ≠ 0
⊢ vars (↑(monomial s) r) = s.support
[PROOFSTEP]
rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ vars (↑C r) = ∅
[PROOFSTEP]
classical rw [vars_def, degrees_C, Multiset.toFinset_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ vars (↑C r) = ∅
[PROOFSTEP]
rw [vars_def, degrees_C, Multiset.toFinset_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Nontrivial R
⊢ vars (X n) = {n}
[PROOFSTEP]
rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single_ne_zero _ (one_ne_zero' ℕ)]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ i ∈ vars p ↔ ∃ d x, i ∈ d.support
[PROOFSTEP]
classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ i ∈ vars p ↔ ∃ d x, i ∈ d.support
[PROOFSTEP]
simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h : ¬v ∈ vars f
⊢ ↑x v = 0
[PROOFSTEP]
classical
rw [vars_def, Multiset.mem_toFinset] at h
rw [← Finsupp.not_mem_support_iff]
contrapose! h
rw [degrees_def]
rw [show f.support = insert x f.support from Eq.symm <| Finset.insert_eq_of_mem H]
rw [Finset.sup_insert]
simp only [Multiset.mem_union, Multiset.sup_eq_union]
left
rwa [← toFinset_toMultiset, Multiset.mem_toFinset] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h : ¬v ∈ vars f
⊢ ↑x v = 0
[PROOFSTEP]
rw [vars_def, Multiset.mem_toFinset] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ↑x v = 0
[PROOFSTEP]
rw [← Finsupp.not_mem_support_iff]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ¬v ∈ x.support
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ degrees f
[PROOFSTEP]
rw [degrees_def]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
[PROOFSTEP]
rw [show f.support = insert x f.support from Eq.symm <| Finset.insert_eq_of_mem H]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (insert x (support f)) fun s => ↑toMultiset s
[PROOFSTEP]
rw [Finset.sup_insert]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ⊔ Finset.sup (support f) fun s => ↑toMultiset s
[PROOFSTEP]
simp only [Multiset.mem_union, Multiset.sup_eq_union]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ∨ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
[PROOFSTEP]
left
[GOAL]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x
[PROOFSTEP]
rwa [← toFinset_toMultiset, Multiset.mem_toFinset] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ vars (p + q) ⊆ vars p ∪ vars q
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ vars (p + q)
⊢ x ∈ vars p ∪ vars q
[PROOFSTEP]
simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ degrees (p + q)
⊢ x ∈ degrees p ∨ x ∈ degrees q
[PROOFSTEP]
simpa using Multiset.mem_of_le (degrees_add _ _) hx
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
⊢ vars (p + q) = vars p ∪ vars q
[PROOFSTEP]
apply Finset.Subset.antisymm (vars_add_subset p q)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
⊢ vars p ∪ vars q ⊆ vars (p + q)
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
x : σ
hx : x ∈ vars p ∪ vars q
⊢ x ∈ vars (p + q)
[PROOFSTEP]
simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees (p + q))
[PROOFSTEP]
rw [degrees_add_of_disjoint h, Multiset.toFinset_union]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
[PROOFSTEP]
exact hx
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ vars (φ * ψ) ⊆ vars φ ∪ vars ψ
[PROOFSTEP]
intro i
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
⊢ i ∈ vars (φ * ψ) → i ∈ vars φ ∪ vars ψ
[PROOFSTEP]
simp only [mem_vars, Finset.mem_union]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
⊢ (∃ d x, i ∈ d.support) → (∃ d x, i ∈ d.support) ∨ ∃ d x, i ∈ d.support
[PROOFSTEP]
rintro ⟨d, hd, hi⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ support (φ * ψ)
hi : i ∈ d.support
⊢ (∃ d x, i ∈ d.support) ∨ ∃ d x, i ∈ d.support
[PROOFSTEP]
rw [mem_support_iff, coeff_mul] at hd
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd✝ : coeff d (φ * ψ) ≠ 0
hd : ∑ x in antidiagonal d, coeff x.fst φ * coeff x.snd ψ ≠ 0
hi : i ∈ d.support
⊢ (∃ d x, i ∈ d.support) ∨ ∃ d x, i ∈ d.support
[PROOFSTEP]
contrapose! hd
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd✝ : coeff d (φ * ψ) ≠ 0
hi : i ∈ d.support
hd : (∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support) ∧ ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
⊢ ∑ x in antidiagonal d, coeff x.fst φ * coeff x.snd ψ = 0
[PROOFSTEP]
cases hd
[GOAL]
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : coeff d (φ * ψ) ≠ 0
hi : i ∈ d.support
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
⊢ ∑ x in antidiagonal d, coeff x.fst φ * coeff x.snd ψ = 0
[PROOFSTEP]
rw [Finset.sum_eq_zero]
[GOAL]
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : coeff d (φ * ψ) ≠ 0
hi : i ∈ d.support
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), x ∈ antidiagonal d → coeff x.fst φ * coeff x.snd ψ = 0
[PROOFSTEP]
rintro ⟨d₁, d₂⟩ H
[GOAL]
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : coeff d (φ * ψ) ≠ 0
hi : i ∈ d.support
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
H : (d₁, d₂) ∈ antidiagonal d
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
rw [Finsupp.mem_antidiagonal] at H
[GOAL]
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : coeff d (φ * ψ) ≠ 0
hi : i ∈ d.support
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
H : (d₁, d₂).fst + (d₁, d₂).snd = d
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
subst H
[GOAL]
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
obtain H | H : i ∈ d₁.support ∨ i ∈ d₂.support := by simpa only [Finset.mem_union] using Finsupp.support_add hi
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
⊢ i ∈ d₁.support ∨ i ∈ d₂.support
[PROOFSTEP]
simpa only [Finset.mem_union] using Finsupp.support_add hi
[GOAL]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
suffices coeff d₁ φ = 0 by simp [this]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
this : coeff d₁ φ = 0
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
simp [this]
[GOAL]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff d₁ φ = 0
[PROOFSTEP]
rw [coeff, ← Finsupp.not_mem_support_iff]
[GOAL]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ ¬d₁ ∈ φ.support
[PROOFSTEP]
intro
[GOAL]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
a✝ : d₁ ∈ φ.support
⊢ False
[PROOFSTEP]
solve_by_elim
[GOAL]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
suffices coeff d₂ ψ = 0 by simp [this]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
this : coeff d₂ ψ = 0
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
[PROOFSTEP]
simp [this]
[GOAL]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff d₂ ψ = 0
[PROOFSTEP]
rw [coeff, ← Finsupp.not_mem_support_iff]
[GOAL]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ ¬d₂ ∈ ψ.support
[PROOFSTEP]
intro
[GOAL]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
left✝ : ∀ (d : σ →₀ ℕ), d ∈ support φ → ¬i ∈ d.support
right✝ : ∀ (d : σ →₀ ℕ), d ∈ support ψ → ¬i ∈ d.support
d₁ d₂ : σ →₀ ℕ
hd : coeff ((d₁, d₂).fst + (d₁, d₂).snd) (φ * ψ) ≠ 0
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
a✝ : d₂ ∈ ψ.support
⊢ False
[PROOFSTEP]
solve_by_elim
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
⊢ vars (φ ^ n) ⊆ vars φ
[PROOFSTEP]
classical
induction' n with n ih
· simp
· rw [pow_succ]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset (Finset.Subset.refl _) ih
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
⊢ vars (φ ^ n) ⊆ vars φ
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
⊢ vars (φ ^ Nat.zero) ⊆ vars φ
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ ^ Nat.succ n) ⊆ vars φ
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars (φ * φ ^ n) ⊆ vars φ
[PROOFSTEP]
apply Finset.Subset.trans (vars_mul _ _)
[GOAL]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q φ : MvPolynomial σ R
n : ℕ
ih : vars (φ ^ n) ⊆ vars φ
⊢ vars φ ∪ vars (φ ^ n) ⊆ vars φ
[PROOFSTEP]
exact Finset.union_subset (Finset.Subset.refl _) ih
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ vars (∏ i in s, f i) ⊆ Finset.biUnion s fun i => vars (f i)
[PROOFSTEP]
classical induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ vars (∏ i in s, f i) ⊆ Finset.biUnion s fun i => vars (f i)
[PROOFSTEP]
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ vars (∏ i in s, f i) ⊆ Finset.biUnion s fun i => vars (f i)
[PROOFSTEP]
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
⊢ vars (∏ i in ∅, f i) ⊆ Finset.biUnion ∅ fun i => vars (f i)
[PROOFSTEP]

| empty => simp
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
⊢ vars (∏ i in ∅, f i) ⊆ Finset.biUnion ∅ fun i => vars (f i)
[PROOFSTEP]
simp
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (∏ i in insert a✝ s✝, f i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (f i)
[PROOFSTEP]

| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (∏ i in insert a✝ s✝, f i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (f i)
[PROOFSTEP]
simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝ * ∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
[PROOFSTEP]
apply Finset.Subset.trans (vars_mul _ _)
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝) ∪ vars (∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
[PROOFSTEP]
exact Finset.union_subset_union (Finset.Subset.refl _) hsub
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ vars (↑C a * φ) = vars φ
[PROOFSTEP]
ext1 i
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ vars (↑C a * φ) ↔ i ∈ vars φ
[PROOFSTEP]
simp only [mem_vars, exists_prop, mem_support_iff]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support
[PROOFSTEP]
apply exists_congr
[GOAL]
case a.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (↑C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
[PROOFSTEP]
intro d
[GOAL]
case a.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
[PROOFSTEP]
apply and_congr _ Iff.rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : IsDomain A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (↑C a * φ) ≠ 0 ↔ coeff d φ ≠ 0
[PROOFSTEP]
rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and_iff]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in t, φ i) ⊆ Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
classical induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine' Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in t, φ i) ⊆ Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine' Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in t, φ i) ⊆ Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine' Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in ∅, φ i) ⊆ Finset.biUnion ∅ fun i => vars (φ i)
[PROOFSTEP]

| empty => simp
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in ∅, φ i) ⊆ Finset.biUnion ∅ fun i => vars (φ i)
[PROOFSTEP]
simp
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
[PROOFSTEP]

| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine' Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
[PROOFSTEP]
rw [Finset.biUnion_insert, Finset.sum_insert has]
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (φ a✝ + ∑ x in s✝, φ x) ⊆ vars (φ a✝) ∪ Finset.biUnion s✝ fun i => vars (φ i)
[PROOFSTEP]
refine' Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ x in s✝, φ x) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
[PROOFSTEP]
assumption
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in t, φ i) = Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
classical induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h ⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in t, φ i) = Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h ⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in t, φ i) = Finset.biUnion t fun i => vars (φ i)
[PROOFSTEP]
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h ⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in ∅, φ i) = Finset.biUnion ∅ fun i => vars (φ i)
[PROOFSTEP]

| empty => simp
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in ∅, φ i) = Finset.biUnion ∅ fun i => vars (φ i)
[PROOFSTEP]
simp
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) = Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
[PROOFSTEP]

| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h ⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) = Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
[PROOFSTEP]
rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
[PROOFSTEP]
unfold Pairwise onFun at h
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
[PROOFSTEP]
rw [hsum]
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (Finset.biUnion s✝ fun i => vars (φ i))
[PROOFSTEP]
simp only [Finset.disjoint_iff_ne] at h ⊢
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
⊢ ∀ (a : σ), a ∈ vars (φ a✝) → ∀ (b : σ), (b ∈ Finset.biUnion s✝ fun i => vars (φ i)) → a ≠ b
[PROOFSTEP]
intro v hv v2 hv2
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : v2 ∈ Finset.biUnion s✝ fun i => vars (φ i)
⊢ v ≠ v2
[PROOFSTEP]
rw [Finset.mem_biUnion] at hv2
[GOAL]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : ∃ a, a ∈ s✝ ∧ v2 ∈ vars (φ a)
⊢ v ≠ v2
[PROOFSTEP]
rcases hv2 with ⟨i, his, hi⟩
[GOAL]
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ v ≠ v2
[PROOFSTEP]
refine' h _ _ hv _ hi
[GOAL]
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ a✝ ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
his : a✝ ∈ s✝
hi : v2 ∈ vars (φ a✝)
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ vars (↑(map f) p) ⊆ vars p
[PROOFSTEP]
classical simp [vars_def, degrees_map]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ vars (↑(map f) p) ⊆ vars p
[PROOFSTEP]
simp [vars_def, degrees_map]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
hf : Injective ↑f
⊢ vars (↑(map f) p) = vars p
[PROOFSTEP]
simp [vars, degrees_map_of_injective _ hf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r✝ : R
e✝ : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ vars (↑(monomial (Finsupp.single i e)) r) = {i}
[PROOFSTEP]
rw [vars_monomial hr, Finsupp.support_single_ne_zero _ he]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
⊢ vars p = Finset.biUnion (support p) Finsupp.support
[PROOFSTEP]
ext i
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ vars p ↔ i ∈ Finset.biUnion (support p) Finsupp.support
[PROOFSTEP]
rw [mem_vars, Finset.mem_biUnion]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
f : R →+* S
inst✝ : DecidableEq σ
i : σ
⊢ (∃ d x, i ∈ d.support) ↔ ∃ a, a ∈ support p ∧ i ∈ a.support
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ degreeOf n p = Multiset.count n (degrees p)
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n (degrees p) = Multiset.count n (degrees p)
[PROOFSTEP]
convert rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = Finset.sup (support f) fun m => ↑m n
[PROOFSTEP]
classical
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
congr
ext
simp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = Finset.sup (support f) fun m => ↑m n
[PROOFSTEP]
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (Finset.sup (support f) fun a => Multiset.count n (↑toMultiset a)) = Finset.sup (support f) fun m => ↑m n
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (fun a => Multiset.count n (↑toMultiset a)) = fun m => ↑m n
[PROOFSTEP]
ext
[GOAL]
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (↑toMultiset x✝) = ↑x✝ n
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ (m : σ →₀ ℕ), m ∈ support f → ↑m n < d
[PROOFSTEP]
rwa [degreeOf_eq_sup n f, Finset.sup_lt_iff]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
⊢ degreeOf n 0 = 0
[PROOFSTEP]
classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
⊢ degreeOf n 0 = 0
[PROOFSTEP]
simp only [degreeOf_def, degrees_zero, Multiset.count_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
x : σ
⊢ degreeOf x (↑C a) = 0
[PROOFSTEP]
classical simp [degreeOf_def, degrees_C]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
x : σ
⊢ degreeOf x (↑C a) = 0
[PROOFSTEP]
simp [degreeOf_def, degrees_C]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0
[PROOFSTEP]
classical
by_cases c : i = j
· simp only [c, if_true, eq_self_iff_true, degreeOf_def, degrees_X, Multiset.count_singleton]
simp [c, if_false, degreeOf_def, degrees_X]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0
[PROOFSTEP]
by_cases c : i = j
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
[PROOFSTEP]
simp only [c, if_true, eq_self_iff_true, degreeOf_def, degrees_X, Multiset.count_singleton]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
[PROOFSTEP]
simp [c, if_false, degreeOf_def, degrees_X]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
[PROOFSTEP]
letI := Classical.decEq σ
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
[PROOFSTEP]
repeat' rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (degreeOf n f) (degreeOf n g)
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (degreeOf n g)
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees (f + g)) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
[PROOFSTEP]
apply (Multiset.count_le_of_le n (degrees_add f g)).trans
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ⊔ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f g : MvPolynomial σ R
this : DecidableEq σ := Classical.decEq σ
⊢ Multiset.count n (degrees f ∪ degrees g) ≤ max (Multiset.count n (degrees f)) (Multiset.count n (degrees g))
[PROOFSTEP]
rw [Multiset.count_union]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ support f
⊢ ↑m i ≤ degreeOf i f
[PROOFSTEP]
rw [degreeOf_eq_sup i]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ support f
⊢ ↑m i ≤ Finset.sup (support f) fun m => ↑m i
[PROOFSTEP]
apply Finset.le_sup h_m
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
[PROOFSTEP]
classical
repeat' rw [degreeOf]
convert Multiset.count_le_of_le i (degrees_mul f g)
rw [Multiset.count_add]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
[PROOFSTEP]
repeat' rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ degreeOf i f + degreeOf i g
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + degreeOf i g
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees (f * g)) ≤ Multiset.count i (degrees f) + Multiset.count i (degrees g)
[PROOFSTEP]
convert Multiset.count_le_of_le i (degrees_mul f g)
[GOAL]
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (degrees f) + Multiset.count i (degrees g) = Multiset.count i (degrees f + degrees g)
[PROOFSTEP]
rw [Multiset.count_add]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
[PROOFSTEP]
classical
repeat' rw [degreeOf_eq_sup (R := R) i]
rw [support_mul_X]
simp only [Finset.sup_map]
congr
ext
simp only [Finsupp.single, Nat.one_ne_zero, add_right_eq_self, addRightEmbedding_apply, coe_mk, Pi.add_apply,
  comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
[PROOFSTEP]
repeat' rw [degreeOf_eq_sup (R := R) i]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
[PROOFSTEP]
rw [degreeOf_eq_sup (R := R) i]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = degreeOf i f
[PROOFSTEP]
rw [degreeOf_eq_sup (R := R) i]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
[PROOFSTEP]
rw [degreeOf_eq_sup (R := R) i]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (support (f * X j)) fun m => ↑m i) = Finset.sup (support f) fun m => ↑m i
[PROOFSTEP]
rw [support_mul_X]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (Finset.sup (Finset.map (addRightEmbedding (Finsupp.single j 1)) (support f)) fun m => ↑m i) =
    Finset.sup (support f) fun m => ↑m i
[PROOFSTEP]
simp only [Finset.sup_map]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ Finset.sup (support f) ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) =
    Finset.sup (support f) fun m => ↑m i
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1)) = fun m => ↑m i
[PROOFSTEP]
ext
[GOAL]
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m => ↑m i) ∘ ↑(addRightEmbedding (Finsupp.single j 1))) x✝ = ↑x✝ i
[PROOFSTEP]
simp only [Finsupp.single, Nat.one_ne_zero, add_right_eq_self, addRightEmbedding_apply, coe_mk, Pi.add_apply,
  comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
[PROOFSTEP]
classical
repeat' rw [degreeOf]
apply (Multiset.count_le_of_le j (degrees_mul f (X j))).trans
simp only [Multiset.count_add, add_le_add_iff_left]
convert Multiset.count_le_of_le j (degrees_X' (R := R) j)
rw [Multiset.count_singleton_self]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
[PROOFSTEP]
repeat' rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ degreeOf j f + 1
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
[PROOFSTEP]
rw [degreeOf]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
[PROOFSTEP]
apply (Multiset.count_le_of_le j (degrees_mul f (X j))).trans
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees f + degrees (X j)) ≤ Multiset.count j (degrees f) + 1
[PROOFSTEP]
simp only [Multiset.count_add, add_le_add_iff_left]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (X j)) ≤ 1
[PROOFSTEP]
convert Multiset.count_le_of_le j (degrees_X' (R := R) j)
[GOAL]
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}
[PROOFSTEP]
rw [Multiset.count_singleton_self]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) (↑(rename f) p) = degreeOf i p
[PROOFSTEP]
classical simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) (↑(rename f) p) = degreeOf i p
[PROOFSTEP]
simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p = Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
rw [totalDegree]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => sum s fun x e => e) = Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (fun s => sum s fun x e => e) = fun m => ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
funext m
[GOAL]
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (sum m fun x e => e) = ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
exact (Finsupp.card_toMultiset _).symm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p ≤ ↑Multiset.card (degrees p)
[PROOFSTEP]
classical
rw [totalDegree_eq]
exact Finset.sup_le fun s hs => Multiset.card_le_of_le <| Finset.le_sup hs
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p ≤ ↑Multiset.card (degrees p)
[PROOFSTEP]
rw [totalDegree_eq]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) ≤ ↑Multiset.card (degrees p)
[PROOFSTEP]
exact Finset.sup_le fun s hs => Multiset.card_le_of_le <| Finset.le_sup hs
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
⊢ (sum n fun x e => e) ≤ 0
[PROOFSTEP]
have := Finsupp.support_single_subset hn
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n ∈ {0}
⊢ (sum n fun x e => e) ≤ 0
[PROOFSTEP]
rw [Finset.mem_singleton] at this
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n = 0
⊢ (sum n fun x e => e) ≤ 0
[PROOFSTEP]
subst this
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
hn : 0 ∈ support (↑C a)
⊢ (sum 0 fun x e => e) ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ totalDegree 0 = 0
[PROOFSTEP]
rw [← C_0]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ totalDegree (↑C 0) = 0
[PROOFSTEP]
exact totalDegree_C (0 : R)
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R✝
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝² : CommSemiring R✝
p q : MvPolynomial σ R✝
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ totalDegree (X s) = 1
[PROOFSTEP]
rw [totalDegree, support_X]
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R✝
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝² : CommSemiring R✝
p q : MvPolynomial σ R✝
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (Finset.sup {Finsupp.single s 1} fun s => sum s fun x e => e) = 1
[PROOFSTEP]
simp only [Finset.sup, Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) = totalDegree p
[PROOFSTEP]
classical
apply le_antisymm
· rw [← max_eq_left_of_lt h]
  exact totalDegree_add p q
by_cases hp : p = 0
· simp [hp]
obtain ⟨b, hb₁, hb₂⟩ :=
  p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ => Multiset.card (toMultiset m)
have hb : ¬b ∈ q.support := by
  contrapose! h
  rw [totalDegree_eq p, hb₂, totalDegree_eq]
  apply Finset.le_sup h
have hbb : b ∈ (p + q).support := by
  apply support_sdiff_support_subset_support_add
  rw [Finset.mem_sdiff]
  exact ⟨hb₁, hb⟩
rw [totalDegree_eq, hb₂, totalDegree_eq]
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) = totalDegree p
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ totalDegree p
[PROOFSTEP]
rw [← max_eq_left_of_lt h]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ max (totalDegree p) (totalDegree q)
[PROOFSTEP]
exact totalDegree_add p q
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : p = 0
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
obtain ⟨b, hb₁, hb₂⟩ :=
  p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ => Multiset.card (toMultiset m)
[GOAL]
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
have hb : ¬b ∈ q.support := by
  contrapose! h
  rw [totalDegree_eq p, hb₂, totalDegree_eq]
  apply Finset.le_sup h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
⊢ ¬b ∈ support q
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ totalDegree p ≤ totalDegree q
[PROOFSTEP]
rw [totalDegree_eq p, hb₂, totalDegree_eq]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support q) fun m => ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
apply Finset.le_sup h
[GOAL]
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
have hbb : b ∈ (p + q).support := by
  apply support_sdiff_support_subset_support_add
  rw [Finset.mem_sdiff]
  exact ⟨hb₁, hb⟩
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support (p + q)
[PROOFSTEP]
apply support_sdiff_support_subset_support_add
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p \ support q
[PROOFSTEP]
rw [Finset.mem_sdiff]
[GOAL]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p ∧ ¬b ∈ support q
[PROOFSTEP]
exact ⟨hb₁, hb⟩
[GOAL]
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ totalDegree p ≤ totalDegree (p + q)
[PROOFSTEP]
rw [totalDegree_eq, hb₂, totalDegree_eq]
[GOAL]
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support (p + q)) fun m => ↑Multiset.card (↑toMultiset m)
[PROOFSTEP]
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (q + p) = totalDegree p
[PROOFSTEP]
rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
⊢ ∀ {a b : σ →₀ ℕ}, (sum (a + b) fun x e => e) ≤ (sum a fun x e => e) + sum b fun x e => e
[PROOFSTEP]
exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
⊢ totalDegree (a ^ n) ≤ n * totalDegree a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
⊢ totalDegree (a ^ Nat.zero) ≤ Nat.zero * totalDegree a
[PROOFSTEP]
simp only [Nat.zero_eq, zero_mul, pow_zero, totalDegree_one]
[GOAL]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a ^ Nat.succ n) ≤ Nat.succ n * totalDegree a
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a * a ^ n) ≤ Nat.succ n * totalDegree a
[PROOFSTEP]
calc
  totalDegree (a * a ^ n) ≤ a.totalDegree + (a ^ n).totalDegree := totalDegree_mul _ _
  _ ≤ a.totalDegree + n * a.totalDegree := (add_le_add_left ih _)
  _ = (n + 1) * a.totalDegree := by rw [add_mul, one_mul, add_comm]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree a + n * totalDegree a = (n + 1) * totalDegree a
[PROOFSTEP]
rw [add_mul, one_mul, add_comm]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree (↑(monomial s) c) = sum s fun x e => e
[PROOFSTEP]
classical simp [totalDegree, support_monomial, if_neg hc]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree (↑(monomial s) c) = sum s fun x e => e
[PROOFSTEP]
simp [totalDegree, support_monomial, if_neg hc]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ totalDegree (X s ^ n) = n
[PROOFSTEP]
simp [X_pow_eq_monomial, one_ne_zero]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ totalDegree (List.prod []) ≤ List.sum (List.map totalDegree [])
[PROOFSTEP]
rw [@List.prod_nil (MvPolynomial σ R) _, totalDegree_one]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ 0 ≤ List.sum (List.map totalDegree [])
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ totalDegree (List.prod (p :: ps)) ≤ List.sum (List.map totalDegree (p :: ps))
[PROOFSTEP]
rw [@List.prod_cons (MvPolynomial σ R) _, List.map, List.sum_cons]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ totalDegree (p * List.prod ps) ≤ totalDegree p + List.sum (List.map totalDegree ps)
[PROOFSTEP]
exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
⊢ totalDegree (Multiset.prod s) ≤ Multiset.sum (Multiset.map totalDegree s)
[PROOFSTEP]
refine' Quotient.inductionOn s fun l => _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (Multiset.prod (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l)) ≤
    Multiset.sum (Multiset.map totalDegree (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l))
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map, Multiset.coe_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (List.prod l) ≤ List.sum (List.map totalDegree l)
[PROOFSTEP]
exact totalDegree_list_prod l
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ totalDegree (Finset.prod s f) ≤ ∑ i in s, totalDegree (f i)
[PROOFSTEP]
refine' le_trans (totalDegree_multiset_prod _) _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map totalDegree (Multiset.map f s.val)) ≤ ∑ i in s, totalDegree (f i)
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map (totalDegree ∘ f) s.val) ≤ ∑ i in s, totalDegree (f i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ totalDegree (Finset.sum s f) ≤ Finset.sup s fun i => totalDegree (f i)
[PROOFSTEP]
induction' s using Finset.cons_induction with a s has hind
[GOAL]
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ totalDegree (Finset.sum ∅ f) ≤ Finset.sup ∅ fun i => totalDegree (f i)
[PROOFSTEP]
exact zero_le _
[GOAL]
case cons
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : ¬a ∈ s
hind : totalDegree (Finset.sum s f) ≤ Finset.sup s fun i => totalDegree (f i)
⊢ totalDegree (Finset.sum (Finset.cons a s has) f) ≤ Finset.sup (Finset.cons a s has) fun i => totalDegree (f i)
[PROOFSTEP]
rw [Finset.sum_cons, Finset.sup_cons, sup_eq_max]
[GOAL]
case cons
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : ¬a ∈ s
hind : totalDegree (Finset.sum s f) ≤ Finset.sup s fun i => totalDegree (f i)
⊢ totalDegree (f a + ∑ x in s, f x) ≤ max (totalDegree (f a)) (Finset.sup s fun i => totalDegree (f i))
[PROOFSTEP]
exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : totalDegree f < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ support f
⊢ ∃ i, ↑d i < n
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ n * Fintype.card σ ≤ totalDegree f
[PROOFSTEP]
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
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ n * Fintype.card σ = ∑ _s : σ, n
[PROOFSTEP]
rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ ∑ s : σ, ↑d s ≤ sum d fun x e => e
[PROOFSTEP]
rw [Finsupp.sum_fintype]
[GOAL]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ σ → 0 = 0
[PROOFSTEP]
intros
[GOAL]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
i✝ : σ
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : totalDegree f < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
[PROOFSTEP]
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
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : totalDegree f < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
[PROOFSTEP]
rw [totalDegree, Finset.sup_lt_iff] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ (b : σ →₀ ℕ), b ∈ support f → (sum b fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
[PROOFSTEP]
specialize h d
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ support f → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
[PROOFSTEP]
rw [mem_support_iff] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
[PROOFSTEP]
refine' not_not.mp (mt h _)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ ¬(sum d fun x e => e) < ∑ i in d.support, ↑d i
[PROOFSTEP]
exact lt_irrefl _
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : (Finset.sup (support f) fun s => sum s fun x e => e) < ∑ i in d.support, ↑d i
⊢ ⊥ < ∑ i in d.support, ↑d i
[PROOFSTEP]
exact lt_of_le_of_lt (Nat.zero_le _) h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ support (↑(rename f) p) → (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
classical
intro h
rw [rename_eq] at h
have h' := Finsupp.mapDomain_support h
rw [Finset.mem_image] at h'
rcases h' with ⟨s, hs, rfl⟩
rw [Finsupp.sum_mapDomain_index]
exact le_trans le_rfl (le_totalDegree hs)
exact fun _ => rfl
exact fun _ _ _ => rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
⊢ b ∈ support (↑(rename f) p) → (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (↑(rename f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
rw [rename_eq] at h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
have h' := Finsupp.mapDomain_support h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support
⊢ (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
rw [Finset.mem_image] at h'
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
h' : ∃ a, a ∈ p.support ∧ Finsupp.mapDomain f a = b
⊢ (sum b fun x e => e) ≤ totalDegree p
[PROOFSTEP]
rcases h' with ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum (Finsupp.mapDomain f s) fun x e => e) ≤ totalDegree p
[PROOFSTEP]
rw [Finsupp.sum_mapDomain_index]
[GOAL]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ (sum s fun a m => m) ≤ totalDegree p
case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0
case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
[PROOFSTEP]
exact le_trans le_rfl (le_totalDegree hs)
[GOAL]
case intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → 0 = 0
case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
[PROOFSTEP]
exact fun _ => rfl
[GOAL]
case intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)
⊢ τ → ∀ (m₁ m₂ : ℕ), m₁ + m₂ = m₁ + m₂
[PROOFSTEP]
exact fun _ _ _ => rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ ↑(eval₂Hom f g) p = ↑f (↑constantCoeff p)
[PROOFSTEP]
conv_lhs => rw [p.as_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
| ↑(eval₂Hom f g) p
[PROOFSTEP]
rw [p.as_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
| ↑(eval₂Hom f g) p
[PROOFSTEP]
rw [p.as_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
| ↑(eval₂Hom f g) p
[PROOFSTEP]
rw [p.as_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ ↑(eval₂Hom f g) (∑ v in support p, ↑(monomial v) (coeff v p)) = ↑f (↑constantCoeff p)
[PROOFSTEP]
simp only [map_sum, eval₂Hom_monomial]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
by_cases h0 : constantCoeff p = 0
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
on_goal 1 =>
  rw [h0, f.map_zero, Finset.sum_eq_zero]
  intro d hd
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
on_goal 1 =>
  rw [h0, f.map_zero, Finset.sum_eq_zero]
  intro d hd
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
rw [h0, f.map_zero, Finset.sum_eq_zero]
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ ∀ (x : σ →₀ ℕ), x ∈ support p → (↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = 0
[PROOFSTEP]
intro d hd
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
on_goal 2 =>
  rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
  · rw [Finsupp.prod_zero_index, mul_one]
    rfl
  intro d hd hd0
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
on_goal 2 =>
  rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
  · rw [Finsupp.prod_zero_index, mul_one]
    rfl
  intro d hd hd0
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = ↑f (↑constantCoeff p)
[PROOFSTEP]
rw [Finsupp.prod_zero_index, mul_one]
[GOAL]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ↑f (coeff 0 p) = ↑f (↑constantCoeff p)
[PROOFSTEP]
rfl
[GOAL]
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → b ≠ 0 → (↑f (coeff b p) * Finsupp.prod b fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
intro d hd hd0
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
on_goal 3 =>
  rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
  intro
  contradiction
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
on_goal 3 =>
  rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
  intro
  contradiction
[GOAL]
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
[GOAL]
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
intro
[GOAL]
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
a✝ : ¬0 ∈ support p
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
[PROOFSTEP]
contradiction
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
[PROOFSTEP]
repeat'
  obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) :=
    by
    rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
    rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
    rintro rfl
    contradiction
  rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
  rw [hp, zero_pow (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)]
  rw [mem_vars]
  exact ⟨d, hd, hi⟩
[GOAL]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
[PROOFSTEP]
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) :=
  by
  rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
  rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
  rintro rfl
  contradiction
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ Finset.Nonempty d.support
[PROOFSTEP]
rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
⊢ Finset.Nonempty d.support
[PROOFSTEP]
rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ¬d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬0 ∈ p.support
hd : 0 ∈ support p
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
hi : i ∈ d.support
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
[PROOFSTEP]
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
[GOAL]
case pos.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
hi : i ∈ d.support
⊢ g i ^ ↑d i = 0
[PROOFSTEP]
rw [hp, zero_pow (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)]
[GOAL]
case pos.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p
[PROOFSTEP]
rw [mem_vars]
[GOAL]
case pos.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
[PROOFSTEP]
exact ⟨d, hd, hi⟩
[GOAL]
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
[PROOFSTEP]
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) :=
  by
  rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
  rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
  rintro rfl
  contradiction
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ Finset.Nonempty d.support
[PROOFSTEP]
rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ Finset.Nonempty d.support
[PROOFSTEP]
rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ ¬d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
hd : 0 ∈ support p
hd0 : 0 ≠ 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
[PROOFSTEP]
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
[GOAL]
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ g i ^ ↑d i = 0
[PROOFSTEP]
rw [hp, zero_pow (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)]
[GOAL]
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p
[PROOFSTEP]
rw [mem_vars]
[GOAL]
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
[PROOFSTEP]
exact ⟨d, hd, hi⟩
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : R →+* S
g₁ g₂ : σ → S
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → (∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → g₁ i = g₂ i) → p₁ = p₂ → ↑(eval₂Hom f₁ g₁) p₁ = ↑(eval₂Hom f₂ g₂) p₂
[PROOFSTEP]
rintro rfl h rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) p₁ = ↑(eval₂Hom f₁ g₂) p₁
[PROOFSTEP]
rw [p₁.as_sum]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) (∑ v in support p₁, ↑(monomial v) (coeff v p₁)) =
    ↑(eval₂Hom f₁ g₂) (∑ v in support p₁, ↑(monomial v) (coeff v p₁))
[PROOFSTEP]
simp only [map_sum, eval₂Hom_monomial]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ (∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) =
    ∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ∀ (x : σ →₀ ℕ),
    x ∈ support p₁ →
      (↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) = ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
[PROOFSTEP]
intro d hd
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₁ i ^ k) = ↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₂ i ^ k
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (Finsupp.prod d fun i k => g₁ i ^ k) = Finsupp.prod d fun i k => g₂ i ^ k
[PROOFSTEP]
simp only [Finsupp.prod]
[GOAL]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∏ x in d.support, g₁ x ^ ↑d x = ∏ x in d.support, g₂ x ^ ↑d x
[PROOFSTEP]
apply Finset.prod_congr rfl
[GOAL]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∀ (x : σ), x ∈ d.support → g₁ x ^ ↑d x = g₂ x ^ ↑d x
[PROOFSTEP]
intro i hi
[GOAL]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
[PROOFSTEP]
have : i ∈ p₁.vars := by
  rw [mem_vars]
  exact ⟨d, hd, hi⟩
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p₁
[PROOFSTEP]
rw [mem_vars]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
[PROOFSTEP]
exact ⟨d, hd, hi⟩
[GOAL]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
this : i ∈ vars p₁
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
[PROOFSTEP]
rw [h i this this]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
⊢ f₁ = eval₂Hom (RingHom.comp f₁ C) (↑f₁ ∘ X)
[PROOFSTEP]
ext
[GOAL]
case hC.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ ↑(RingHom.comp f₁ C) x✝ = ↑(RingHom.comp (eval₂Hom (RingHom.comp f₁ C) (↑f₁ ∘ X)) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ ↑f₁ (X i✝) = ↑(eval₂Hom (RingHom.comp f₁ C) (↑f₁ ∘ X)) (X i✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
⊢ eval₂Hom (RingHom.comp f₂ C) (↑f₂ ∘ X) = f₂
[PROOFSTEP]
ext
[GOAL]
case hC.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ ↑(RingHom.comp (eval₂Hom (RingHom.comp f₂ C) (↑f₂ ∘ X)) C) x✝ = ↑(RingHom.comp f₂ C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : RingHom.comp f₁ C = RingHom.comp f₂ C
hv : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → ↑f₁ (X i) = ↑f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ ↑(eval₂Hom (RingHom.comp f₂ C) (↑f₂ ∘ X)) (X i✝) = ↑f₂ (X i✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ↑(rename f) (↑(aeval fun i => Option.elim' 0 X (partialInv f i)) p) = p
[PROOFSTEP]
show (rename f).toRingHom.comp _ p = RingHom.id _ p
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) p = ↑(RingHom.id (MvPolynomial σ R)) p
[PROOFSTEP]
refine' hom_congr_vars _ _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C =
    RingHom.comp (RingHom.id (MvPolynomial σ R)) C
[PROOFSTEP]
ext1
[GOAL]
case refine'_1.a
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) C) x✝ =
    ↑(RingHom.comp (RingHom.id (MvPolynomial σ R)) C) x✝
[PROOFSTEP]
simp [algebraMap_eq]
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ ∀ (i : σ),
    i ∈ vars p →
      i ∈ vars p →
        ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
          ↑(RingHom.id (MvPolynomial σ R)) (X i)
[PROOFSTEP]
intro i hip _
[GOAL]
case refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : σ
hip a✝ : i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X i) =
    ↑(RingHom.id (MvPolynomial σ R)) (X i)
[PROOFSTEP]
rcases hf hip with ⟨i, rfl⟩
[GOAL]
case refine'_2.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
i : τ
hip a✝ : f i ∈ vars p
⊢ ↑(RingHom.comp ↑(rename f) ↑(aeval fun i => Option.elim' 0 X (partialInv f i))) (X (f i)) =
    ↑(RingHom.id (MvPolynomial σ R)) (X (f i))
[PROOFSTEP]
simp [partialInv_left hfi]
[GOAL]
case refine'_3
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑(vars p) ⊆ range f
⊢ p = p
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ vars (↑(rename f) φ) ⊆ Finset.image f (vars φ)
[PROOFSTEP]
classical
intro i hi
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
simpa only [Multiset.mem_map] using degrees_rename _ _ hi
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ vars (↑(rename f) φ) ⊆ Finset.image f (vars φ)
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ vars (↑(rename f) φ)
⊢ i ∈ Finset.image f (vars φ)
[PROOFSTEP]
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ degrees (↑(rename f) φ)
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
[PROOFSTEP]
simpa only [Multiset.mem_map] using degrees_rename _ _ hi
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(rename f) φ)
⊢ ∃ i, i ∈ vars φ ∧ f i = j
[PROOFSTEP]
classical simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h
[GOAL]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(rename f) φ)
⊢ ∃ i, i ∈ vars φ ∧ f i = j
[PROOFSTEP]
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h