case mk
n : ℕ
α : Type u_1
l : List α
hl : List.length l = n
⊢ List.Nodup (toList { val := l, property := hl }) ↔ Function.Injective (get { val := l, property := hl })
n : ℕ
α : Type u_1
v : Vector α n
⊢ List.Nodup (toList v) ↔ Function.Injective (get v)
cases' v with l hl
case mk
α : Type u_1
l : List α
⊢ List.Nodup (toList { val := l, property := (_ : List.length l = List.length l) }) ↔
    Function.Injective (get { val := l, property := (_ : List.length l = List.length l) })
case mk
n : ℕ
α : Type u_1
l : List α
hl : List.length l = n
⊢ List.Nodup (toList { val := l, property := hl }) ↔ Function.Injective (get { val := l, property := hl })
subst hl
no goals
case mk
α : Type u_1
l : List α
⊢ List.Nodup (toList { val := l, property := (_ : List.length l = List.length l) }) ↔
    Function.Injective (get { val := l, property := (_ : List.length l = List.length l) })
exact List.nodup_iff_injective_get