Theorem: DividedPowers.IdealAdd.dpow_mul (DividedPowers/IdealAdd.lean)

State before:
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 : ℕ
x : A
⊢ x ∈ I + J → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + n) x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup]
State after:
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 : ℕ
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + n) x

State before:
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 : ℕ
x : A
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → dpow hI hJ m x * dpow hI hJ n x = ↑((m + n).choose m) * dpow hI hJ (m + n) x
Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
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
⊢ dpow hI hJ m (a + b) * dpow hI hJ n (a + b) = ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ dpow hI hJ m (a + b) * dpow hI hJ n (a + b) = ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ m ha hb]
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
⊢ (∑ k ∈ range (m + 1), hI.dpow k a * hJ.dpow (m - k) b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ (∑ k ∈ range (m + 1), hI.dpow k a * hJ.dpow (m - k) b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => hI.dpow i a * hJ.dpow j b]
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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * dpow hI hJ n (a + b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ n ha hb]
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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun k l => hI.dpow k a * hJ.dpow l b]
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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ (∑ ij ∈ antidiagonal m, hI.dpow ij.1 a * hJ.dpow ij.2 b) * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [Finset.sum_mul]
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
⊢ ∑ i ∈ antidiagonal m, hI.dpow i.1 a * hJ.dpow i.2 b * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ ∑ i ∈ antidiagonal m, hI.dpow i.1 a * hJ.dpow i.2 b * ∑ ij ∈ antidiagonal n, hI.dpow ij.1 a * hJ.dpow ij.2 b =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
simp_rw [Finset.mul_sum]
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
⊢ ∑ x ∈ antidiagonal m, ∑ i ∈ antidiagonal n, hI.dpow x.1 a * hJ.dpow x.2 b * (hI.dpow i.1 a * hJ.dpow i.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ ∑ x ∈ antidiagonal m, ∑ i ∈ antidiagonal n, hI.dpow x.1 a * hJ.dpow x.2 b * (hI.dpow i.1 a * hJ.dpow i.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.sum_product']
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
⊢ ∑ x ∈ antidiagonal m ×ˢ antidiagonal n, hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ ∑ x ∈ antidiagonal m ×ˢ antidiagonal n, hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
have hf :
  ∀ x : (ℕ × ℕ) × ℕ × ℕ,
    hI.dpow x.fst.fst a * hJ.dpow x.fst.snd b * (hI.dpow x.snd.fst a * hJ.dpow x.snd.snd b) =
      (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 := by
  rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
  dsimp
  rw [mul_assoc]; rw [← mul_assoc (hJ.dpow j b) _ _]; rw [mul_comm (hJ.dpow j b)]
  rw [mul_assoc]; rw [hJ.dpow_mul j l hb]
  rw [← mul_assoc]; rw [hI.dpow_mul i k ha]
  ring
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
⊢ ∑ x ∈ antidiagonal m ×ˢ antidiagonal n, hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ ∑ x ∈ antidiagonal m ×ˢ antidiagonal n, hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [Finset.sum_congr rfl fun x _ => hf x]
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
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
set s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => ⟨x.fst.fst + x.snd.fst, x.fst.snd + x.snd.snd⟩
  with hs_def
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)
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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)
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
have hs :
  ∀ x ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
    s x ∈ Finset.antidiagonal (m + n) :=
  by
  rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ h
  simp only [Finset.mem_antidiagonal, Finset.mem_product] at h ⊢
  rw [add_assoc, ← add_assoc k j l, add_comm k _, add_assoc, h.2, ← add_assoc, h.1]
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)
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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)
⊢ ∑ x ∈ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [← Finset.sum_fiberwise_of_maps_to hs]
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)
⊢ ∑ 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)

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]
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)

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)
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)
Tactic:
rw [hs']
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)

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)
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * dpow hI hJ (m + n) (a + b)
Tactic:
rw [dpow_eq hI hJ hIJ (m + n) ha hb]
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * ∑ k ∈ range (m + n + 1), hI.dpow k a * hJ.dpow (m + n - k) b

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)
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * ∑ k ∈ range (m + n + 1), hI.dpow k a * hJ.dpow (m + n - k) b
Tactic:
rw [← Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => hI.dpow i a * hJ.dpow j b]
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * ∑ ij ∈ antidiagonal (m + n), hI.dpow ij.1 a * hJ.dpow ij.2 b

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)
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
⊢ ∑ 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 =
    ↑((m + n).choose m) * ∑ ij ∈ antidiagonal (m + n), hI.dpow ij.1 a * hJ.dpow ij.2 b
