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