More equality of sets

Stream: new members

[Pranav cs22b015]

Is there a nice way to prove the equality of two sets automatically? For example, is there an easy way to show the following

theorem sets_equal: forall (s: Set Int), {b | b ∈ s ∪ {5} ∧ b != 5} = {a | a ∈ s}

[Aaron Liu]

docs#Set.ext

[Ruben Van de Velde]

And then simp or grind will probably work

[Notification Bot]

3 messages were moved here from #new members > Encoding FStar-like sets axiomatically by Ruben Van de Velde.

[Rémy Degenne]

Your goal is false by the way. If you fix it, grind solves it.

import Mathlib.Data.Set.Insert

theorem not_sets_equal : ¬ ∀ (s: Set Int),
    {b | b ∈ s ∪ {5} ∧ b != 5} = {a | a ∈ s} := by
  push_neg
  use {(5 : ℤ)}
  symm
  simp

theorem sets_equal' : ∀ (s: Set Int),
    {b | b ∈ s ∪ {5} ∧ b != 5} = {a | a ∈ s ∧ a ≠ 5} := by
  grind