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