English
For p : α → Prop, swapping two elements in a subtype corresponds to swapping their images in the ambient type.
Русский
Для p : α → Prop, перестановка двух элементов в подпорядке соответствует перестановке их образов в исходном типе.
LaTeX
$$$$ \operatorname{ofSubtype}(\mathrm{swap}(x,y)) = \mathrm{swap}(\,x\, ,\,y\) $$ where x,y : Subtype p.$$
Lean4
@[simp]
theorem ofSubtype_swap_eq {p : α → Prop} [DecidablePred p] (x y : Subtype p) :
ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y :=
Equiv.ext fun z => by
by_cases hz : p z
· rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]
split_ifs with hzx hzy
· simp_rw [hzx, Subtype.coe_eta, swap_apply_left]
· simp_rw [hzy, Subtype.coe_eta, swap_apply_right]
· rw [swap_apply_of_ne_of_ne] <;> simp [Subtype.ext_iff, *]
· rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne] <;> grind
