no goals
α : Type u_1
β : Type ?u.10660
γ : Type ?u.10663
ι : Type ?u.10666
ι' : Type ?u.10669
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
⊢ a ≠ b → r a b ∧ r b a ↔ r a b ∧ r b a
simp [(ne_of_mem_of_not_mem hb ha).symm]