internlm/Lean-Github huggingface dataset:
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j = m ∧ u - i + (v - j) = n
Tactic:
apply And.intro hij
Proof state after:
case h₁.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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ u - i + (v - j) = n
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ u - i + (v - j) = n
Tactic:
apply Nat.add_left_cancel
Proof state after:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ ?h₁.hnc.n + (u - i + (v - j)) = ?h₁.hnc.n + n

case h₁.hnc.n
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ ℕ
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ ?h₁.hnc.n + (u - i + (v - j)) = ?h₁.hnc.n + n

case h₁.hnc.n
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ ℕ
Tactic:
rw [h, ← hij]
Proof state after:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i + (v - j)) = u + v
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i + (v - j)) = u + v
Tactic:
conv_rhs => rw [← hb'.1, ← hb'.2]
Proof state after:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i + (v - j)) = i + (u - i) + (j + (v - j))
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i + (v - j)) = i + (u - i) + (j + (v - j))
Tactic:
simp only [← add_assoc, add_left_inj]
Proof state after:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i) = i + (u - i) + j
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ i + j + (u - i) = i + (u - i) + j
Tactic:
simp only [add_assoc, add_right_inj]
Proof state after:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ j + (u - i) = u - i + j
Theorem: rewriting_4_fold_sums
Proof state before:
case h₁.hnc.a
α : 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
hb : ((i, j), u - i, v - j) ∉ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
hb' : i + (u - i) = u ∧ j + (v - j) = v
⊢ j + (u - i) = u - i + j
Tactic:
apply add_comm
Proof state after:
no goals
Theorem: rewriting_4_fold_sums
Proof state before:
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)
Tactic:
simp only [not_and_or, not_le] at hij'
Proof state after:
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' : u < i ∨ v < 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:
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' : u < i ∨ v < 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:
rw [hf ⟨i, j⟩ hij', MulZeroClass.mul_zero]
Proof state after:
no goals
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
⊢ ∀ (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)
Tactic:
intro x
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 : (ℕ × ℕ) × ℕ × ℕ
⊢ (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)
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
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)
Tactic:
split_ifs with hx
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
x : (ℕ × ℕ) × ℕ × ℕ
hx : (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j)
⊢ g x = 1 * 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
x : (ℕ × ℕ) × ℕ × ℕ
hx : ¬((x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j))
⊢ 0 = 0 * 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
x : (ℕ × ℕ) × ℕ × ℕ
hx : (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j)
⊢ g x = 1 * f (i, j)
Tactic:
simp only [one_mul, hgf]
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
x : (ℕ × ℕ) × ℕ × ℕ
hx : (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j)
⊢ f (x.1.1, x.1.2) = 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
x : (ℕ × ℕ) × ℕ × ℕ
hx : (x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j)
⊢ f (x.1.1, x.1.2) = f (i, j)
Tactic:
rw [hx.2]
Proof state after:
no goals
Theorem: rewriting_4_fold_sums
Proof state before:
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
x : (ℕ × ℕ) × ℕ × ℕ
hx : ¬((x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) ∧ x.1 = (i, j))
⊢ 0 = 0 * f (i, j)
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ (∑ x ∈ antidiagonal n,
      match x with
      | (k, l) =>
        ∑ x ∈ antidiagonal k,
          match x with
          | (a, b) =>
            ∑ x ∈ antidiagonal l,
              match x with
              | (c, d) => f (a, b, c, d)) =
    ∑ x ∈ antidiagonal n,
      match x with
      | (k, l) =>
        ∑ x ∈ antidiagonal k,
          match x with
          | (a, c) =>
            ∑ x ∈ antidiagonal l,
              match x with
              | (b, d) => f (a, b, c, d)
Tactic:
simp only [Finset.sum_sigma']
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Tactic:
set φ : ((_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ) → ((_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ) :=
  fun ⟨⟨_, _⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ ↦ ⟨⟨a+c, b+ d⟩, ⟨⟨a, c⟩, ⟨b, d⟩⟩⟩
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Tactic:
suffices hφ : _ by
  suffices hφ' : _ by
    apply Finset.sum_bij' (fun m _ => φ m) (fun m _ => φ m) hφ hφ hφ' hφ'
    rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
    simp only [mem_sigma, mem_antidiagonal] at H ⊢
  rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
  simp only [mem_sigma, mem_antidiagonal] at H ⊢
  simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_eq_eq, and_true, φ, H.2.1, H.2.2]
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
⊢ ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2