internlm/Lean-Github huggingface dataset:
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 = 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
Tactic:
specialize hb' hb''.2.1 hb''.2.2
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 + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : 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 = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ False
Tactic:
rw [hb''.2.1, hb''.2.2] 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 : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : 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 : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ False
Tactic:
apply hb'
Proof state after:
case h₀.mk.mk.mk.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ z = u - i

case h₀.mk.mk.mk.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ t = v - j
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ?h₀.mk.mk.mk.hnc.a.n + z = ?h₀.mk.mk.mk.hnc.a.n + (u - i)

case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ℕ

case h₀.mk.mk.mk.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ t = v - j
Tactic:
rw [Nat.add_sub_of_le hij'.1, ← hb''.2.1, hb''.1.1]
Proof state after:
case h₀.mk.mk.mk.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ t = v - j
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ t = v - j
Tactic:
apply Nat.add_left_cancel
Proof state after:
case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ?h₀.mk.mk.mk.hnc.a.n + t = ?h₀.mk.mk.mk.hnc.a.n + (v - j)

case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ℕ
Theorem: rewriting_4_fold_sums
Proof state before:
case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ?h₀.mk.mk.mk.hnc.a.n + t = ?h₀.mk.mk.mk.hnc.a.n + (v - j)

case h₀.mk.mk.mk.hnc.a.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
x y z t : ℕ
hb : i + j = m ∧ z + t = n
hb'' : (x + z = u ∧ y + t = v) ∧ x = i ∧ y = j
hb' : z = u - i → ¬t = v - j
⊢ ℕ
Tactic:
rw [Nat.add_sub_of_le hij'.2, ← hb''.2.2, hb''.1.2]
Proof state after:
no goals
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
⊢ ((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
Tactic:
intro hb
Proof state after:
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
hb : ((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
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
hb : ((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
Tactic:
rw [if_neg]
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
⊢ ¬((((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))
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
⊢ ¬((((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))
Tactic:
intro hb'
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, 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)
⊢ False
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, 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)
⊢ False
Tactic:
apply hb
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, 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)
⊢ ((i, j), u - i, v - j) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal 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, 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)
⊢ ((i, j), u - i, v - j) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
Tactic:
simp only [eq_self_iff_true, and_true_iff] at hb'
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
⊢ ((i, j), u - i, v - j) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal 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
⊢ ((i, j), u - i, v - j) ∈ Finset.antidiagonal m ×ˢ Finset.antidiagonal n
Tactic:
simp only [Finset.mem_product, Finset.mem_antidiagonal]
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
⊢ i + j = m ∧ u - i + (v - j) = n