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

State before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ (∑ x ∈ antidiagonal n,
      match x with
      | (k, l) =>
        ∑ x ∈ antidiagonal k,
          match x with
          | (a, b) =>
            ∑ x ∈ antidiagonal l,
              match x with
              | (c, d) => f (a, b, c, d)) =
    ∑ x ∈ antidiagonal n,
      match x with
      | (k, l) =>
        ∑ x ∈ antidiagonal k,
          match x with
          | (a, c) =>
            ∑ x ∈ antidiagonal l,
              match x with
              | (b, d) => f (a, b, c, d)
Tactic:
simp only [Finset.sum_sigma']
State after:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ 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)

State before:
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
⊢ ∑ 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:
set φ : ((_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ) → ((_ : ℕ × ℕ) × (_ : ℕ × ℕ) × ℕ × ℕ) :=
  fun ⟨⟨_, _⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ ↦ ⟨⟨a+c, b+ d⟩, ⟨⟨a, c⟩, ⟨b, d⟩⟩⟩
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)⟩⟩
⊢ ∑ 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)

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)⟩⟩
⊢ ∑ 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
  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 ⊢
  rintro ⟨⟨k, l⟩, ⟨⟨a, b⟩, ⟨c, d⟩⟩⟩ H
  simp only [mem_sigma, mem_antidiagonal] at H ⊢
  simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_eq_eq, and_true, φ, H.2.1, H.2.2]
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)⟩⟩
⊢ ∀ (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

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

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

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

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

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

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

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

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

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

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

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