kreplace_self — Mathlib

English

If l has NodupKeys and l contains ⟨a,b⟩, then kreplace a b l = l.

Русский

Если l имеет NodupKeys и содержит ⟨a,b⟩, то kreplace a b l = l.

LaTeX

$$$ \text{nd} : l.NodupKeys \Rightarrow \ \mathrm{kreplace}(a,b,l) = l $$$

Lean4

theorem kreplace_self {a : α} {b : β a} {l : List (Sigma β)} (nd : NodupKeys l) (h : Sigma.mk a b ∈ l) :
    kreplace a b l = l :=
  by
  refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)
  · rintro ⟨a', b'⟩ h'
    dsimp [Option.guard]
    split_ifs
    · subst a'
      simp [nd.eq_of_mk_mem h h']
    · simp_all
    · simp_all
    · rfl
  · simp

Похожие утверждения