English
For n, k with k ≤ n, the set {a ∈ antidiagonal n | a.fst ≤ k} equals the image of antidiagonal k under an embedding adjusting coordinates.
Русский
Для n, k с k ≤ n множество {a ∈ antidiagonal n | a.fst ≤ k} тождественно отображается как образ antidiagonal(k) под соответствующим вложением.
LaTeX
$$$\\{a \\in \\operatorname{antidiagonal}(n) \\mid a.\\mathrm{fst} \\le k\\} = \\operatorname{antidiagonal}(k).map (\\mathrm{Embedding.prodMap} \\langle _, \\mathrm{add\\_left\\_injective}(n-k)\\rangle (\\mathrm{Embedding.refl} \\mathbb{N}))$$$
Lean4
@[simp]
theorem antidiagonal_filter_fst_le_of_le {n k : ℕ} (h : k ≤ n) :
{a ∈ antidiagonal n | a.fst ≤ k} =
(antidiagonal k).map (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective (n - k)⟩) :=
by
have aux₁ : (fun a ↦ a.fst ≤ k) = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
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])
rw [← map_prodComm_antidiagonal]
simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
ext ⟨i, j⟩
simpa using aux₂ i j
