English
Elimination with a patched function distributes over updating the argument function: elim' f (update g a x) equals update (elim' f g) (some a) x.
Русский
Элиминация с обновлением распределяется над обновлением функции: elim' f (update g a x) = update (elim' f g) (some a) x.
LaTeX
$$$ \mathrm{Option.elim}' f (\mathrm{update}\ g\ a\ x) = \mathrm{update}\ (\mathrm{Option.elim}' f\ g)\ (\mathrm{some}\ a)\ x $$$
Lean4
@[simp]
theorem elim'_update {α : Type*} {β : Type*} [DecidableEq α] (f : β) (g : α → β) (a : α) (x : β) :
Option.elim' f (update g a x) = update (Option.elim' f g) (some a) x :=
-- Can't reuse `Option.rec_update` as `Option.elim'` is not defeq.
Function.rec_update (α := fun _ => β) (@Option.some.inj _) (Option.elim' f) (fun _ _ => rfl)
(fun
| _, _, some _, h => (h _ rfl).elim
| _, _, none, _ => rfl)
_ _ _
