induction x using cons_induction with
| empty =>
  simp only [nodup_empty, true_iff]
  intro i; exact i.elim0
| cons a x IH =>
  rewrite [nodup_cons, IH]; clear IH
  constructor
  . intro h i j hxij
    rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
    cases i <;> cases j <;> simp at hxij ⊢
    . exfalso; apply h.1
      rewrite [hxij]; exact getElem_mem x _
    . exfalso; apply h.1
      rewrite [← hxij]; exact getElem_mem x _
    . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
  . intro h
    constructor
    . intro hmem
      have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
      specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
      cases h
    . intro i j
      specialize h i.succ j.succ
      simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
      exact h
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
no goals