σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
this :
  ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ antidiagonal m → ↑(coeff R p.fst) φ * ↑(coeff R p.snd) (↑(monomial R n) a) ≠ 0 → p.snd = n
⊢ ↑(coeff R m) (φ * ↑(monomial R n) a) = if n ≤ m then ↑(coeff R (m - n)) φ * a else 0
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
⊢ ↑(coeff R m) (φ * ↑(monomial R n) a) = if n ≤ m then ↑(coeff R (m - n)) φ * a else 0
have :
  ∀ p ∈ antidiagonal m,
    coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n :=
  fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
this :
  ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ antidiagonal m → ↑(coeff R p.fst) φ * ↑(coeff R p.snd) (↑(monomial R n) a) ≠ 0 → p.snd = n
⊢ (if n ≤ m then ∑ x in {(m - n, n)}, ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (↑(monomial R n) a)
    else ∑ x in ∅, ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (↑(monomial R n) a)) =
    if n ≤ m then ↑(coeff R (m - n)) φ * a else 0
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
this :
  ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ antidiagonal m → ↑(coeff R p.fst) φ * ↑(coeff R p.snd) (↑(monomial R n) a) ≠ 0 → p.snd = n
⊢ ↑(coeff R m) (φ * ↑(monomial R n) a) = if n ≤ m then ↑(coeff R (m - n)) φ * a else 0
rw [coeff_mul, ← Finset.sum_filter_of_ne this, antidiagonal_filter_snd_eq, Finset.sum_ite_index]
no goals
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
this :
  ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ antidiagonal m → ↑(coeff R p.fst) φ * ↑(coeff R p.snd) (↑(monomial R n) a) ≠ 0 → p.snd = n
⊢ (if n ≤ m then ∑ x in {(m - n, n)}, ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (↑(monomial R n) a)
    else ∑ x in ∅, ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (↑(monomial R n) a)) =
    if n ≤ m then ↑(coeff R (m - n)) φ * a else 0
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]