English
The multiset antidiagonalTuple k n contains no duplicates.
Русский
Мультимножество antidiagonalTuple k n не содержит повторяющихся элементов.
LaTeX
$$$ List.Nodup (antidiagonalTuple k n) $$$
Lean4
/-- The antidiagonal of `n` does not contain duplicate entries. -/
theorem nodup_antidiagonalTuple (k n : ℕ) : List.Nodup (antidiagonalTuple k n) :=
by
induction k generalizing n with
| zero => cases n <;> simp
| succ k ih => ?_
simp_rw [antidiagonalTuple, List.nodup_flatMap]
constructor
· intro i _
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)
induction n with
| zero => exact List.pairwise_singleton _ _
| succ n n_ih =>
rw [List.Nat.antidiagonal_succ]
refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
· rw [List.mem_map] at hx₁ hx₂ ha
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
rw [Fin.cons_inj] at h
injection h.1
· rw [List.mem_map] at hx₁ hx₂
obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
dsimp at h₁₂
rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
obtain ⟨h₁₂, rfl⟩ := h₁₂
rw [Function.onFun, h₁₂] at h
exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)
