Theorem: rewriting_4_fold_sums (DividedPowers/BasicLemmas.lean)

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
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f
Tactic:
have hq :∀ x ∈ Finset.filter
  (fun x : (ℕ × ℕ) × ℕ × ℕ => x.fst.fst + x.snd.fst = u ∧ x.fst.snd + x.snd.snd = v)
    (Finset.antidiagonal m ×ˢ Finset.antidiagonal n),
  x.fst ∈ Finset.antidiagonal m := by
  intro x; simp; intro h'; simp [h']
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
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f

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
⊢ (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)).sum
      g =
    (Finset.antidiagonal m).sum f
Tactic:
rw [← Finset.sum_fiberwise_of_maps_to hq]
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
⊢ ∑ j ∈ Finset.antidiagonal m,
      ∑
        i ∈
          Finset.filter (fun i => i.1 = j)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
    (Finset.antidiagonal m).sum f

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
⊢ ∑ j ∈ Finset.antidiagonal m,
      ∑
        i ∈
          Finset.filter (fun i => i.1 = j)
            (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
              (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
        g i =
    (Finset.antidiagonal m).sum f
Tactic:
apply Finset.sum_congr rfl
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
⊢ ∀ x ∈ Finset.antidiagonal m,
    ∑
        i ∈
          Finset.filter (fun i => i.1 = 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)),
        g i =
      f x

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
⊢ ∀ x ∈ Finset.antidiagonal m,
    ∑
        i ∈
          Finset.filter (fun i => i.1 = 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)),
        g i =
      f x
Tactic:
rintro ⟨i, j⟩ hij
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) ∈ Finset.antidiagonal m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)

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) ∈ Finset.antidiagonal m
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Tactic:
simp only [Finset.mem_antidiagonal] at hij
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
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)

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
⊢ ∑
      i ∈
        Finset.filter (fun i_1 => i_1.1 = (i, j))
          (Finset.filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v)
            (Finset.antidiagonal m ×ˢ Finset.antidiagonal n)),
      g i =
    f (i, j)
Tactic:
rw [Finset.sum_filter]
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.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)

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

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

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

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

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'
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

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']
State after:
no goals

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

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

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

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

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⟩⟩ : (ℕ × ℕ) × ℕ × ℕ)]
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

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
⊢ (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
Tactic:
simp only [Nat.add_sub_of_le hij'.1, Nat.add_sub_of_le hij'.2, eq_self_iff_true, and_self_iff,
  if_true]
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
⊢ ∀ 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

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'
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

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

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''
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

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

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'
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

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''
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

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

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

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'
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

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
⊢ 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
Tactic:
apply Nat.add_left_cancel
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 + 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

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

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
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
⊢ ℕ

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]
State after:
no goals

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

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

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'
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

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

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'
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

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

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

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
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
⊢ ℕ

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

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

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

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

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
State after:
no goals

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

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]
State after:
no goals

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

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

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

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]
State after:
no goals

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]
State after:
no goals