English
If l' is a list of multisets and H asserts that every element in revzip(l') sums to ↑l, then revzip(l') equals l'.map (λ x, (x, ↑l - x)).
Русский
Пусть l' — список мультимножеств; если для каждого элемента revzip(l') выполнено равенство, то revzip(l') = l'.map (λ x, (x, ↑l - x)).
LaTeX
$$$ \\forall \\alpha, \\text{ ... } \\; revzip(l') = l'.map(\\lambda x. (x, (l : Multiset\\alpha) - x)) $$$
Lean4
theorem revzip_powersetAux_lemma {α : Type*} [DecidableEq α] (l : List α) {l' : List (Multiset α)}
(H : ∀ ⦃x : _ × _⦄, x ∈ revzip l' → x.1 + x.2 = ↑l) : revzip l' = l'.map fun x => (x, (l : Multiset α) - x) :=
by
have :
Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
((revzip l').map Prod.fst) :=
by
rw [forall₂_map_right_iff, forall₂_same]
rintro ⟨s, t⟩ h
dsimp
rw [← H h, add_tsub_cancel_left]
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
simpa using this
