no goals
α : Type u_1
β : Type ?u.92
γ : Type ?u.95
ι : Type ?u.98
ι' : Type ?u.101
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a✝ b✝ : α
hr : Symmetric r
a b : α
⊢ Pairwise (r on fun c => bif c then a else b) ↔ r a b
simpa [Pairwise, Function.onFun] using @hr a b