no goals
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a : α
l : List α
f : β → α
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []
simp only [map, Pairwise.nil]
no goals
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a : α
l✝ : List α
f : β → α
b : β
l : List β
⊢ Pairwise R (map f (b :: l)) ↔ Pairwise (fun a b => R (f a) (f b)) (b :: l)
simp only [map, pairwise_cons, mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, pairwise_map]