English
Two Sigma elements are equal if their second components (the tails) are equal as multisets and the first components agree by the Fin-index equality.
Русский
Два элемента в сумме равны, если их вторые компоненты (хвосты) равны как множества и первые компоненты согласованы по индексу Fin.
LaTeX
$$Sigma.subtype_ext with Fin.ext ensures equality from tail equality$$
Lean4
/-- Remove every `a` from a given `Sym α n`.
Yields the number of copies `i` and a term of `Sym α (n - i)`. -/
def filterNe [DecidableEq α] (a : α) (m : Sym α n) : Σ i : Fin (n + 1), Sym α (n - i) :=
⟨⟨m.1.count a, (count_le_card _ _).trans_lt <| by rw [m.2, Nat.lt_succ_iff]⟩, m.1.filter (a ≠ ·),
Nat.eq_sub_of_add_eq <|
Eq.trans
(by
rw [← countP_eq_card_filter, add_comm]
simp only [eq_comm, Ne, count]
rw [← card_eq_countP_add_countP _ _])
m.2⟩
