internlm/Lean-Github huggingface dataset:
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ (a + c ≤ n ∧ a ≤ a + c) ∧ k - a ≤ n - (a + c)
Tactic:
constructor
Proof state after:
case mk.mk.left
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + c ≤ n ∧ a ≤ a + c

case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (a + c)
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.left
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + c ≤ n ∧ a ≤ a + c

case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (a + c)
Tactic:
constructor
Proof state after:
case mk.mk.left.left
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + c ≤ n

case mk.mk.left.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a ≤ a + c

case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (a + c)
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.left.left
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + c ≤ n
Tactic:
apply le_trans (add_le_add h.1.2 h.2) _
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k + (n - k) ≤ n
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k + (n - k) ≤ n
Tactic:
rw [add_comm]
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ n - k + k ≤ n
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ n - k + k ≤ n
Tactic:
rw [Nat.sub_add_cancel h.1.1]
Proof state after:
no goals
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.left.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a ≤ a + c
Tactic:
exact le_self_add
Proof state after:
no goals
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (a + c)
Tactic:
rw [add_comm a c]
Proof state after:
case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (c + a)
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - (c + a)
Tactic:
rw [← Nat.sub_sub n c a]
Proof state after:
case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - c - a
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k - a ≤ n - c - a
Tactic:
apply Nat.sub_le_sub_right
Proof state after:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k ≤ n - c
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k ≤ n - c
Tactic:
rw [Nat.le_sub_iff_add_le]
Proof state after:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k + c ≤ n

case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ k + c ≤ n

case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Tactic:
rw [Nat.le_sub_iff_add_le h.1.1, add_comm] at h
Proof state after:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ k + c ≤ n
⊢ k + c ≤ n

case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ k + c ≤ n
⊢ k + c ≤ n

case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Tactic:
exact h.2
Proof state after:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk.right.h
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ c ≤ n
Tactic:
exact le_trans h.2 (Nat.sub_le n k)
Proof state after:
no goals
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
⊢ ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
Tactic:
rintro ⟨⟨k, a⟩, c⟩ h
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h)
      ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h ∈
        ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
    ⟨⟨k, a⟩, c⟩
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h)
      ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h ∈
        ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
    ⟨⟨k, a⟩, c⟩
Tactic:
simp only [Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff] at h
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝)
      ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝ ∈
        ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
    ⟨⟨k, a⟩, c⟩
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝)
      ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝ ∈
        ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
    ⟨⟨k, a⟩, c⟩
Tactic:
rw [Sigma.mk.inj_iff]
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ ⟨a + (k - a), a⟩ = ⟨k, a⟩ ∧ HEq (a + c - a) c
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ ⟨a + (k - a), a⟩ = ⟨k, a⟩ ∧ HEq (a + c - a) c
Tactic:
simp only [Sigma.mk.inj_iff, heq_eq_eq, and_true, add_tsub_cancel_left]
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + (k - a) = k
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ a + (k - a) = k
Tactic:
refine add_tsub_cancel_of_le h.1.2
Proof state after:
no goals
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h2 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
⊢ ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    f (a.fst.snd, a.fst.fst - a.fst.snd, a.snd, n - a.fst.fst - a.snd) =
      f
        (((fun m x => φ m) a ha).fst.snd, ((fun m x => φ m) a ha).snd,
          ((fun m x => φ m) a ha).fst.fst - ((fun m x => φ m) a ha).fst.snd,
          n - ((fun m x => φ m) a ha).fst.fst - ((fun m x => φ m) a ha).snd)
Tactic:
rintro ⟨⟨k, a⟩, c⟩ h
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h2 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
c k a : ℕ
h : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
⊢ f
      (⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.snd,
        n - ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.snd) =
    f
      (((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.snd, ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).snd,
        ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.snd,
        n - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).snd)