Failed to synthesize instance

Stream: new members

[Owen Anderson]

Can anyone shed light on why I'm getting "failed to synthesize instance, Inter ↑subsets" on this snippet:

@[ext]
structure SetPartition (set : Set α) :=
  subsets : Set (Set α)
  union_to_all: Set.sUnion subsets = set
  all_disjoint : ∀ (suba subb : subsets), suba ≠ subb → suba ∩ subb = ∅

[Ruben Van de Velde]

#mwe, please

[Filippo A. E. Nuccio]

You should convince lean that suba must be regarder as a set:

structure SetPartition (set : Set α) :=
  subsets : Set (Set α)
  union_to_all: sUnion subsets = set
  all_disjoint : ∀ (suba subb : subsets), suba ≠ subb → (suba : Set α) ∩ subb = ∅

[Patrick Massot]

It would be much better to have them being sets from the beginning:

@[ext]
structure SetPartition (set : Set α) :=
  subsets : Set (Set α)
  union_to_all: Set.sUnion subsets = set
  all_disjoint : ∀ suba ∈ subsets, ∀ subb ∈ subsets, suba ≠ subb → suba ∩ subb = ∅