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

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

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

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

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

Tactic:
rw [← map_prodComm_antidiagonal]

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

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

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

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

Tactic:
simpa using aux₂ i j

Result:
no goals

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

Tactic:
ext ⟨i, j⟩

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

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

Tactic:
rw [exists_comm]

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

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

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

Result:
no goals

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

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

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

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

Tactic:
rw [add_comm]

Result:
no goals