English
If x is not in t, then inserting x into t yields a Finset insert x t. The elements of insert x t are either x itself or elements of t. This yields a canonical bijection between the elements of insert x t and the option type containing elements of t, i.e., an equivalence between Subtype (i ∈ insert x t) and Option (Subtype (i ∈ t)).
Русский
Если x не принадлежит t, то вставка x в t образует множество insert x t. Элементы insert x t либо равны x, либо принадлежат t. Это даёт каноническое биекцию между подмножеством элементов insert x t и опциональным множеством элементов t.
LaTeX
$$$\\{ i \\mid i \\in \\operatorname{insert} x t\\} \\cong \\operatorname{Option}\\{ i \\mid i \\in t\\}.$$$
Lean4
/-- Inserting an element to a finite set is equivalent to the option type. -/
def subtypeInsertEquivOption {t : Finset α} {x : α} (h : x ∉ t) : { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
where
toFun y := if h : ↑y = x then none else some ⟨y, (mem_insert.mp y.2).resolve_left h⟩
invFun y := (y.elim ⟨x, mem_insert_self _ _⟩) fun z => ⟨z, mem_insert_of_mem z.2⟩
left_inv y := by grind
right_inv := by rintro (_ | y) <;> grind
