R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
⊢ i ∈ vars (φ * ψ) → i ∈ vars φ ∪ vars ψ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ vars (φ * ψ) ⊆ vars φ ∪ vars ψ
intro i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
⊢ i ∈ vars (φ * ψ) → i ∈ vars φ ∪ vars ψ
simp only [mem_vars, Finset.mem_union]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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
rintro ⟨d, hd, hi⟩
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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
rw [mem_support_iff, coeff_mul] at hd
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
contrapose! hd
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
cases hd
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
rw [Finset.sum_eq_zero]
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
rintro ⟨d₁, d₂⟩ H
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
rw [Finsupp.mem_antidiagonal] at H
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
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
subst H
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0

case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
case intro.intro.intro.mk
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
obtain H | H : i ∈ d₁.support ∨ i ∈ d₂.support := by
  simpa only [Finset.mem_union] using Finsupp.support_add hi
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
⊢ i ∈ d₁.support ∨ i ∈ d₂.support
simpa only [Finset.mem_union] using Finsupp.support_add hi
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff d₁ φ = 0
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
suffices coeff d₁ φ = 0 by simp [this]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ ¬d₁ ∈ φ.support
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ coeff d₁ φ = 0
rw [coeff, ← Finsupp.not_mem_support_iff]
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
a✝ : d₁ ∈ φ.support
⊢ False
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
⊢ ¬d₁ ∈ φ.support
intro
no goals
case intro.intro.intro.mk.inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₁.support
a✝ : d₁ ∈ φ.support
⊢ False
solve_by_elim
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
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
simp [this]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff d₂ ψ = 0
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff (d₁, d₂).fst φ * coeff (d₁, d₂).snd ψ = 0
suffices coeff d₂ ψ = 0 by simp [this]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ ¬d₂ ∈ ψ.support
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ coeff d₂ ψ = 0
rw [coeff, ← Finsupp.not_mem_support_iff]
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
a✝ : d₂ ∈ ψ.support
⊢ False
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
⊢ ¬d₂ ∈ ψ.support
intro
no goals
case intro.intro.intro.mk.inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
hi : i ∈ ((d₁, d₂).fst + (d₁, d₂).snd).support
H : i ∈ d₂.support
a✝ : d₂ ∈ ψ.support
⊢ False
solve_by_elim
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.160498
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₂ : σ →₀ ℕ
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
simp [this]