Theorem: Finset.sum_4_rw (DividedPowers/BasicLemmas.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)
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)
Tactic:
simp only [mem_sigma, mem_range, Nat.lt_succ_iff] at h
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)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ 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)

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)
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)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ 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)
Tactic:
simp only [Nat.add_sub_self_left a c, Nat.sub_sub,
  add_comm (a + c), ← add_assoc, Nat.sub_add_cancel h.1.2]
State after:
no goals