Set membership with explicit constructor

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

tidy solves it.

[Kevin Buzzard]

simp * at *, tauto also works

[ROCKY KAMEN-RUBIO]

Thank you! I always forget about tidy. That's fascinating that simp at h, simp, behaves differently than simp * at *.

[Kevin Buzzard]

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]

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.