# Zulip Chat Archive

## Stream: new members

### Topic: Solving a problem about set membership

#### Dillon Huff (Feb 20 2021 at 20:13):

Is there a tactic in mathlib for solving set membership problems? I'm interested in proving some theorems about whether or not a set includes members from a superset. For example:

```
theorem set_trivia [α : Type] (S Γ : set α) (φ : α) (φ ∉ S) (S ⊆ Γ ∪ {φ}) :
S ⊆ Γ :=
begin
sorry,
end
```

Thanks in advance!

#### Ruben Van de Velde (Feb 20 2021 at 21:12):

I don't think there's a tactic; your example can be solved with

#### Kevin Buzzard (Feb 20 2021 at 21:19):

I think we've had this conversation before. What happens if you turn everything into propositions and then use `cc`

?

#### Dillon Huff (Feb 20 2021 at 21:31):

Unfortunately I'm a newb so I don't know enough about lean to say.

I had thought there might be tactic for this because in this video on formalizing matroids in lean: https://www.youtube.com/watch?v=FzJuoXy5cG0 they seem to have a related tactic they call `timed_simplify_sets`

, though at 37:14 the presenter says something about how its not efficient, and that the correspondence between some of the problems they wanted to solve and propositional logic was more complicated than they thought. Maybe that comment is relevant here?

#### Bryan Gin-ge Chen (Feb 20 2021 at 21:35):

Once you put in the `have`

from Ruben's proof, `finish`

can do the rest of the job:

```
import tactic
theorem set_trivia [α : Type] (S Γ : set α) (φ : α) (H : φ ∉ S) (H' : S ⊆ Γ ∪ {φ}) :
S ⊆ Γ :=
begin
intros x hs,
have := H' hs,
finish,
end
```

Last updated: May 16 2021 at 05:21 UTC