-- Mathlib/Data/List/Nodup.lean
theorem nodup_iff_injective_getElem {l : List α} :
    Nodup l ↔ Function.Injective (fun i : Fin l.length => l[i.1]) :=
  pairwise_iff_getElem.trans
    ⟨fun h i j hg => by
      obtain ⟨i, hi⟩ := i; obtain ⟨j, hj⟩ := j
      rcases lt_trichotomy i j with (hij | rfl | hji)
      · exact (h i j hi hj hij hg).elim
      · rfl
      · exact (h j i hj hi hji hg.symm).elim,
      fun hinj i j hi hj hij h => Nat.ne_of_lt hij (Fin.val_eq_of_eq (@hinj ⟨i, hi⟩ ⟨j, hj⟩ h))⟩

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 : Fin l.length
hg : (fun i => l[↑i]) i = (fun i => l[↑i]) j
⊢ i = j

Tactic:
obtain ⟨i, hi⟩ := i

Result:
case mk
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
j : Fin l.length
i : ℕ
hi : i < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) j
⊢ ⟨i, hi⟩ = j

Proof state:
case mk.mk.inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
exact (h j i hj hi hji hg.symm).elim

Result:
no goals

Proof state:
case mk.mk.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
exact (h i j hi hj hij hg).elim

Result:
no goals

Proof state:
case mk
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
j : Fin l.length
i : ℕ
hi : i < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) j
⊢ ⟨i, hi⟩ = j

Tactic:
obtain ⟨j, hj⟩ := j

Result:
case mk.mk
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Proof state:
case mk.mk
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
rcases lt_trichotomy i j with (hij | rfl | hji)

Result:
case mk.mk.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

case mk.mk.inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

case mk.mk.inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Proof state:
case mk.mk.inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

Tactic:
rfl

Result:
no goals