case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ → ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0) → X s ^ n ∣ φ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
constructor
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
⊢ ↑(coeff R m) (X s ^ n * φ) = 0
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ → ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
rintro ⟨φ, rfl⟩ m h
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), x ∈ antidiagonal m → ↑(coeff R x.fst) (X s ^ n) * ↑(coeff R x.snd) φ = 0
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
⊢ ↑(coeff R m) (X s ^ n * φ) = 0
rw [coeff_mul, Finset.sum_eq_zero]
case mp.intro.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) φ = 0
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), x ∈ antidiagonal m → ↑(coeff R x.fst) (X s ^ n) * ↑(coeff R x.snd) φ = 0
rintro ⟨i, j⟩ hij
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).fst = single s n
case mp.intro.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) φ = 0
rw [coeff_X_pow, if_neg, MulZeroClass.zero_mul]
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
h : i = single s n
⊢ n ≤ ↑m s
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : ↑m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).fst = single s n
contrapose! h
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j) ∈ antidiagonal m
⊢ n ≤ ↑m s
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
h : i = single s n
⊢ n ≤ ↑m s
subst i
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).fst + (single s n, j).snd = m
⊢ n ≤ ↑m s
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j) ∈ antidiagonal m
⊢ n ≤ ↑m s
rw [Finsupp.mem_antidiagonal] at hij
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).fst + (single s n, j).snd = m
⊢ n ≤ n + ↑(single s n, j).snd s
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).fst + (single s n, j).snd = m
⊢ n ≤ ↑m s
rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
no goals
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).fst + (single s n, j).snd = m
⊢ n ≤ n + ↑(single s n, j).snd s
exact Nat.le_add_right n _
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
⊢ X s ^ n ∣ φ
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0) → X s ^ n ∣ φ
intro h
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
⊢ φ = X s ^ n * fun m => ↑(coeff R (m + single s n)) φ
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
⊢ X s ^ n ∣ φ
refine' ⟨fun m => coeff R (m + single s n) φ, _⟩
case mpr.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
⊢ φ = X s ^ n * fun m => ↑(coeff R (m + single s n)) φ
ext m
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)
case mpr.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)
by_cases H : m - single s n + single s n = m
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ =
    ↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
      ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ

case pos.h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ∀ (b : (σ →₀ ℕ) × (σ →₀ ℕ)),
    b ∈ antidiagonal m →
      b ≠ (single s n, m - single s n) →
        (↑(coeff R b.fst) (X s ^ n) * ↑(coeff R b.snd) fun m => ↑(coeff R (m + single s n)) φ) = 0

case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ¬(single s n, m - single s n) ∈ antidiagonal m →
    (↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
        ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ) =
      0
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)
rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ =
    ↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
      ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ
