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
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p 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
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
refine' (coeff_monomial_mul' _ _ _ _).trans _
no goals
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
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
  one_mul]