English
A higher-level swap identity for two holes in Fin(n+2) matches the two-hole swap above.
Русский
Идентичность перестановки двух дыр в Fin(n+2) согласуется со свопом двух дыр выше.
LaTeX
$$$\forall n:\mathbb{N},\forall i:\mathrm{Fin}(n+2),\forall j:\mathrm{Fin}(n+1),\forall k:\mathrm{Fin}(n),\ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)$$$
Lean4
/-- Given `i : Fin (n + 2)` and `j : Fin (n + 1)`,
there are two ways to represent the order embedding `Fin n → Fin (n + 2)`
leaving holes at `i` and `i.succAbove j`.
One is `i.succAbove ∘ j.succAbove`.
It corresponds to embedding `Fin n` to `Fin (n + 1)` leaving a hole at `j`,
then embedding the result to `Fin (n + 2)` leaving a hole at `i`.
The other one is `(i.succAbove j).succAbove ∘ (j.predAbove i).succAbove`.
It corresponds to swapping the roles of `i` and `j`.
This lemma says that these two ways are equal.
It is used in `Fin.removeNth_removeNth_eq_swap`
to show that two ways of removing 2 elements from a sequence give the same answer.
-/
theorem succAbove_succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n) :
(i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k) := by
/- While it is possible to give a "morally correct" proof
by saying that both functions are strictly monotone and have the same range `{i, i.succAbove j}ᶜ`,
we give a direct proof by case analysis to avoid extra dependencies. -/
ext
simp? [succAbove, predAbove, lt_def, apply_dite Fin.val, apply_ite Fin.val] says
simp only [succAbove, predAbove, lt_def, coe_castSucc, apply_dite Fin.val, coe_pred, coe_castPred, dite_eq_ite,
apply_ite Fin.val, val_succ]
split_ifs <;> omega
