case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ ∀ (i : ℕ), ↑i < order φ + order ψ → ↑(coeff R i) (φ * ψ) = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ order φ + order ψ ≤ order (φ * ψ)
apply le_order
case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
⊢ ↑(coeff R n) (φ * ψ) = 0
case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ ∀ (i : ℕ), ↑i < order φ + order ψ → ↑(coeff R i) (φ * ψ) = 0
intro n hn
case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal n → ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
⊢ ↑(coeff R n) (φ * ψ) = 0
rw [coeff_mul, Finset.sum_eq_zero]
case h.mk
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal n → ↑(coeff R x.fst) φ * ↑(coeff R x.snd) ψ = 0
rintro ⟨i, j⟩ hij
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ↑i < order φ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0

case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case h.mk
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
by_cases hi : ↑i < order φ
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
hj : ↑j < order ψ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0

case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
hj : ¬↑j < order ψ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
by_cases hj : ↑j < order ψ
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
hj : ¬↑j < order ψ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [not_lt] at hi hj
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [Finset.Nat.mem_antidiagonal] at hij
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ False
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
exfalso
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑n = ↑i + ↑j
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ False
apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)
no goals
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
hi : order φ ≤ ↑i
hj : order ψ ≤ ↑j
⊢ ↑n = ↑i + ↑j
rw [← Nat.cast_add, hij]
no goals
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ↑i < order φ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [coeff_of_lt_order i hi, MulZeroClass.zero_mul]
no goals
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
n : ℕ
hn : ↑n < order φ + order ψ
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
hi : ¬↑i < order φ
hj : ↑j < order ψ
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [coeff_of_lt_order j hj, MulZeroClass.mul_zero]