English
For any a and Finset s, the attach of insert a s equals an insertion of the pair (a, proof) into the image of s, where the proof component records membership of a in insert a s, and the images of s are adjusted accordingly.
Русский
Для любого элемента a и множества s, attach (insert a s) равен вставке пары (a, доказательство) в образ s через attach, при этом образ элементов s пересчитывается с учётом принадлежности a к insert a s.
LaTeX
$$$\\operatorname{attach}(\\operatorname{insert} a\\, s) = \\operatorname{insert} (\\langle a, \\operatorname{mem\\_insert\\_self}\\ a\\ s\\rangle) ((\\operatorname{attach} s).image (\\lambda x, \\langle x.1, \\operatorname{mem\\_insert\\_of\\_mem} x.2\\rangle))$$$
Lean4
@[simp]
theorem attach_insert [DecidableEq α] {a : α} {s : Finset α} :
attach (insert a s) =
insert (⟨a, mem_insert_self a s⟩ : { x // x ∈ insert a s })
((attach s).image fun x => ⟨x.1, mem_insert_of_mem x.2⟩) :=
ext fun ⟨x, hx⟩ =>
⟨Or.casesOn (mem_insert.1 hx) (fun h : x = a => fun _ => mem_insert.2 <| Or.inl <| Subtype.eq h) fun h : x ∈ s =>
fun _ => mem_insert_of_mem <| mem_image.2 <| ⟨⟨x, h⟩, mem_attach _ _, Subtype.eq rfl⟩,
fun _ => Finset.mem_attach _ _⟩
