# Zulip Chat Archive

## Stream: new members

### Topic: Set membership with explicit constructor

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 17:22):

I'm back with another noob finset question.

**MWE:**

```
import tactic
import data.finset
variable P : Type*
example {p1 p2 p3 p : P} {h : p ∈ ({p1, p2} : finset P)} : p ∈ ({p1, p2, p3} : finset P) :=
begin
sorry,
end
```

**More context:**

I'm trying to simplify a more complex expression that a finset is a subset of the union/intersection of other finsets. All are defined explicitly, and I have equality/inequality expressions for every pair of elements. `simp`

reduces the larger set into a series of `insert`

expression, but that's it. Has anyone tried writing something like `linarith`

but for sets?

#### Kevin Buzzard (Jun 22 2020 at 17:24):

`tidy`

solves it.

#### Kevin Buzzard (Jun 22 2020 at 17:25):

`simp * at *, tauto`

also works

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 17:45):

Thank you! I always forget about tidy. That's fascinating that `simp at h, simp,`

behaves differently than `simp * at *`

.

#### Kevin Buzzard (Jun 22 2020 at 18:22):

For me, both `simp at h, simp`

and `simp * at *`

turn the local context into

```
P : Type u_1
_inst_1 : decidable_eq P
p1 : P
p2 : P
p3 : P
p : P
h : p = p1 ∨ p = p2
⊢ p = p1 ∨ p = p2 ∨ p = p3
```

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 18:29):

Kevin Buzzard said:

For me, both

`simp at h, simp`

and`simp * at *`

turn the local context into`P : Type u_1 _inst_1 : decidable_eq P p1 : P p2 : P p3 : P p : P h : p = p1 ∨ p = p2 ⊢ p = p1 ∨ p = p2 ∨ p = p3`

Interesting. Trying it again I'm getting the same behavior as you. Maybe my file is just getting too big. I've been careful not to leave any errors though.

Last updated: May 15 2021 at 23:13 UTC