insertNth_apply_above — Mathlib

English

If i < j, then (insertNth i x p) j equals p(j.pred) (with a suitable cast).

Русский

Если i < j, то (insertNth i x p) j равно p(j.pred) с подходящим приведением типа.

LaTeX

$$If {h: i < j}, (insertNth i x p) j = succAbove_pred_of_lt _ _ h ▸ (p <| j.pred _)$$

Lean4

theorem insertNth_apply_above {i j : Fin (n + 1)} (h : i < j) (x : α i) (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = succAbove_pred_of_lt _ _ h ▸ (p <| j.pred _) := by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

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