case inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
p : MvPolynomial σ R
⊢ coeff m (p * ↑(monomial s) 0) = if s ≤ m then coeff (m - s) p * 0 else 0

case inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
obtain rfl | hr := eq_or_ne r 0
case inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
case inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
haveI : Nontrivial R := nontrivial_of_ne _ _ hr
case inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = coeff (m - s) p * r

case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = 0
case inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
⊢ coeff m (p * ↑(monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
split_ifs with h
no goals
case inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
p : MvPolynomial σ R
⊢ coeff m (p * ↑(monomial s) 0) = if s ≤ m then coeff (m - s) p * 0 else 0
simp only [monomial_zero, coeff_zero, MulZeroClass.mul_zero, ite_self]
case inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = coeff (m - s + s) (p * ↑(monomial s) r)
case inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = coeff (m - s) p * r
conv_rhs => rw [← coeff_mul_monomial _ s]
case inr.inl.e_m.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
t : σ
⊢ ↑m t = ↑(m - s + s) t
case inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = coeff (m - s + s) (p * ↑(monomial s) r)
congr with t
no goals
case inr.inl.e_m.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : s ≤ m
t : σ
⊢ ↑m t = ↑(m - s + s) t
rw [tsub_add_cancel_of_le h]
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
⊢ ¬m ∈ support (p * ↑(monomial s) r)
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
⊢ coeff m (p * ↑(monomial s) r) = 0
rw [← not_mem_support_iff]
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
⊢ False
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
⊢ ¬m ∈ support (p * ↑(monomial s) r)
intro hm
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
⊢ s ≤ m
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
⊢ False
apply h
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
H : m ∈ Finset.biUnion (support p) fun a => Finset.biUnion (support (↑(monomial s) r)) fun b => {a + b}
⊢ s ≤ m
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
⊢ s ≤ m
have H := support_mul _ _ hm
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
H : ∃ a, a ∈ support p ∧ ∃ a_1, a_1 ∈ support (↑(monomial s) r) ∧ m ∈ {a + a_1}
⊢ s ≤ m
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
H : m ∈ Finset.biUnion (support p) fun a => Finset.biUnion (support (↑(monomial s) r)) fun b => {a + b}
⊢ s ≤ m
simp only [Finset.mem_biUnion] at H
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
i' : σ →₀ ℕ
hi' : i' ∈ support (↑(monomial s) r)
H : m ∈ {j + i'}
⊢ s ≤ m
case inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
H : ∃ a, a ∈ support p ∧ ∃ a_1, a_1 ∈ support (↑(monomial s) r) ∧ m ∈ {a + a_1}
⊢ s ≤ m
rcases H with ⟨j, _hj, i', hi', H⟩
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
i' : σ →₀ ℕ
hi'✝ : i' ∈ support (↑(monomial s) r)
hi' : i' = s
H : m ∈ {j + i'}
⊢ s ≤ m
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
i' : σ →₀ ℕ
hi' : i' ∈ support (↑(monomial s) r)
H : m ∈ {j + i'}
⊢ s ≤ m
rw [support_monomial, if_neg hr, Finset.mem_singleton] at hi'
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
H : m ∈ {j + s}
⊢ s ≤ m
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
i' : σ →₀ ℕ
hi'✝ : i' ∈ support (↑(monomial s) r)
hi' : i' = s
H : m ∈ {j + i'}
⊢ s ≤ m
subst i'
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
H : m = j + s
⊢ s ≤ m
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
H : m ∈ {j + s}
⊢ s ≤ m
rw [Finset.mem_singleton] at H
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
h : ¬s ≤ j + s
hm : j + s ∈ support (p * ↑(monomial s) r)
⊢ s ≤ j + s
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
h : ¬s ≤ m
hm : m ∈ support (p * ↑(monomial s) r)
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
H : m = j + s
⊢ s ≤ m
subst m
no goals
case inr.inr.intro.intro.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
hr : r ≠ 0
this : Nontrivial R
j : σ →₀ ℕ
_hj : j ∈ support p
hi' : s ∈ support (↑(monomial s) r)
h : ¬s ≤ j + s
hm : j + s ∈ support (p * ↑(monomial s) r)
⊢ s ≤ j + s
exact le_add_left le_rfl