removeNth_removeNth_heq_swap — Mathlib

English

The two-step removals commute up to heterogeneous equality when tracked over indices.

Русский

Два последовательных удаления совпадают, если учитывать гетеро-равенства между индексами.

LaTeX

$$$$ i.removeNth (j.removeNth m) \equiv_{HEq} (i.predAbove j).removeNth ((j.succAbove i).removeNth m) $$$$

Lean4

/-- A `HEq` version of `Fin.removeNth_removeNth_eq_swap`. -/
theorem removeNth_removeNth_heq_swap {α : Fin (n + 2) → Sort*} (m : ∀ i, α i) (i : Fin (n + 1)) (j : Fin (n + 2)) :
    i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) :=
  by
  apply Function.hfunext rfl
  simp only [heq_iff_eq]
  rintro k _ rfl
  unfold removeNth
  apply congr_arg_heq
  rw [succAbove_succAbove_succAbove_predAbove]

Похожие утверждения