internlm/Lean-Github huggingface dataset:
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
⊢ ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
Tactic:
rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ (fun m x => φ m) ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ H ∈
    (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ (fun m x => φ m) ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ H ∈
    (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
Tactic:
simp only [mem_sigma, mem_antidiagonal, and_self, and_true] at H ⊢
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ a + c + (b + d) = n
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ a + c + (b + d) = n
Tactic:
rw [← H.1, ← H.2.1, ← H.2.2]
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ a + c + (b + d) = a + b + (c + d)
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ a + c + (b + d) = a + b + (c + d)
Tactic:
abel
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
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ : ?m.15077
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Tactic:
suffices hφ' : _ by
  apply Finset.sum_bij' (fun m _ => φ m) (fun m _ => φ m) hφ hφ hφ' hφ'
  rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
  simp only [mem_sigma, mem_antidiagonal] at H ⊢
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
Tactic:
rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ H) ⋯ = ⟨(k, l), ⟨(a, b), (c, d)⟩⟩
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ (fun m x => φ m) ((fun m x => φ m) ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ H) ⋯ = ⟨(k, l), ⟨(a, b), (c, d)⟩⟩
Tactic:
simp only [mem_sigma, mem_antidiagonal] at H ⊢
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ φ (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩) = ⟨(k, l), ⟨(a, b), (c, d)⟩⟩
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
k l a b c d : ℕ
H : k + l = n ∧ a + b = k ∧ c + d = l
⊢ φ (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩) = ⟨(k, l), ⟨(a, b), (c, d)⟩⟩
Tactic:
simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_eq_eq, and_true, φ, H.2.1, H.2.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
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ : ?m.15077
hφ' : ?m.15083
⊢ ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.fst.2, x.snd.snd.1, x.snd.snd.2) =
    ∑ x ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
      f (x.snd.fst.1, x.snd.snd.1, x.snd.fst.2, x.snd.snd.2)
Tactic:
apply Finset.sum_bij' (fun m _ => φ m) (fun m _ => φ m) hφ hφ hφ' hφ'
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
hφ' :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
⊢ ∀ a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
    f (a.snd.fst.1, a.snd.fst.2, a.snd.snd.1, a.snd.snd.2) =
      f ((φ a).snd.fst.1, (φ a).snd.snd.1, (φ a).snd.fst.2, (φ a).snd.snd.2)
Theorem: Finset.sum_4_rw'
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
hφ' :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
⊢ ∀ a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2,
    f (a.snd.fst.1, a.snd.fst.2, a.snd.snd.1, a.snd.snd.2) =
      f ((φ a).snd.fst.1, (φ a).snd.snd.1, (φ a).snd.fst.2, (φ a).snd.snd.2)
Tactic:
rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
Proof state after:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
hφ' :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ f
      (⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.fst.1, ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.fst.2, ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.snd.1,
        ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.snd.2) =
    f
      ((φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.fst.1, (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.snd.1,
        (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.fst.2, (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.snd.2)
Theorem: Finset.sum_4_rw'
Proof state before:
case mk.mk.mk.mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ → (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ :=
  fun x =>
    match x with
    | ⟨(fst, snd), ⟨(a, b), (c, d)⟩⟩ => ⟨(a + c, b + d), ⟨(a, c), (b, d)⟩⟩
hφ :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) a ha ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
hφ' :
  ∀ (a : (_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ)
    (ha : a ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2),
    (fun m x => φ m) ((fun m x => φ m) a ha) ⋯ = a
k l a b c d : ℕ
H : ⟨(k, l), ⟨(a, b), (c, d)⟩⟩ ∈ (antidiagonal n).sigma fun a => (antidiagonal a.1).sigma fun a_1 => antidiagonal a.2
⊢ f
      (⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.fst.1, ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.fst.2, ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.snd.1,
        ⟨(k, l), ⟨(a, b), (c, d)⟩⟩.snd.snd.2) =
    f
      ((φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.fst.1, (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.snd.1,
        (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.fst.2, (φ ⟨(k, l), ⟨(a, b), (c, d)⟩⟩).snd.snd.2)
Tactic:
simp only [mem_sigma, mem_antidiagonal] at H ⊢
Proof state after:
no goals
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ k ∈ range (n + 1), ∑ a ∈ range (k + 1), ∑ c ∈ range (n - k + 1), f (a, k - a, c, n - k - c) =
    ∑ l ∈ range (n + 1), ∑ a ∈ range (l + 1), ∑ b ∈ range (n - l + 1), f (a, b, l - a, n - l - b)
Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma', Finset.sum_sigma', Finset.sum_sigma']
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
Theorem: Finset.sum_4_rw
Proof state before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
Tactic:
let φ : (Σ (_ : Σ (_ : ℕ), ℕ), ℕ) → (Σ (_ : Σ (_ : ℕ), ℕ), ℕ) :=
  fun ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
Proof state after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
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)
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
Tactic:
have h2 : ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ) (ha : a ∈ Finset.sigma (Finset.sigma (range (n + 1))
    fun k => range (k + 1)) fun x => range (n - x.fst + 1)),
    (fun m _ => φ m) ((fun m _ => φ m) a ha) ((fun m _ => φ m) a ha ∈
      Finset.sigma (Finset.sigma (range (n + 1)) fun k => range (k + 1))
        fun x => range (n - x.fst + 1)) =
  a := by
  rintro ⟨⟨k, a⟩, c⟩ h
  simp only [Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff] at h
  rw [Sigma.mk.inj_iff]
  simp only [Sigma.mk.inj_iff, heq_eq_eq, and_true, add_tsub_cancel_left]
  refine add_tsub_cancel_of_le h.1.2
Proof state after:
α : 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
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
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
⊢ ∑ x ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.fst.fst - x.fst.snd, x.snd, n - x.fst.fst - x.snd) =
    ∑ x ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1),
      f (x.fst.snd, x.snd, x.fst.fst - x.fst.snd, n - x.fst.fst - x.snd)
Tactic:
refine Finset.sum_bij' (fun m _ => φ m) (fun m _ => φ m) h1 h1 h2 h2 ?_
Proof state after:
α : 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)
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⟩
⊢ ∀ (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)
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⟩
c k a : ℕ
h : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)
⊢ (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)
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)
⊢ (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)
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⟩
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
⊢ (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)
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
⊢ (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)
Tactic:
simp_rw [Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_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⟩
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)