English
For n, k with k ≤ n, the set {a ∈ antidiagonal n | k ≤ a.fst} equals the image of antidiagonal (n-k) under an embedding adjusting coordinates.
Русский
Для n, k с k ≤ n множество {a ∈ antidiagonal n | k ≤ a.fst} равно образ antidiagonal(n-k) через вложение, подгоняющее координаты.
LaTeX
$$$\\{a \\in \\operatorname{antidiagonal}(n) \\mid k \\le a.\\mathrm{fst}\\} = \\operatorname{antidiagonal}(n-k).map (\\mathrm{Embedding.prodMap} \\langle _, \\mathrm{add\\_left\\_injective} k\\rangle (\\mathrm{Embedding.refl} \\mathbb{N}))$$$
Lean4
@[simp]
theorem antidiagonal_filter_le_fst_of_le {n k : ℕ} (h : k ≤ n) :
{a ∈ antidiagonal n | k ≤ a.fst} =
(antidiagonal (n - k)).map (Embedding.prodMap ⟨_, add_left_injective k⟩ (Embedding.refl ℕ)) :=
by
ext ⟨i, j⟩
suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
· rw [← Nat.sub_add_comm hi.2, hi.1]
· rintro ⟨l, hl, rfl⟩
refine ⟨?_, Nat.le_add_left k l⟩
rw [add_right_comm, hl]
exact tsub_add_cancel_of_le h
