# Zulip Chat Archive

## Stream: general

### Topic: unique existence with Prop

#### Peter Nelson (Feb 16 2021 at 17:56):

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 (Feb 16 2021 at 18:01):

```
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 (Feb 16 2021 at 18:01):

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 (Feb 16 2021 at 18:05):

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 (Feb 16 2021 at 18:07):

`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 (Feb 16 2021 at 18:09):

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 (Feb 16 2021 at 18:13):

One day it will be, but `simp?`

is a work in progress right now.

Last updated: May 11 2021 at 00:31 UTC