English
Filling and then filtering by removing a given a yields the original tail part.
Русский
Заполнение и последующая фильтрация по удалению заданного элемента возвращает исходный хвост.
LaTeX
$$$\\mathrm{fill}(a,\\cdot)\\circ \\mathrm{filterNe}(a) = \\text{identity on tail}$$$
Lean4
theorem filter_ne_fill [DecidableEq α] (a : α) (m : Σ i : Fin (n + 1), Sym α (n - i)) (h : a ∉ m.2) :
(m.2.fill a m.1).filterNe a = m :=
sigma_sub_ext
(by
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
rw [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]
· intro b hb
rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
exact hb.2 hb.1.2.symm
· exact fun a ha ha' => h <| ha'.symm ▸ ha)
