Solving a problem about set membership

Stream: new members

[Dillon Huff]

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]

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

theorem set_trivia [α : Type] (S Γ : set α) (φ : α) (H : φ ∉ S) (H' : S ⊆ Γ ∪ {φ}) :
  S ⊆ Γ :=
begin
  intros x hs,
  have := H' hs,
  rw set.mem_union at this,
  apply this.resolve_right,
  rw set.mem_singleton_iff,
  rintro rfl,
  contradiction,
end

[Kevin Buzzard]

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

[Dillon Huff]

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]

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