Coordinate laws for successive block splitting

The index equivalence puts each first coordinate immediately before its second coordinate. Splitting a head pair therefore prepends two coordinates to the split tail, with only the equality of the tuple lengths transported.

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockIndexEquiv_val {t : ℕ} (i : Fin t) (j : Fin 2) : ↑((splitBlockIndexEquiv t) (i, j)) = ↑j + 2 * ↑i

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockEquiv_apply {α : Type u_1} {t : ℕ} (x : Fin t → α × α) (i : Fin t) (j : Fin 2) : (splitBlockEquiv α t) x ((splitBlockIndexEquiv t) (i, j)) = (finTwoArrowEquiv α).symm (x i) j

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockEquiv_apply_fst {α : Type u_1} {t : ℕ} (x : Fin t → α × α) (i : Fin t) : (splitBlockEquiv α t) x ((splitBlockIndexEquiv t) (i, 0)) = (x i).1

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockEquiv_apply_snd {α : Type u_1} {t : ℕ} (x : Fin t → α × α) (i : Fin t) : (splitBlockEquiv α t) x ((splitBlockIndexEquiv t) (i, 1)) = (x i).2

theorem Algebraic.Cutwidth.Extractor.Internal.pairPrependEquiv_apply {α : Type u_1} {t : ℕ} (ab : α × α) (z : Fin t → α) : (pairPrependEquiv α t) (ab, z) = Fin.cons ab.1 (Fin.cons ab.2 z)

theorem Algebraic.Cutwidth.Extractor.Internal.pairPrependEquiv_symm_apply {α : Type u_1} {t : ℕ} (x : Fin (t + 2) → α) : (pairPrependEquiv α t).symm x = ((x 0, x 1), Fin.tail (Fin.tail x))

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockIndexEquiv_succ_cast {t : ℕ} (i : Fin t) (j : Fin 2) : Fin.cast ⋯ ((splitBlockIndexEquiv (t + 1)) (i.succ, j)) = ((splitBlockIndexEquiv t) (i, j)).succ.succ

theorem Algebraic.Cutwidth.Extractor.Internal.splitBlockEquiv_cons {α : Type u_1} {t : ℕ} (ab : α × α) (z : Fin t → α × α) : (splitBlockEquiv α (t + 1)) (Fin.cons ab z) = fun (i : Fin (2 * t.succ)) => (pairPrependEquiv α (2 * t)) (ab, (splitBlockEquiv α t) z) (Fin.cast ⋯ i)