R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∑ p in Finset.Nat.antidiagonal n, ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = ↑(coeff R n) (φ * ψ)
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ↑(coeff R n) (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ
symm
case hi
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a : ℕ × ℕ), a ∈ Finset.Nat.antidiagonal n → (single () a.fst, single () a.snd) ∈ Finsupp.antidiagonal (single () n)

case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a : ℕ × ℕ),
    a ∈ Finset.Nat.antidiagonal n →
      ↑(coeff R a.fst) φ * ↑(coeff R a.snd) ψ =
        ↑(MvPowerSeries.coeff R (single () a.fst, single () a.snd).fst) φ *
          ↑(MvPowerSeries.coeff R (single () a.fst, single () a.snd).snd) ψ

case i_inj
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a₁ a₂ : ℕ × ℕ),
    a₁ ∈ Finset.Nat.antidiagonal n →
      a₂ ∈ Finset.Nat.antidiagonal n →
        (single () a₁.fst, single () a₁.snd) = (single () a₂.fst, single () a₂.snd) → a₁ = a₂

case i_surj
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (b : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    b ∈ Finsupp.antidiagonal (single () n) → ∃ a ha, b = (single () a.fst, single () a.snd)
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∑ p in Finset.Nat.antidiagonal n, ↑(coeff R p.fst) φ * ↑(coeff R p.snd) ψ = ↑(coeff R n) (φ * ψ)
apply Finset.sum_bij fun (p : ℕ × ℕ) _h => (single () p.1, single () p.2)
case hi.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
case hi
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a : ℕ × ℕ), a ∈ Finset.Nat.antidiagonal n → (single () a.fst, single () a.snd) ∈ Finsupp.antidiagonal (single () n)
rintro ⟨i, j⟩ hij
case hi.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
case hi.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
rw [Finset.Nat.mem_antidiagonal] at hij
no goals
case hi.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
rw [Finsupp.mem_antidiagonal, ← Finsupp.single_add, hij]
case h.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ =
    ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) ψ
case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a : ℕ × ℕ),
    a ∈ Finset.Nat.antidiagonal n →
      ↑(coeff R a.fst) φ * ↑(coeff R a.snd) ψ =
        ↑(MvPowerSeries.coeff R (single () a.fst, single () a.snd).fst) φ *
          ↑(MvPowerSeries.coeff R (single () a.fst, single () a.snd).snd) ψ
rintro ⟨i, j⟩ _hij
no goals
case h.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) ψ =
    ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) ψ
rfl
case i_inj.mk.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j k l : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
_hkl : (k, l) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) = (single () (k, l).fst, single () (k, l).snd) → (i, j) = (k, l)
case i_inj
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (a₁ a₂ : ℕ × ℕ),
    a₁ ∈ Finset.Nat.antidiagonal n →
      a₂ ∈ Finset.Nat.antidiagonal n →
        (single () a₁.fst, single () a₁.snd) = (single () a₂.fst, single () a₂.snd) → a₁ = a₂
rintro ⟨i, j⟩ ⟨k, l⟩ _hij _hkl
no goals
case i_inj.mk.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
i j k l : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
_hkl : (k, l) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) = (single () (k, l).fst, single () (k, l).snd) → (i, j) = (k, l)
simpa only [Prod.mk.inj_iff, Finsupp.unique_single_eq_iff] using id
case i_surj.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ ∃ a ha, (f, g) = (single () a.fst, single () a.snd)
case i_surj
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
⊢ ∀ (b : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    b ∈ Finsupp.antidiagonal (single () n) → ∃ a ha, b = (single () a.fst, single () a.snd)
rintro ⟨f, g⟩ hfg
case i_surj.mk.refine'_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n

case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (f, g) = (single () (↑f (), ↑g ()).fst, single () (↑f (), ↑g ()).snd)
case i_surj.mk
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ ∃ a ha, (f, g) = (single () a.fst, single () a.snd)
refine' ⟨(f (), g ()), _, _⟩
case i_surj.mk.refine'_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g).fst + (f, g).snd = single () n
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
case i_surj.mk.refine'_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
rw [Finsupp.mem_antidiagonal] at hfg
no goals
case i_surj.mk.refine'_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g).fst + (f, g).snd = single () n
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
rw [Finset.Nat.mem_antidiagonal, ← Finsupp.add_apply, hfg, Finsupp.single_eq_same]
case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f (), ↑g ()).fst ∧ g = single () (↑f (), ↑g ()).snd
case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (f, g) = (single () (↑f (), ↑g ()).fst, single () (↑f (), ↑g ()).snd)
rw [Prod.mk.inj_iff]
case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f ()) ∧ g = single () (↑g ())
case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f (), ↑g ()).fst ∧ g = single () (↑f (), ↑g ()).snd
dsimp
no goals
case i_surj.mk.refine'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : PowerSeries R
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f ()) ∧ g = single () (↑g ())
exact ⟨Finsupp.unique_single f, Finsupp.unique_single g⟩