rw [coeff_X_pow, if_pos rfl, one_mul]
no goals
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ
simpa using congr_arg (fun m : σ →₀ ℕ => coeff R m φ) H.symm
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case pos.h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ∀ (b : (σ →₀ ℕ) × (σ →₀ ℕ)),
    b ∈ antidiagonal m →
      b ≠ (single s n, m - single s n) →
        (↑(coeff R b.fst) (X s ^ n) * ↑(coeff R b.snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rintro ⟨i, j⟩ hij hne
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rw [Finsupp.mem_antidiagonal] at hij
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ ((if (i, j).fst = single s n then 1 else 0) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rw [coeff_X_pow]
case pos.h₀.mk.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ (1 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0

case pos.h₀.mk.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : ¬(i, j).fst = single s n
⊢ (0 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ ((if (i, j).fst = single s n then 1 else 0) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
split_ifs with hi
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ False
case pos.h₀.mk.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ (1 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
exfalso
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ (i, j) = (single s n, m - single s n)
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ False
apply hne
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ i = (i, j).fst ∧ j = (i, j).fst + (i, j).snd - (i, j).fst
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ (i, j) = (single s n, m - single s n)
rw [← hij, ← hi, Prod.mk.inj_iff]
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ j = (i, j).fst + (i, j).snd - (i, j).fst
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ i = (i, j).fst ∧ j = (i, j).fst + (i, j).snd - (i, j).fst
refine' ⟨rfl, _⟩
case pos.h₀.mk.inl.h.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
t : σ
⊢ ↑j t = ↑((i, j).fst + (i, j).snd - (i, j).fst) t
case pos.h₀.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
⊢ j = (i, j).fst + (i, j).snd - (i, j).fst
ext t
no goals
case pos.h₀.mk.inl.h.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).fst = single s n
t : σ
⊢ ↑j t = ↑((i, j).fst + (i, j).snd - (i, j).fst) t
simp only [add_tsub_cancel_left, Finsupp.add_apply, Finsupp.tsub_apply]
no goals
case pos.h₀.mk.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : ¬(i, j).fst = single s n
⊢ (0 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
exact MulZeroClass.zero_mul _
case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ (↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
      ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ) =
    0
case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ ¬(single s n, m - single s n) ∈ antidiagonal m →
    (↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
        ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ) =
      0
intro hni
case pos.h₁.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ False
case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ (↑(coeff R (single s n, m - single s n).fst) (X s ^ n) *
      ↑(coeff R (single s n, m - single s n).snd) fun m => ↑(coeff R (m + single s n)) φ) =
    0
exfalso
case pos.h₁.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ (single s n, m - single s n) ∈ antidiagonal m
case pos.h₁.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ False
apply hni
no goals
case pos.h₁.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : ¬(single s n, m - single s n) ∈ antidiagonal m
⊢ (single s n, m - single s n) ∈ antidiagonal m
rwa [Finsupp.mem_antidiagonal, add_comm]
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    x ∈ antidiagonal m → (↑(coeff R x.fst) (X s ^ n) * ↑(coeff R x.snd) fun m => ↑(coeff R (m + single s n)) φ) = 0

case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ↑m s < n
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ↑(coeff R m) φ = ↑(coeff R m) (X s ^ n * fun m => ↑(coeff R (m + single s n)) φ)
rw [h, coeff_mul, Finset.sum_eq_zero]
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    x ∈ antidiagonal m → (↑(coeff R x.fst) (X s ^ n) * ↑(coeff R x.snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rintro ⟨i, j⟩ hij
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rw [Finsupp.mem_antidiagonal] at hij
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
⊢ ((if (i, j).fst = single s n then 1 else 0) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
⊢ (↑(coeff R (i, j).fst) (X s ^ n) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
rw [coeff_X_pow]
case neg.mk.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ (1 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0

case neg.mk.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : ¬(i, j).fst = single s n
⊢ (0 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
⊢ ((if (i, j).fst = single s n then 1 else 0) * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
split_ifs with hi
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ False
case neg.mk.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ (1 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
exfalso
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ m - single s n + single s n = m
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ False
apply H
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ single s n + (i, j).snd - single s n + single s n = single s n + (i, j).snd
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ m - single s n + single s n = m
rw [← hij, hi]
case neg.mk.inl.h.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
a✝ : σ
⊢ ↑(single s n + (i, j).snd - single s n + single s n) a✝ = ↑(single s n + (i, j).snd) a✝
case neg.mk.inl.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
⊢ single s n + (i, j).snd - single s n + single s n = single s n + (i, j).snd
ext
no goals
case neg.mk.inl.h.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : (i, j).fst = single s n
a✝ : σ
⊢ ↑(single s n + (i, j).snd - single s n + single s n) a✝ = ↑(single s n + (i, j).snd) a✝
rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
no goals
case neg.mk.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).fst + (i, j).snd = m
hi : ¬(i, j).fst = single s n
⊢ (0 * ↑(coeff R (i, j).snd) fun m => ↑(coeff R (m + single s n)) φ) = 0
exact MulZeroClass.zero_mul _
case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
⊢ m - single s n + single s n = m
case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ↑m s < n
contrapose! H
case neg.a.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
⊢ ↑(m - single s n + single s n) t = ↑m t
case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
⊢ m - single s n + single s n = m
ext t
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
hst : s = t
⊢ ↑(m - single s n + single s n) t = ↑m t

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
hst : ¬s = t
⊢ ↑(m - single s n + single s n) t = ↑m t
case neg.a.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
⊢ ↑(m - single s n + single s n) t = ↑m t
by_cases hst : s = t
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
⊢ ↑(m - single s n + single s n) s = ↑m s
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
hst : s = t
⊢ ↑(m - single s n + single s n) t = ↑m t
subst t
no goals
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
⊢ ↑(m - single s n + single s n) s = ↑m s
simpa using tsub_add_cancel_of_le H
no goals
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < n → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ ↑m s
t : σ
hst : ¬s = t
⊢ ↑(m - single s n + single s n) t = ↑m t
simp [Finsupp.single_apply, hst]