no goals
α : Type u_1
β : Type ?u.12763
γ : Type ?u.12766
ι : Type ?u.12769
ι' : Type ?u.12772
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a
simp [pairwise_insert]