R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
⊢ ∀ (m_1 : MvPolynomial σ R),
    m_1 ∈ weightedHomogeneousSubmodule R w m →
      ∀ (n_1 : MvPolynomial σ R),
        n_1 ∈ weightedHomogeneousSubmodule R w n → m_1 * n_1 ∈ weightedHomogeneousSubmodule R w (m + n)
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
⊢ weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤ weightedHomogeneousSubmodule R w (m + n)
rw [Submodule.mul_le]
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
⊢ ∀ (m_1 : MvPolynomial σ R),
    m_1 ∈ weightedHomogeneousSubmodule R w m →
      ∀ (n_1 : MvPolynomial σ R),
        n_1 ∈ weightedHomogeneousSubmodule R w n → m_1 * n_1 ∈ weightedHomogeneousSubmodule R w (m + n)
intro φ hφ ψ hψ c hc
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
rw [coeff_mul] at hc
case intro.mk.intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
case intro.mk.intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
case intro.mk.intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ ↑(weightedDegree' w) c = 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]
no goals
case intro.mk.intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ ↑(weightedDegree' w) c = m + n
rw [← Finsupp.mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
⊢ coeff d φ * coeff e ψ = 0
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
contrapose! H
no goals
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x in antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ 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]