no goals
α : Type u_1
β : Type ?u.14609
γ : Type ?u.14612
ι : Type ?u.14615
ι' : Type ?u.14618
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b
simp [pairwise_insert_of_symmetric hr]