no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b✝ : α
f : β → α
b : β
l : List β
⊢ Chain R (f b) (map f l) ↔ Chain (fun a b => R (f a) (f b)) b l
induction l generalizing b <;> simp only [map, Chain.nil, chain_cons, *]