English
The right-side sum-congruence with swapping on the right component equals swapping on the right injections.
Русский
Правая сумма-конгруэнтность с перестановкой на правой компоненте равна перестановке на правых инъекциях.
LaTeX
$$$\mathrm{Equiv}.\mathrm{Perm}.\mathrm{sumCongr}(\mathrm{Equiv}.\mathrm{refl} \ alpha)(\mathrm{Equiv}.\mathrm{swap} \ i \ j) = \mathrm{Equiv}.\mathrm{swap}(\mathrm{Sum}.\mathrm{inr} \ i)(\mathrm{Sum}.\mathrm{inr} \ j)$$$
Lean4
@[simp]
theorem sumCongr_refl_swap {α β : Sort _} [DecidableEq α] [DecidableEq β] (i j : β) :
Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j) :=
by
ext x
cases x
· simp [Sum.map, swap_apply_of_ne_of_ne]
· simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp_id, Sum.elim_inr, comp_apply, swap_apply_def,
Sum.inr.injEq]
split_ifs <;> rfl
