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