English
Extending a swap on α to Option α via optionCongr yields the corresponding swap on the Some-values, with none fixed.
Русский
Расширение перестановки-обмена (swap x y) на α до Option α через optionCongr даёт соответствующую перестановку-обмен для значений типа Some, а none фиксируется.
LaTeX
$$$ \\forall x,y \\in \\alpha: \\; \\mathrm{optionCongr}(\\mathrm{swap}\\ x\\ y) = \\mathrm{swap}(\\mathrm{some}\\ x)(\\mathrm{some}\\ y) $$$
Lean4
@[simp]
theorem optionCongr_swap {α : Type*} [DecidableEq α] (x y : α) : optionCongr (swap x y) = swap (some x) (some y) :=
by
ext (_ | i)
· simp [swap_apply_of_ne_of_ne]
· by_cases hx : i = x
· simp only [hx, optionCongr_apply, Option.map_some, swap_apply_left, Option.some.injEq]
by_cases hy : i = y <;> simp [hx, hy, swap_apply_of_ne_of_ne]
