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


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