English
The eliminator for toOption obeys a conditional: a.toOption.elim b f equals f(a.get h) if a has a defined element, otherwise equals b.
Русский
Элиминация toOption удовлетворяет условию: a.toOption.elim b f равняется f(a.get h) при наличии элемента, иначе b.
LaTeX
$$$a.toOption.elim b f = \\begin{cases} f(a.get h), & \\text{if } a.Dom, \\\\ b, & \\text{otherwise} \\end{cases}$$$
Lean4
@[simp]
theorem elim_toOption {α β : Type*} (a : Part α) [Decidable a.Dom] (b : β) (f : α → β) :
a.toOption.elim b f = if h : a.Dom then f (a.get h) else b :=
by
split_ifs with h
· rw [h.toOption]
rfl
· rw [Part.toOption_eq_none_iff.2 h]
rfl
