R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
this : ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
⊢ ↑(coeff R n) (φ * ψ) = 0

case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * ψ) = 0
suffices : coeff R n (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
this : ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
⊢ ↑(coeff R n) (φ * ψ) = 0

case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
rw [this, Finset.sum_const_zero]
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ∑ p in Finset.Nat.antidiagonal n, ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = ∑ p in Finset.Nat.antidiagonal n, 0
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, 0
rw [coeff_mul]
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal n → ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ∑ p in Finset.Nat.antidiagonal n, ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = ∑ p in Finset.Nat.antidiagonal n, 0
apply Finset.sum_congr rfl
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal n → ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
intro x hx
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal n
⊢ ↑x.snd ≤ ↑n
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
refine' mul_eq_zero_of_right (coeff R x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt _ h))
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x.fst + x.snd = n
⊢ ↑x.snd ≤ ↑n
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal n
⊢ ↑x.snd ≤ ↑n
rw [Finset.Nat.mem_antidiagonal] at hx
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x.fst + x.snd = n
⊢ x.snd ≤ n
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x.fst + x.snd = n
⊢ ↑x.snd ≤ ↑n
norm_cast
no goals
case this
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
x : ℕ × ℕ
hx : x.fst + x.snd = n
⊢ x.snd ≤ n
linarith