∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (d : DiscreteQuotient X),
  DiscreteQuotient.finsetClopens X d = (Set.range fun x => { carrier := d.proj ⁻¹' {x}, isClopen' := ⋯ }).toFinset