append_insert — Mathlib

English

Inserting into a concatenation t + v at index i + m is compatible with appending after inserting into v: insert(a, t + v, i + m) = (t + insert(a,v,i)) with index adjustment.

Русский

Вставка элемента в конкатенацию t + v на индекс i + m согласуется с вставкой в v и последующим конкатенированием: insert(a, t + v, i + m) = t + insert(a,v,i) с поправкой по индексу.

LaTeX

$$$ \mathrm{insert}(a,(t \,+\, v), (i + m)) = \mathrm{insert}(a,t,v,i) \text{ after index adjustment (via } e). $$$

Lean4

theorem append_insert (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (n + 1)) (e : (n + 1) + m = (n + m) + 1) :
    insert a (t +-+ v) (Eq.recOn e (i.add m)) = Eq.recOn e (t +-+ insert a v i) :=
  by
  refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e
  · rfl
  have e' : (n + 1) + k = (n + k) + 1 := by omega
  change
    insert a (b :: t +-+ v) (Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (add i k))) =
      Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (b :: t +-+ insert a v i)
  rw [←
    (Eq.recOn e' rfl :
      fs (Eq.recOn e' (i.add k) : Fin2 ((n + k) + 1)) = Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (i.add k)))]
  simpa [IH] using Eq.recOn e' rfl

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