English
For e : α ≃ β, removeNone e.optionCongr = e; equivalently, the action of lifting an equivalence on α ≃ β to Option α ≃ Option β and then removing the None returns the original equivalence.
Русский
Для эвиалентности e: α ≃ β, removeNone e.optionCongr = e; то есть операция подъема эквивалентности на α → β до Option α ≃ Option β и последующее удаление None возвращает исходную эквивалентность.
LaTeX
$$$\mathrm{removeNone}(e\mathrm{.optionCongr}) = e.$$$
Lean4
theorem some_removeNone_iff {x : α} : some (removeNone e x) = e none ↔ e.symm none = some x :=
by
rcases h : e (some x) with a | a
· rw [removeNone_none _ h]
simpa using (congr_arg e.symm h).symm
· rw [removeNone_some _ ⟨a, h⟩]
have h1 := congr_arg e.symm h
rw [symm_apply_apply] at h1
simp only [apply_eq_iff_eq, reduceCtorEq]
simp [h1]
