English
If a Finset s is nontrivial, then s can be built by inserting two distinct elements into some smaller Finset.
Русский
Если Finset s не тривиален, то его можно собрать вставив два различных элемента в некоторый меньший Finset.
LaTeX
$$$ \\forall {\\alpha} {s : Finset \\alpha}, s.Nontrivial \\rightarrow \\exists t\\ a\\ ha\\ b\\ hb\\ hab, s = insert a (insert b t) $$$
Lean4
theorem exists_cons_eq {s : Finset α} (hs : s.Nontrivial) :
∃ t a ha b hb hab, (cons b t hb).cons a (mem_cons.not.2 <| not_or_intro hab ha) = s := by
classical
obtain ⟨a, ha, b, hb, hab⟩ := hs
have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase this, insert_erase ha, *]
