α : Type u_1
ι : Type ?u.6985
ι' : Type ?u.6988
β : Type ?u.6991
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a | a ∈ l} r
hn : Nodup l
⊢ Pairwise r l
α : Type u_1
ι : Type ?u.6985
ι' : Type ?u.6988
β : Type ?u.6991
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise (↑(toFinset l)) r
hn : Nodup l
⊢ Pairwise r l
rw [coe_toFinset] at hl
no goals
α : Type u_1
ι : Type ?u.6985
ι' : Type ?u.6988
β : Type ?u.6991
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a | a ∈ l} r
hn : Nodup l
⊢ Pairwise r l
exact hn.pairwise_of_set_pairwise hl