Theorem: rewriting_4_fold_sums
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
hf' :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
      (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then 1 else 0) * f (i, j)
hij' : i ≤ u ∧ j ≤ v
⊢ (∑ i_1 ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
      if (i_1.1.1 + i_1.2.1 = u ∧ i_1.1.2 + i_1.2.2 = v) ∧ i_1.1 = (i, j) then 1 else 0) =
    1
Tactic:
rw [Finset.sum_eq_single (⟨⟨i, j⟩, ⟨u - i, v - j⟩⟩ : (ℕ × ℕ) × ℕ × ℕ)]
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
hf' :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
      (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then 1 else 0) * f (i, j)
hij' : i ≤ u ∧ j ≤ v
⊢ (if
        (((i, j), u - i, v - j).1.1 + ((i, j), u - i, v - j).2.1 = u ∧
            ((i, j), u - i, v - j).1.2 + ((i, j), u - i, v - j).2.2 = v) ∧
          ((i, j), u - i, v - j).1 = (i, j) then
      1
    else 0) =
    1

case h₀
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
hf' :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
      (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then 1 else 0) * f (i, j)
hij' : i ≤ u ∧ j ≤ v
⊢ ∀ b ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
    b ≠ ((i, j), u - i, v - j) → (if (b.1.1 + b.2.1 = u ∧ b.1.2 + b.2.2 = v) ∧ b.1 = (i, j) then 1 else 0) = 0

case h₁
α : Type u_1
inst✝ : CommSemiring α
m n u v : ℕ
h : m + n = u + v
f : ℕ × ℕ → α
g : (ℕ × ℕ) × ℕ × ℕ → α
hgf : g = fun x => f (x.1.1, x.1.2)
hf : ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → f x = 0
hq :
  ∀ x ∈ Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
    x.1 ∈ Finset.antidiagonal m
i j : ℕ
hij : i + j = m
hf' :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
      (if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then 1 else 0) * f (i, j)
hij' : i ≤ u ∧ j ≤ v
⊢ ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n →
    (if
          (((i, j), u - i, v - j).1.1 + ((i, j), u - i, v - j).2.1 = u ∧
              ((i, j), u - i, v - j).1.2 + ((i, j), u - i, v - j).2.2 = v) ∧
            ((i, j), u - i, v - j).1 = (i, j) then
        1
      else 0) =
      0