2 members of a set with 2 elements

Stream: Is there code for X?

[Snir Broshi]

import Mathlib
theorem foo {α : Type*} (a b c d : α)
    (hc : c ∈ ({a, b} : Set α))
    (hd : d ∈ ({a, b} : Set α)) :
    c = d ∨ s(a, b) = s(c, d) := by
  sorry

This feels like a grind or tauto problem but they fail here.

[Ruben Van de Velde]

simp_all; grind works

[Snir Broshi]

Thanks! This also helped me find grind [Sym2.eq_iff]

[Jakub Nowak]

Yeah, Sym2 doesn't have any lemmas marked with @[grind] unfortunately. :(
It has some @[aesop] lemmas though, and indeed aesop can close the goal.