internlm/Lean-Github huggingface dataset:
Theorem: rewriting_4_fold_sums
Proof state before:
case mk
α : 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
⊢ (∑
      a ∈
        Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
      if a.1 = (i, j) then g a else 0) =
    f (i, j)
Tactic:
rw [Finset.sum_filter]
Proof state after:
case mk
α : 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
⊢ (∑ a ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
      if a.1.1 + a.2.1 = u ∧ a.1.2 + a.2.2 = v then if a.1 = (i, j) then g a else 0 else 0) =
    f (i, j)
Theorem: rewriting_4_fold_sums
Proof state before:
case mk
α : 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
⊢ (∑ a ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
      if a.1.1 + a.2.1 = u ∧ a.1.2 + a.2.2 = v then if a.1 = (i, j) then g a else 0 else 0) =
    f (i, j)
Tactic:
simp_rw [← ite_and]
Proof state after:
case mk
α : 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
⊢ (∑ x ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
      if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
    f (i, j)
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
⊢ ∀ 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
Tactic:
intro x
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
x : (ℕ × ℕ) × ℕ × ℕ
⊢ 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
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
x : (ℕ × ℕ) × ℕ × ℕ
⊢ 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
Tactic:
simp
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
x : (ℕ × ℕ) × ℕ × ℕ
⊢ x.1.1 + x.1.2 = m → x.2.1 + x.2.2 = n → x.1.1 + x.2.1 = u → x.1.2 + x.2.2 = v → x.1.1 + x.1.2 = m
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
x : (ℕ × ℕ) × ℕ × ℕ
⊢ x.1.1 + x.1.2 = m → x.2.1 + x.2.2 = n → x.1.1 + x.2.1 = u → x.1.2 + x.2.2 = v → x.1.1 + x.1.2 = m
Tactic:
intro h'
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
x : (ℕ × ℕ) × ℕ × ℕ
h' : x.1.1 + x.1.2 = m
⊢ x.2.1 + x.2.2 = n → x.1.1 + x.2.1 = u → x.1.2 + x.2.2 = v → x.1.1 + x.1.2 = m
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
x : (ℕ × ℕ) × ℕ × ℕ
h' : x.1.1 + x.1.2 = m
⊢ x.2.1 + x.2.2 = n → x.1.1 + x.2.1 = u → x.1.2 + x.2.2 = v → x.1.1 + x.1.2 = m
Tactic:
simp [h']
Proof state after:
no goals
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)
⊢ (∑ x ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n,
      if (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j) then g x else 0) =
    f (i, j)
Tactic:
rw [Finset.sum_congr rfl fun x _ => hf' x, ← Finset.sum_mul]
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)
⊢ (∑ 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) *
      f (i, j) =
    f (i, j)
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)
⊢ (∑ 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) *
      f (i, j) =
    f (i, j)
Tactic:
by_cases hij' : i ≤ u ∧ j ≤ v
Proof state after:
case pos
α : 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) *
      f (i, j) =
    f (i, j)

case neg
α : 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) *
      f (i, j) =
    f (i, j)
Theorem: rewriting_4_fold_sums
Proof state before:
case pos
α : 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) *
      f (i, j) =
    f (i, j)
Tactic:
conv_rhs => rw [← one_mul (f ⟨i, j⟩)]
Proof state after:
case pos
α : 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) *
      f (i, j) =
    1 * f (i, j)
Theorem: rewriting_4_fold_sums
Proof state before:
case pos
α : 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) *
      f (i, j) =
    1 * f (i, j)
Tactic:
apply congr_arg₂ _ _ rfl
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
⊢ (∑ 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
Theorem: rewriting_4_fold_sums
Proof state before:
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
Tactic:
rintro ⟨⟨x, y⟩, ⟨z, t⟩⟩ hb hb'
Proof state after:
case h₀.mk.mk.mk
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
⊢ (if
        (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
          ((x, y), z, t).1 = (i, j) then
      1
    else 0) =
    0
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
⊢ (if
        (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
          ((x, y), z, t).1 = (i, j) then
      1
    else 0) =
    0
Tactic:
rw [if_neg]
Proof state after:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
⊢ ¬((((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
      ((x, y), z, t).1 = (i, j))
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
⊢ ¬((((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
      ((x, y), z, t).1 = (i, j))
Tactic:
intro hb''
Proof state after:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
⊢ False
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb : ((x, y), z, t) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
⊢ False
Tactic:
simp only [Finset.mem_product, Finset.mem_antidiagonal] at hb
Proof state after:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
hb : x + y = m ∧ z + t = n
⊢ False
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb' : ((x, y), z, t) ≠ ((i, j), u - i, v - j)
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
hb : x + y = m ∧ z + t = n
⊢ False
Tactic:
simp only [ne_eq, Prod.mk.injEq, not_and, and_imp] at hb'
Proof state after:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
hb : x + y = m ∧ z + t = n
hb' : x = i → y = j → z = u - i → ¬t = v - j
⊢ False
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb'' :
  (((x, y), z, t).1.1 + ((x, y), z, t).2.1 = u ∧ ((x, y), z, t).1.2 + ((x, y), z, t).2.2 = v) ∧
    ((x, y), z, t).1 = (i, j)
hb : x + y = m ∧ z + t = n
hb' : x = i → y = j → z = u - i → ¬t = v - j
⊢ False
Tactic:
simp only [Prod.mk.inj_iff] at hb''
Proof state after:
case h₀.mk.mk.mk.hnc
α : 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
x y z t : ℕ
hb : x + y = m ∧ z + t = n
hb' : x = i → y = j → z = u - i → ¬t = v - j
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
⊢ False