no goals
α : Type u_1
β : Type ?u.11936
γ : Type ?u.11939
ι : Type ?u.11942
ι' : Type ?u.11945
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
ha : ¬a ∈ s
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → r a b
simp only [pairwise_insert_of_not_mem ha, hr.iff a, and_self_iff]