Tactic:
rw [Finset.mul_sum]
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
⊢ ∑ 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 =
    ∑ i ∈ antidiagonal (m + n), ↑((m + n).choose m) * (hI.dpow i.1 a * hJ.dpow i.2 b)

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)
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
⊢ ∑ 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 =
    ∑ i ∈ antidiagonal (m + n), ↑((m + n).choose m) * (hI.dpow i.1 a * hJ.dpow i.2 b)
Tactic:
apply Finset.sum_congr rfl
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
⊢ ∀ x ∈ antidiagonal (m + n),
    ↑(∑ x_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b =
      ↑((m + n).choose m) * (hI.dpow x.1 a * hJ.dpow x.2 b)

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)
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
⊢ ∀ x ∈ antidiagonal (m + n),
    ↑(∑ x_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b =
      ↑((m + n).choose m) * (hI.dpow x.1 a * hJ.dpow x.2 b)
Tactic:
rintro ⟨u, v⟩ h
State after:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 b =
    ↑((m + n).choose m) * (hI.dpow (u, v).1 a * hJ.dpow (u, v).2 b)

State before:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 b =
    ↑((m + n).choose m) * (hI.dpow (u, v).1 a * hJ.dpow (u, v).2 b)
Tactic:
simp only [Prod.mk.inj_iff]
State after:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
        hI.dpow u a *
      hJ.dpow v b =
    ↑((m + n).choose m) * (hI.dpow u a * hJ.dpow v b)

State before:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
        hI.dpow u a *
      hJ.dpow v b =
    ↑((m + n).choose m) * (hI.dpow u a * hJ.dpow v b)
Tactic:
rw [← mul_assoc]
State after:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
        hI.dpow u a *
      hJ.dpow v b =
    ↑((m + n).choose m) * hI.dpow u a * hJ.dpow v b

State before:
case intro.intro.intro.intro.mk
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
        hI.dpow u a *
      hJ.dpow v b =
    ↑((m + n).choose m) * hI.dpow u a * hJ.dpow v b
Tactic:
apply congr_arg₂ _ _ rfl
State after:
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
      hI.dpow u a =
    ↑((m + n).choose m) * hI.dpow u a

State before:
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) *
      hI.dpow u a =
    ↑((m + n).choose m) * hI.dpow u a
Tactic:
apply congr_arg₂ _ _ rfl
State after:
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) =
    ↑((m + n).choose m)

State before:
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) ∈ antidiagonal (m + n)
⊢ ↑(∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2) =
    ↑((m + n).choose m)
Tactic:
apply congr_arg
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) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m

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) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m
Tactic:
simp only [Finset.mem_antidiagonal] at h
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 ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m

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 => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m
Tactic:
simp only [hs_def, Prod.mk.injEq]
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 ∈ 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

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 _]
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

State before:
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
⊢ ∀ (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
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow ((i, j), k, l).1.1 a * hJ.dpow ((i, j), k, l).1.2 b *
      (hI.dpow ((i, j), k, l).2.1 a * hJ.dpow ((i, j), k, l).2.2 b) =
    ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow ((i, j), k, l).1.1 a * hJ.dpow ((i, j), k, l).1.2 b *
      (hI.dpow ((i, j), k, l).2.1 a * hJ.dpow ((i, j), k, l).2.2 b) =
    ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b
Tactic:
dsimp
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * hJ.dpow j b * (hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * hJ.dpow j b * (hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_assoc]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * (hI.dpow k a * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * (hI.dpow k a * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [← mul_assoc (hJ.dpow j b) _ _]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_comm (hJ.dpow j b)]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * hJ.dpow j b * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * hJ.dpow j b * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_assoc]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (hJ.dpow j b * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (hJ.dpow j b * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [hJ.dpow_mul j l hb]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [← mul_assoc]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ hI.dpow i a * hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [hI.dpow_mul i k ha]
State after:
case mk.mk.mk
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
i j k l : ℕ
⊢ ↑((i + k).choose i) * hI.dpow (i + k) a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b

State before:
case mk.mk.mk
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
i j k l : ℕ
⊢ ↑((i + k).choose i) * hI.dpow (i + k) a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
ring
State after:
no goals

State before:
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)
⊢ ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ h
State after:
case mk.mk.mk
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)
i j k l : ℕ
h : ((i, j), k, l) ∈ antidiagonal m ×ˢ antidiagonal n
⊢ s ((i, j), k, l) ∈ antidiagonal (m + n)

State before:
case mk.mk.mk
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)
i j k l : ℕ
h : ((i, j), k, l) ∈ antidiagonal m ×ˢ antidiagonal n
⊢ s ((i, j), k, l) ∈ antidiagonal (m + n)
Tactic:
simp only [Finset.mem_antidiagonal, Finset.mem_product] at h ⊢
State after:
case mk.mk.mk
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)
i j k l : ℕ
h : i + j = m ∧ k + l = n
⊢ i + k + (j + l) = m + n

