A vertex's odd list, as a multiset

The odd list at a vertex is built by walking the flags there and recording each one's per-flag odd value. Read as a multiset it is simply the image of those flags under that value, with the walking order forgotten — the form in which two orientations' lists can be compared, since only the order distinguishes them.

Helper: bind of a two-element function splits into two maps

The attachWith–sort multiset equals the finset filter val

theorem RS.attachWith_sort_eq_filter_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) (v : W.Vertex) : ↑((F.inFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.flags) ⋯) = {f : ↥F.flags | W.attach ↑f = Sum.inl v ∧ o.isOut ↑f = false}.val

The attachWith of the sorted list of a finset filter, as a multiset, equals the val of univ.filter on the subtype.

The match bijection between incoming and outgoing flags

Splitting the all-at-v filter into in and out parts

Main theorem

theorem RS.oddListAt_coe_multiset {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : ↑(F.oddListAt o φ v) = Multiset.map (fun (f : ↥F.flags) => if o.isOut ↑f = true then oddPartner ℓ (↑φ f) else ↑φ f) {f : ↥F.flags | W.attach ↑f = Sum.inl v}.val

A vertex's odd list as a multiset: the per-flag odd values over the flags at that vertex.