-- Mathlib/Data/List/Nodup.lean
theorem nodup_iff_getElem?_ne_getElem? {l : List α} :
    l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l[i]? ≠ l[j]?

Proof state:
case mp
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : ℕ
hij : i < j
hj : j < l.length
⊢ ¬l[i] = l[j]

Tactic:
exact h _ _ (by omega) hj hij

Result:
no goals

Proof state:
case mp
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : ℕ
hij : i < j
hj : j < l.length
⊢ l[i]? ≠ l[j]?

Tactic:
rw [getElem?_eq_getElem (lt_trans hij hj), getElem?_eq_getElem hj, Ne, Option.some_inj]

Result:
case mp
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : ℕ
hij : i < j
hj : j < l.length
⊢ ¬l[i] = l[j]

Proof state:
case mpr
α : Type u
l : List α
h : ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ l[i] ≠ l[j]

Tactic:
rw [Ne, ← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem]

Result:
case mpr
α : Type u
l : List α
h : ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ ¬l[i]? = l[j]?

Proof state:
case mp
α : Type u
l : List α
⊢ (∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]) →
    ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
intro h i j hij hj

Result:
case mp
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : ℕ
hij : i < j
hj : j < l.length
⊢ l[i]? ≠ l[j]?

Proof state:
case mpr
α : Type u
l : List α
h : ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ ¬l[i]? = l[j]?

Tactic:
exact h i j hij hj

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ (∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]) ↔
    ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
constructor

Result:
case mp
α : Type u
l : List α
⊢ (∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]) →
    ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

case mpr
α : Type u
l : List α
⊢ (∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?) →
    ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]

Proof state:
case mpr
α : Type u
l : List α
⊢ (∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?) →
    ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]

Tactic:
intro h i j hi hj hij

Result:
case mpr
α : Type u
l : List α
h : ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ l[i] ≠ l[j]

Proof state:
α : Type u
l : List α
⊢ l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
rw [Nodup, pairwise_iff_getElem]

Result:
α : Type u
l : List α
⊢ (∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]) ↔
    ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Proof state:
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : ℕ
hij : i < j
hj : j < l.length
⊢ i < l.length

Tactic:
omega

Result:
no goals