α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : Fin (length xs)
h : get xs n = get xs m
hne : n ≠ m
⊢ ¬Injective (get xs)
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : Fin (length xs)
h : get xs n = get xs m
hne : n ≠ m
⊢ ¬Nodup xs
rw [nodup_iff_injective_get]
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : Fin (length xs)
h : get xs n = get xs m
hne : n ≠ m
⊢ ¬Injective (get xs)
exact fun hinj => hne (hinj h)