English
If j is a Fin n index, then the value of the inserted tuple at i.succAbove(j) equals p(j).
Русский
Если j ∈ Fin n, то значение вставленного кортежа в позиции i.succAbove(j) равно p(j).
LaTeX
$$$(insertNth\ i\ x\ p)(i.\\succAbove j) = p j.$$$
Lean4
@[simp]
theorem insertNth_apply_succAbove (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j)) (j : Fin n) :
insertNth i x p (i.succAbove j) = p j :=
by
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]
split_ifs with hlt
· generalize_proofs H₁ H₂; revert H₂
generalize hk : castPred ((succAbove i) j) H₁ = k
rw [castPred_succAbove _ _ hlt] at hk; cases hk
intro; rfl
· generalize_proofs H₀ H₁ H₂; revert H₂
generalize hk : pred (succAbove i j) H₁ = k
rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
intro; rfl
