English
Let e be an equivalence between Option α and Option β. The auxiliary map removeNone_aux e: α → β has inverse removeNone_aux e.symm: β → α, and these compose to the identity on α; i.e., for all x ∈ α, removeNone_aux e.symm (removeNone_aux e (x)) = x.
Русский
Пусть e = α ↔ β является эквивиалентностью между Option α и Option β. Вспомогательное отображение removeNone_aux e: α → β имеет обратное removeNone_aux e.symm: β → α, и их композиция равна тождественной отображению на α; то есть для всякого x ∈ α выполнено removeNone_aux e.symm (removeNone_aux e x) = x.
LaTeX
$$$\forall e : \mathrm{Equiv}(\mathrm{Option}(\alpha), \mathrm{Option}(\beta)),\; (\mathrm{removeNone\_aux}\ e^{ -1}) \circ (\mathrm{removeNone\_aux}\ e) = \mathrm{id}_\alpha.$$$
Lean4
theorem removeNone_aux_inv (x : α) : removeNone_aux e.symm (removeNone_aux e x) = x :=
Option.some_injective _
(by
cases h1 : e.symm (some (removeNone_aux e x)) <;> cases h2 : e (some x)
· rw [removeNone_aux_none _ h1]
exact (e.eq_symm_apply.mpr h2).symm
· rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
simp at h1
· rw [removeNone_aux_none _ h2] at h1
simp at h1
· rw [removeNone_aux_some _ ⟨_, h1⟩]
rw [removeNone_aux_some _ ⟨_, h2⟩]
simp)
