α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n))
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (ofFn f)
rw [ofFn_eq_pmap]
no goals
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n))
exact (nodup_range n).pmap fun _ _ _ _ H => Fin.veq_of_eq <| hf H