no goals
α : Type u_1
β : Type ?u.10052
γ : Type ?u.10055
ι : Type ?u.10058
ι' : Type ?u.10061
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a
simp only [insert_eq, pairwise_union, pairwise_singleton, true_and_iff, mem_singleton_iff,
  forall_eq]