α : Type u_1
ι : Type ?u.7414
ι' : Type ?u.7417
β : Type ?u.7420
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
α : Type u_1
ι : Type ?u.7414
ι' : Type ?u.7417
β : Type ?u.7420
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
letI : IsSymm α r := ⟨hs⟩
no goals
α : Type u_1
ι : Type ?u.7414
ι' : Type ?u.7417
β : Type ?u.7420
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hn : Nodup l
hs : Symmetric r
this : IsSymm α r := { symm := hs }
⊢ Set.Pairwise (↑(toFinset l)) r ↔ Pairwise r l
rw [coe_toFinset, hn.pairwise_coe]