Theorem: nodup_eq_len_imp_eqv (FOL/List.lean)

State before:
α : Type
inst✝ : DecidableEq α
xs ys : List α
h1 : xs.length = ys.length
h2 : xs.Nodup
h3 : ys.Nodup
⊢ ∃ f, List.map (⇑f) xs = ys
Tactic:
sorry
State after:
no goals