English
For Fin n, the image under i.succAbove of i.cycleRange j is the transposition swapping 0 with i.succ and j.succ.
Русский
Для Fin n образ через i.succAbove от i.cycleRange j даёт перестановку swap(0, i.succ, j.succ).
LaTeX
$$$i.succ.succAbove\big(i.cycleRange(j)\big) = \operatorname{swap}(0, i.succ, j.succ)$$$
Lean4
@[simp]
theorem succAbove_cycleRange (i j : Fin n) : i.succ.succAbove (i.cycleRange j) = swap 0 i.succ j.succ :=
by
cases n
· rcases j with ⟨_, ⟨⟩⟩
rcases lt_trichotomy j i with (hlt | heq | hgt)
· have : castSucc (j + 1) = j.succ := by
ext
rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]
· apply Fin.succ_ne_zero
· exact (Fin.succ_injective _).ne hlt.ne
· rw [Fin.lt_iff_val_lt_val]
simpa [this] using hlt
· rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]
· rw [Fin.castSucc_zero]
apply Fin.succ_pos
· rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
· apply Fin.succ_ne_zero
· apply (Fin.succ_injective _).ne hgt.ne.symm
· simpa [Fin.le_iff_val_le_val] using hgt
