-- Mathlib/Data/Finset/NatAntidiagonal.lean
@[simp] lemma antidiagonal_filter_le_snd_of_le {n k : ℕ} (h : k ≤ n) :
    (antidiagonal n).filter (fun a ↦ k ≤ a.snd) = (antidiagonal (n - k)).map
      (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective k⟩)

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
exact exists₂_congr (fun a b ↦ by rw [add_comm])

Result:
no goals

Proof state:
case h.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
i j : ℕ
⊢ (i, j) ∈
      map (({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
        (antidiagonal (n - k)) ↔
    (i, j) ∈ map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
simpa using aux₂ i j

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
rw [exists_comm]

Result:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.2) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]

Result:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map (({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
      (antidiagonal (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => k ≤ a.2) (antidiagonal n) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                    ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
  fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])

Result:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.2) (antidiagonal n) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map (({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
      (antidiagonal (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
ext ⟨i, j⟩

Result:
case h.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
i j : ℕ
⊢ (i, j) ∈
      map (({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
        (antidiagonal (n - k)) ↔
    (i, j) ∈ map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Proof state:
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.2) (antidiagonal n) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl

Result:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => k ≤ a.2) (antidiagonal n) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Proof state:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.2) (antidiagonal n) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
rw [← map_prodComm_antidiagonal]

Result:
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.2) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))