## 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