fix(data/list/nodup): change Type to Type u (#14721)

Change `Type` to `Type u` in `nodup_iff_nth_ne_nth` and two other lemmas added in #14371.

src/data/list/basic.lean

@@ -1381,12 +1381,10 @@ begin
   exact eq_bot_iff.mpr (nat.lt_succ_iff.mp h₂)
 end
 
-lemma nth_le_eq_iff {α : Type}
-  {l : list α} {n : ℕ} {x : α} {h} : l.nth_le n h = x ↔ l.nth n = some x :=
+lemma nth_le_eq_iff {l : list α} {n : ℕ} {x : α} {h} : l.nth_le n h = x ↔ l.nth n = some x :=
 by { rw nth_eq_some, tauto }
 
-lemma some_nth_le_eq {α : Type}
-  {l : list α} {n : ℕ} {h} : some (l.nth_le n h) = l.nth n :=
+lemma some_nth_le_eq {l : list α} {n : ℕ} {h} : some (l.nth_le n h) = l.nth n :=
 by { symmetry, rw nth_eq_some, tauto }
 
 lemma modify_nth_tail_modify_nth_tail {f g : list α → list α} (m : ℕ) :

src/data/list/nodup.lean

@@ -69,12 +69,12 @@ pairwise_iff_nth_le.trans
   .resolve_right (λ h', H _ _ h₁ h' h.symm),
  λ H i j h₁ h₂ h, ne_of_lt h₂ (H _ _ _ _ h)⟩
 
-theorem nodup.nth_le_inj_iff {α : Type*} {l : list α} (h : nodup l)
+theorem nodup.nth_le_inj_iff {l : list α} (h : nodup l)
   {i j : ℕ} (hi : i < l.length) (hj : j < l.length) :
   l.nth_le i hi = l.nth_le j hj ↔ i = j :=
 ⟨nodup_iff_nth_le_inj.mp h _ _ _ _, by simp {contextual := tt}⟩
 
-lemma nodup_iff_nth_ne_nth {α : Type} {l : list α} :
+lemma nodup_iff_nth_ne_nth {l : list α} :
   l.nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.nth i ≠ l.nth j :=
 begin
   rw nodup_iff_nth_le_inj,