English
For any permutation σ of Option α, the extension of removeNone(σ) equals the product of swapping none with σ(none) and σ's action extended to α.
Русский
Для любой перестановки σ над Option α продолжение removeNone(σ) равно произведению перестановки, которая меняет none с σ(none), и действия σ, расширенного до α.
LaTeX
$$$ (\\mathrm{removeNone}\\, σ).\\mathrm{optionCongr} = \\mathrm{swap}\\, none\\ (σ\\ none) * σ $$$
Lean4
@[simp]
theorem map_equiv_removeNone {α : Type*} [DecidableEq α] (σ : Perm (Option α)) :
(removeNone σ).optionCongr = swap none (σ none) * σ :=
by
ext1 x
have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) :=
by
obtain - | x := x
· simp
· cases h : σ (some _)
· simp [removeNone_none _ h]
· have hn : σ (some x) ≠ none := by simp [h]
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
simpa using this