State before:
case mk.mk.mk
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)
i j k l : ℕ
h : i + j = m ∧ k + l = n
⊢ i + k + (j + l) = m + n
Tactic:
rw [add_assoc, ← add_assoc k j l, add_comm k _, add_assoc, h.2, ← add_assoc, h.1]
State after:
no goals

State before:
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)
⊢ ∑ 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
Tactic:
apply Finset.sum_congr rfl
State after:
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)
⊢ ∀ x ∈ antidiagonal (m + n),
    ∑ x ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (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 =
      ↑(∑ x_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b

State before:
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)
⊢ ∀ x ∈ antidiagonal (m + n),
    ∑ x ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (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 =
      ↑(∑ x_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b
Tactic:
rintro ⟨u, v⟩ _
State after:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (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 =
    ↑(∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 b

State before:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (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 =
    ↑(∑ x ∈ filter (fun x => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 b
Tactic:
simp only [Prod.mk.injEq, mem_product, mem_antidiagonal, and_imp, Prod.forall, Nat.cast_sum, Nat.cast_mul]
State after:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (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 =
    (∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), ↑(u.choose x.1.1) * ↑(v.choose x.1.2)) *
        hI.dpow u a *
      hJ.dpow v b

State before:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (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 =
    (∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), ↑(u.choose x.1.1) * ↑(v.choose x.1.2)) *
        hI.dpow u a *
      hJ.dpow v b
Tactic:
simp only [Finset.sum_mul]
State after:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (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 =
    ∑ i ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑(u.choose i.1.1) * ↑(v.choose i.1.2) * hI.dpow u a * hJ.dpow v b

State before:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (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 =
    ∑ i ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑(u.choose i.1.1) * ↑(v.choose i.1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
apply Finset.sum_congr rfl
State after:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∀ x ∈ filter (fun x => s x = (u, v)) (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 =
      ↑(u.choose x.1.1) * ↑(v.choose x.1.2) * hI.dpow u a * hJ.dpow v b

State before:
case mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∀ x ∈ filter (fun x => s x = (u, v)) (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 =
      ↑(u.choose x.1.1) * ↑(v.choose x.1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ hx
State after:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b =
    ↑(u.choose ((i, j), k, l).1.1) * ↑(v.choose ((i, j), k, l).1.2) * hI.dpow u a * hJ.dpow v b

State before:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b =
    ↑(u.choose ((i, j), k, l).1.1) * ↑(v.choose ((i, j), k, l).1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
simp only
State after:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b

State before:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
simp only [hs_def, mem_product, mem_antidiagonal, and_imp, Prod.forall, mem_filter,
  Prod.mk.injEq] at hx
State after:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b

State before:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
rw [hx.2.1]
State after:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑(u.choose i) * ↑((j + l).choose j) * hI.dpow u a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b

State before:
case mk.mk.mk.mk
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)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑(u.choose i) * ↑((j + l).choose j) * hI.dpow u a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
rw [hx.2.2]
State after:
no goals

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 ∈ antidiagonal m, u.choose x.1 * v.choose x.2 = (m + n).choose m
Tactic:
rw [← Nat.add_choose_eq]
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
⊢ (u + v).choose m = (m + n).choose m

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
⊢ (u + v).choose m = (m + n).choose m
Tactic:
rw [h]
State after:
no goals

State before:
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
Tactic:
intro x h
State after:
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 : ℕ × ℕ
h : u < x.1 ∨ v < x.2
⊢ (fun x => u.choose x.1 * v.choose x.2) x = 0

State before:
case inr
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 : ℕ × ℕ
h : v < x.2
⊢ (fun x => u.choose x.1 * v.choose x.2) x = 0
Tactic:
simp only [Nat.choose_eq_zero_of_lt h, MulZeroClass.zero_mul, MulZeroClass.mul_zero]
State after:
no goals