unique existence with Prop

Stream: general

[Peter Nelson]

This is probably an easy one... how do I replace the 'finish' (which works) with a less opaque proof here? When attempting a proof by cases, I seem to be getting snared up in dependent types - proof-irrelevance should somehow be used, but I don't immediately see how.

import data.setoid.partition

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
  have := @setoid.classes_eqv_classes _ r a,
  --  this: ∃! (b : set α) (H : b ∈ r.classes), a ∈ b
  finish,
end

[Yakov Pechersky]

import data.setoid.partition

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
  obtain ⟨b, ⟨h, hb, -⟩, hu⟩ := @setoid.classes_eqv_classes _ r a,
  refine ⟨b, ⟨h, hb⟩, _⟩,
  convert hu,
  simp
end

[Alex J. Best]

You can do

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
  convert @setoid.classes_eqv_classes _ r a,
  simp,
end

[Peter Nelson]

Thank you! simp is a little less opaque - however, in both your solutions, using simp? gives a suggestion which fails. The 'hard part' of the proof is still hiding. Can anyone shed some light on it?

[Bryan Gin-ge Chen]

simp? is still not quite ready for general use, I think. squeeze_simp returns: simp only [exists_prop, exists_unique_iff_exists],, which works.

[Peter Nelson]

Aha, thank you! I didn't realize simp? wasn't the same as squeeze_simp. Those two lemmas give exactly the missing pieces I was curious about.

[Kevin Buzzard]

One day it will be, but simp? is a work in progress right now.