English
Filling an m by i copies of a yields a Sym term equal to m appended with i copies of a, adjusted by a cast.
Русский
Заполнение m копиями a даёт Sym-терм, равный m, дополненному i копиями a и приведённому приведение.
LaTeX
$$$\\mathrm{fill}(a,i,m) = \\mathrm{cast}(\\mathrm{sub}) (m \\append \\mathrm{replicate}(i,a))$$$
Lean4
theorem fill_filterNe [DecidableEq α] (a : α) (m : Sym α n) : (m.filterNe a).2.fill a (m.filterNe a).1 = m :=
Sym.ext
(by
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
ext b; dsimp
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
obtain rfl | h := eq_or_ne a b
· rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
· rw [if_pos h, if_neg h, add_zero])
