append_cast_right — Mathlib

English

For xs : Fin n → α, ys : Fin m → α, m' : ℕ and h : m' = m, append xs (ys ∘ cast h) = append xs ys ∘ (Fin.cast (by rw [h])).

Русский

Для xs : Fin n → α, ys : Fin m → α и h : m' = m, выполняется append xs (ys ∘ cast h) = append xs ys ∘ cast (по доказательству).

LaTeX

$$$\\mathrm{append}(xs,\\, ys \\circ \\mathrm{Fin.cast}\\, h) = \\mathrm{append}(xs, ys) \\circ \\mathrm{Fin.cast}(\\mathrm{by rw [h]}).$$$

Lean4

@[simp]
theorem append_cast_right {n m} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ) (h : m' = m) :
    Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ (Fin.cast <| by rw [h]) := by subst h; simp

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