Representatives of each part of a Finpartition

Stream: mathlib4

[Jeremy Tan]

I have a Finpartition of a Finset over some type, say {{1, 2, 3}, {4, 5, 6, 7}, {8, 9}}. Now I want to (obviously noncomputably) get representatives of each part of this Finpartition and collect them in a new Finset – {2, 4, 9} for example. The code to do this would be

import Mathlib.Order.Partition.Finpartition

variable {α : Type*} [DecidableEq α] {s : Finset α} (P : Finpartition s)

noncomputable def Finpartition.representatives : Finset α :=
  P.parts.image (fun st => st.some)

except that this doesn't work. How can I make it work?

[Yaël Dillies]

What's that .some supposed to be?

[Yaël Dillies]

Surely you mean something like P.parts.attach.map ⟨fun s ↦ (P.nonempty_of_mem_parts s.2).some, sorry⟩?

[Jeremy Tan]

Yaël Dillies said:

What's that .some supposed to be?

"Choose some element from st"

[Yaël Dillies]

Okay, but what is the Lean declaration corresponding to it?

[Jeremy Tan]

Context:

theorem notAdj_card_parts_le' : (notAdjFinpartition hmax).parts.card ≤ r := by
  let fp := notAdjFinpartition hmax
  by_contra h; push_neg at h
  -- `z` is to be proved to be an `r + 1`-clique in G, contradicting Turán-maximality!
  have z := fp.parts.attach.map ⟨fun p => (fp.nonempty_of_mem_parts p.2).choose, by
    rw [Function.Injective]
    intro p1 p2 e
    simp_all⟩
  simp

[Jeremy Tan]

(Yeah I was wrong, .choose is the right method)