Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case intro.intro.intro.intro
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)
⊢ ∑ j ∈ antidiagonal (m + n),
      ∑ i ∈ filter (fun i => s i = j) (antidiagonal m ×ˢ antidiagonal n),
        ↑((i.1.1 + i.2.1).choose i.1.1) * ↑((i.1.2 + i.2.2).choose i.1.2) * hI.dpow (i.1.1 + i.2.1) a *
          hJ.dpow (i.1.2 + i.2.2) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
have hs' :
  ((Finset.antidiagonal (m + n)).sum
    fun y : ℕ × ℕ =>
      ((Finset.antidiagonal m ×ˢ Finset.antidiagonal n).filter    (fun x : (ℕ × ℕ) × ℕ × ℕ => (fun x : (ℕ × ℕ) × ℕ × ℕ => s x) x = y)).sum
        (fun x : (ℕ × ℕ) × ℕ × ℕ =>
        ↑((x.fst.fst + x.snd.fst).choose x.fst.fst) *
              ↑((x.fst.snd + x.snd.snd).choose x.fst.snd) *
            hI.dpow (x.fst.fst + x.snd.fst) a *
          hJ.dpow (x.fst.snd + x.snd.snd) b)) =
    (Finset.antidiagonal (m + n)).sum
      (fun y : ℕ × ℕ =>
      (((Finset.antidiagonal m ×ˢ Finset.antidiagonal n).filter
        (fun x : (ℕ × ℕ) × ℕ × ℕ => (fun x : (ℕ × ℕ) × ℕ × ℕ => s x) x = y)).sum
          (fun x : (ℕ × ℕ) × ℕ × ℕ => (y.fst.choose x.fst.fst) * (y.snd.choose x.fst.snd)) *
          hI.dpow y.fst a *
        hJ.dpow y.snd b)) := by
  apply Finset.sum_congr rfl; rintro ⟨u, v⟩ _
  simp only [Prod.mk.injEq, mem_product, mem_antidiagonal, and_imp, Prod.forall, Nat.cast_sum, Nat.cast_mul]
  simp only [Finset.sum_mul]
  apply Finset.sum_congr rfl; rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ hx
  simp only
  simp only [hs_def, mem_product, mem_antidiagonal, and_imp, Prod.forall, mem_filter,
    Prod.mk.injEq] at hx
  rw [hx.2.1]; rw [hx.2.2]
Proof state after:
case intro.intro.intro.intro
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
⊢ ∑ j ∈ antidiagonal (m + n),
      ∑ i ∈ filter (fun i => s i = j) (antidiagonal m ×ˢ antidiagonal n),
        ↑((i.1.1 + i.2.1).choose i.1.1) * ↑((i.1.2 + i.2.2).choose i.1.2) * hI.dpow (i.1.1 + i.2.1) a *
          hJ.dpow (i.1.2 + i.2.2) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)