α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ¬∀ (i j : ℕ) (h₁ : i < length xs) (h₂ : j < length xs), nthLe xs i h₁ = nthLe xs j h₂ → i = j
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ¬Nodup xs
rw [nodup_iff_nthLe_inj]
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ∃ x x_1, (∃ x_2 x_3, nthLe xs x (_ : x < length xs) = nthLe xs x_1 (_ : x_1 < length xs)) ∧ ¬x = x_1
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ¬∀ (i j : ℕ) (h₁ : i < length xs) (h₂ : j < length xs), nthLe xs i h₁ = nthLe xs j h₂ → i = j
simp only [exists_prop, exists_and_right, not_forall]
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
xs : List α
n m : ℕ
hn : n < length xs
hm : m < length xs
h : nthLe xs n hn = nthLe xs m hm
hne : n ≠ m
⊢ ∃ x x_1, (∃ x_2 x_3, nthLe xs x (_ : x < length xs) = nthLe xs x_1 (_ : x_1 < length xs)) ∧ ¬x = x_1
exact ⟨n, m, ⟨hn, hm, h⟩, hne⟩