no goals
α : Type u_1
β : Type ?u.11504
γ : Type ?u.11507
ι : Type ?u.11510
ι' : Type ?u.11513
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b
simp only [pairwise_insert, hr.iff a, and_self_iff]