English
The keys of kreplace do not depend on the replacement: (kreplace a b l).keys = l.keys.
Русский
Ключи у kreplace не зависят от замены: (kreplace a b l).keys = l.keys.
LaTeX
$$$ (\mathrm{kreplace}(a,b,l)).keys = l.keys $$$
Lean4
theorem keys_kreplace (a : α) (b : β a) : ∀ l : List (Sigma β), (kreplace a b l).keys = l.keys :=
lookmap_map_eq _ _ <| by
rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩
dsimp
split_ifs with h <;> simp +contextual [h]