R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
⊢ ¬φ = 0 → ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
⊢ φ = 0 ∨ ψ = 0
rw [or_iff_not_imp_left]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
⊢ ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
⊢ ¬φ = 0 → ψ = 0
intro H
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
⊢ ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
⊢ ψ = 0
have ex : ∃ m, coeff R m φ ≠ 0 := by
  contrapose! H
  exact ext H
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
⊢ ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
⊢ ψ = 0
let m := Nat.find ex
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
⊢ ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
⊢ ψ = 0
have hm₁ : coeff R m φ ≠ 0 := Nat.find_spec ex
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
⊢ ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
⊢ ψ = 0
have hm₂ : ∀ k < m, ¬coeff R k φ ≠ 0 := fun k => Nat.find_min ex
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
⊢ ↑(coeff R n) ψ = ↑(coeff R n) 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
⊢ ψ = 0
ext n
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
⊢ ↑(coeff R n) ψ = 0
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
⊢ ↑(coeff R n) ψ = ↑(coeff R n) 0
rw [(coeff R n).map_zero]
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
⊢ ↑(coeff R n) ψ = 0
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
⊢ ↑(coeff R n) ψ = 0
induction' n using Nat.strong_induction_on with n ih
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m + n)) (φ * ψ) = ↑(coeff R (m + n)) 0
⊢ ↑(coeff R n) ψ = 0
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
⊢ ↑(coeff R n) ψ = 0
replace h := congr_arg (coeff R (m + n)) h
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m, n).fst) φ * ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0

case h.h.h₀
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal (m + n) → b ≠ (m, n) → ↑(coeff R b.fst) φ * ↑(coeff R b.snd) ψ = 0

case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ¬(m, n) ∈ Finset.Nat.antidiagonal (m + n) → ↑(coeff R (m, n).fst) φ * ↑(coeff R (m, n).snd) ψ = 0
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m + n)) (φ * ψ) = ↑(coeff R (m + n)) 0
⊢ ↑(coeff R n) ψ = 0
rw [LinearMap.map_zero, coeff_mul, Finset.sum_eq_single (m, n)] at h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ∀ (m : ℕ), ↑(coeff R m) φ = 0
⊢ φ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ¬φ = 0
⊢ ∃ m, ↑(coeff R m) φ ≠ 0
contrapose! H
no goals
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
h : φ * ψ = 0
H : ∀ (m : ℕ), ↑(coeff R m) φ = 0
⊢ φ = 0
exact ext H
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m, n).fst) φ = 0 ∨ ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m, n).fst) φ * ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0
replace h := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ¬↑(coeff R (m, n).fst) φ = 0 → ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ↑(coeff R (m, n).fst) φ = 0 ∨ ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0
rw [or_iff_not_imp_left] at h
no goals
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ¬↑(coeff R (m, n).fst) φ = 0 → ↑(coeff R (m, n).snd) ψ = 0
⊢ ↑(coeff R n) ψ = 0
exact h hm₁
case h.h.h₀.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case h.h.h₀
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal (m + n) → b ≠ (m, n) → ↑(coeff R b.fst) φ * ↑(coeff R b.snd) ψ = 0
rintro ⟨i, j⟩ hij hne
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0

case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case h.h.h₀.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
by_cases hj : j < n
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0

case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : ¬i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
by_cases hi : i < m
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : ¬i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : ¬i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [Finset.Nat.mem_antidiagonal] at hij
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : ¬i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
push_neg  at hi hj
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
⊢ m < i
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
suffices m < i by
  have : m + n < i + j := add_lt_add_of_lt_of_le this hj
  exfalso
  exact ne_of_lt this hij.symm
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hi : Nat.find ex ≤ i
hj : n ≤ j
hne : i ≤ Nat.find ex
⊢ (i, j) = (Nat.find ex, n)
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
⊢ m < i
contrapose! hne
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
j : ℕ
hj : n ≤ j
hij : (Nat.find ex, j).fst + (Nat.find ex, j).snd = m + n
hi hne : Nat.find ex ≤ Nat.find ex
⊢ (Nat.find ex, j) = (Nat.find ex, n)
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hi : Nat.find ex ≤ i
hj : n ≤ j
hne : i ≤ Nat.find ex
⊢ (i, j) = (Nat.find ex, n)
obtain rfl := le_antisymm hi hne
no goals
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
j : ℕ
hj : n ≤ j
hij : (Nat.find ex, j).fst + (Nat.find ex, j).snd = m + n
hi hne : Nat.find ex ≤ Nat.find ex
⊢ (Nat.find ex, j) = (Nat.find ex, n)
simpa [Ne.def, Prod.mk.inj_iff] using (add_right_inj m).mp hij
no goals
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [ih j hj, MulZeroClass.mul_zero]
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : ¬↑(coeff R i) φ ≠ 0
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
specialize hm₂ _ hi
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : ↑(coeff R i) φ = 0
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : ¬↑(coeff R i) φ ≠ 0
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
push_neg  at hm₂
no goals
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : ↑(coeff R i) φ = 0
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
rw [hm₂, MulZeroClass.zero_mul]
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
this✝ : m < i
this : m + n < i + j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
this : m < i
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
have : m + n < i + j := add_lt_add_of_lt_of_le this hj
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
this✝ : m < i
this : m + n < i + j
⊢ False
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
this✝ : m < i
this : m + n < i + j
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ = 0
exfalso
no goals
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = m + n
hne : (i, j) ≠ (m, n)
hi : Nat.find ex ≤ i
hj : n ≤ j
this✝ : m < i
this : m + n < i + j
⊢ False
exact ne_of_lt this hij.symm
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ↑(coeff R (Nat.find ex)) φ * ↑(coeff R n) ψ ≠ 0 → (Nat.find ex, n) ∈ Finset.Nat.antidiagonal (Nat.find ex + n)
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ¬(m, n) ∈ Finset.Nat.antidiagonal (m + n) → ↑(coeff R (m, n).fst) φ * ↑(coeff R (m, n).snd) ψ = 0
contrapose!
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
a✝ : ↑(coeff R (Nat.find ex)) φ * ↑(coeff R n) ψ ≠ 0
⊢ (Nat.find ex, n) ∈ Finset.Nat.antidiagonal (Nat.find ex + n)
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
⊢ ↑(coeff R (Nat.find ex)) φ * ↑(coeff R n) ψ ≠ 0 → (Nat.find ex, n) ∈ Finset.Nat.antidiagonal (Nat.find ex + n)
intro
no goals
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : PowerSeries R
H : ¬φ = 0
ex : ∃ m, ↑(coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : ↑(coeff R m) φ ≠ 0
hm₂ : ∀ (k : ℕ), k < m → ¬↑(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ (m : ℕ), m < n → ↑(coeff R m) ψ = 0
h : ∑ p in Finset.Nat.antidiagonal (m + n), ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = 0
a✝ : ↑(coeff R (Nat.find ex)) φ * ↑(coeff R n) ψ ≠ 0
⊢ (Nat.find ex, n) ∈ Finset.Nat.antidiagonal (Nat.find ex + n)
rw [Finset.Nat.mem_antidiagonal]