σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
⊢ ∀ (m_1 : MvPolynomial σ R),
    m_1 ∈ homogeneousSubmodule σ R m →
      ∀ (n_1 : MvPolynomial σ R), n_1 ∈ homogeneousSubmodule σ R n → m_1 * n_1 ∈ homogeneousSubmodule σ R (m + n)
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
⊢ homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n)
rw [Submodule.mul_le]
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
⊢ ∀ (m_1 : MvPolynomial σ R),
    m_1 ∈ homogeneousSubmodule σ R m →
      ∀ (n_1 : MvPolynomial σ R), n_1 ∈ homogeneousSubmodule σ R n → m_1 * n_1 ∈ homogeneousSubmodule σ R (m + n)
intro φ hφ ψ hψ c hc
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
rw [coeff_mul] at hc
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
  contrapose! H
  by_cases h : coeff d φ = 0 <;>
    simp_all only [Ne.def, not_false_iff, MulZeroClass.zero_mul, MulZeroClass.mul_zero]
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
specialize hφ aux.1
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
⊢ ∑ i in c.support, ↑c i = m + n
specialize hψ aux.2
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
rw [Finsupp.mem_antidiagonal] at hde
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
⊢ coeff d φ * coeff e ψ = 0
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
contrapose! H
no goals
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
⊢ coeff d φ * coeff e ψ = 0
by_cases h : coeff d φ = 0 <;>
  simp_all only [Ne.def, not_false_iff, MulZeroClass.zero_mul, MulZeroClass.mul_zero]
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
have hd' : d.support ⊆ d.support ∪ e.support := Finset.subset_union_left _ _
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
have he' : e.support ⊆ d.support ∪ e.support := Finset.subset_union_right _ _
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ x in (d, e).fst.support ∪ (d, e).snd.support, ↑((d, e).fst + (d, e).snd) x =
    ∑ x in d.support ∪ e.support, (↑d x + ↑e x)

case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ e.support → ↑e x = 0

case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ d.support → ↑d x = 0

case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ),
    x ∈ (d, e).fst.support ∪ (d, e).snd.support →
      ¬x ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) x = 0
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd',
  Finset.sum_subset he', ← Finset.sum_add_distrib]
no goals
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ e.support → ↑e x = 0

case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ d.support → ↑d x = 0

case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ),
    x ∈ (d, e).fst.support ∪ (d, e).snd.support →
      ¬x ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) x = 0
all_goals intro i hi; apply Finsupp.not_mem_support_iff.mp
no goals
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ x in (d, e).fst.support ∪ (d, e).snd.support, ↑((d, e).fst + (d, e).snd) x =
    ∑ x in d.support ∪ e.support, (↑d x + ↑e x)
congr
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
i : σ
hi : i ∈ (d, e).fst.support ∪ (d, e).snd.support
⊢ ¬i ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) i = 0
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ),
    x ∈ (d, e).fst.support ∪ (d, e).snd.support →
      ¬x ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) x = 0
intro i hi
no goals
case intro.mk.intro
σ : Type u_2
τ : Type ?u.119978
R : Type u_1
S : Type ?u.119984
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
i : σ
hi : i ∈ (d, e).fst.support ∪ (d, e).snd.support
⊢ ¬i ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) i = 0
apply Finsupp.not_mem_support_iff.mp