Get single element from `finset`

Stream: Is there code for X?

[Marcus Rossel]

Is there a way to (a) state that a finset contains exactly one element, and (b) extract that element if (a) is true?

[Johan Commelin]

Computably?

[Johan Commelin]

Otherwise, s.card = 1

[Johan Commelin]

And there must be some lemma that gives s.nonempty from 0 < s.card

[Johan Commelin]

If you want to do this computably, you'll have to look at the def'n of finset, and notice that it's basically a list under the hood.

[Marcus Rossel]

(deleted)

[Marcus Rossel]

For the classical path finset.card_eq_one works.

[Mario Carneiro]

import data.finset

def multiset.extract_singleton {α} (s : multiset α) : s.card = 1 → α :=
quotient.rec_on s (λ l, match l with [a], _ := a end) $ λ a b h,
funext $ λ H₂, begin
  have H₁ := by rw ← quotient.sound h at H₂; exact H₂,
  exact match a, b, H₁, H₂, h :
    ∀ a b (H₁ : a.length = 1) (H : b.length = 1) (h : list.perm a b), _ with
  | [a], [b], _, _, h := begin
      rcases h.mem_iff.1 (or.inl rfl) with rfl | ⟨⟨⟩⟩,
      refl,
    end
  end
end

theorem multiset.eq_extract_singleton {α} (s : multiset α) (h) : s = s.extract_singleton h ::ₘ 0 :=
quotient.induction_on s (λ l, match l with [a], _ := rfl end) h

def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α :=
s.1.extract_singleton h

theorem finset.eq_extract_singleton {α} (s : finset α) (h) : s = singleton (s.extract_singleton h) :=
finset.eq_of_veq $ s.1.eq_extract_singleton h

[Eric Wieser]

Can docs#finset.choose help here?

[Eric Wieser]

def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α :=
s.choose (set.univ) $ begin
  obtain ⟨a, rfl⟩ := finset.card_eq_one.mp h,
  refine ⟨a, ⟨finset.mem_singleton_self a, trivial⟩, λ i h, finset.mem_singleton.mp h.1⟩,
end