Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ ∑ x ∈ filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (antidiagonal m ×ˢ antidiagonal n),
      u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m
Tactic:
rw [rewriting_4_fold_sums h.symm (fun x => u.choose x.fst * v.choose x.snd) rfl _]
Proof state after:
case h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ ∑ x ∈ antidiagonal m, u.choose x.1 * v.choose x.2 = (m + n).choose m

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → (fun x => u.choose x.1 * v.choose x.2) x = 0