English
CutExpand r s' s is equivalent to the existence of a witness t and an element a with certain properties relating a to s and s'.
Русский
CutExpand r s' s эквивалентно существованию свидетельства t и элемента a с определёнными свойствами, связывающими a с s и s'.
LaTeX
$$$\\mathrm{CutExpand}(r)(s',s) \\iff \\exists t,a:\\; (\\forall a'\\in t, r(a',a)) \\land a\\in s \\land s' = s.erase(a) + t$$$
Lean4
theorem cutExpand_iff [DecidableEq α] [IsIrrefl α r] {s' s : Multiset α} :
CutExpand r s' s ↔ ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t :=
by
simp_rw [CutExpand, add_singleton_eq_iff]
refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩
· rintro ⟨ht, ha, rfl⟩
obtain h | h := mem_add.1 ha
exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
· rintro ⟨ht, h, rfl⟩
exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
