[Merged by Bors] - chore: delete Init.Data.Fin.Basic

Mathlib.lean

@@ -2790,7 +2790,6 @@ import Mathlib.InformationTheory.Hamming
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Init.Classical
 import Mathlib.Init.Core
-import Mathlib.Init.Data.Fin.Basic
 import Mathlib.Init.Data.Int.Order
 import Mathlib.Init.Data.List.Basic
 import Mathlib.Init.Data.List.Instances

Mathlib/Data/Fin/Basic.lean

@@ -79,6 +79,11 @@ def finZeroElim {α : Fin 0 → Sort*} (x : Fin 0) : α x :=
 
 namespace Fin
 
+@[deprecated (since := "2024-02-15")] alias eq_of_veq := eq_of_val_eq
+@[deprecated (since := "2024-02-15")] alias veq_of_eq := val_eq_of_eq
+@[deprecated (since := "2024-08-13")] alias ne_of_vne := ne_of_val_ne
+@[deprecated (since := "2024-08-13")] alias vne_of_ne := val_ne_of_ne
+
 instance {n : ℕ} : CanLift ℕ (Fin n) Fin.val (· < n) where
   prf k hk := ⟨⟨k, hk⟩, rfl⟩
 

Mathlib/Data/List/Nodup.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kenny Lau
 -/
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.Set.Pairwise.Basic
-import Mathlib.Init.Data.Fin.Basic
 
 /-!
 # Lists with no duplicates
@@ -84,7 +83,7 @@ theorem nodup_iff_nthLe_inj {l : List α} :
     Nodup l ↔ ∀ i j h₁ h₂, nthLe l i h₁ = nthLe l j h₂ → i = j :=
   nodup_iff_injective_get.trans
     ⟨fun hinj _ _ _ _ h => congr_arg Fin.val (hinj h),
-     fun hinj i j h => Fin.eq_of_veq (hinj i j i.2 j.2 h)⟩
+     fun hinj i j h => Fin.eq_of_val_eq (hinj i j i.2 j.2 h)⟩
 
 theorem Nodup.get_inj_iff {l : List α} (h : Nodup l) {i j : Fin l.length} :
     l.get i = l.get j ↔ i = j :=

Mathlib/Data/List/Range.lean

@@ -67,7 +67,7 @@ theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n :=
       rfl⟩
 
 theorem nodup_finRange (n : ℕ) : (finRange n).Nodup :=
-  (Pairwise.pmap (nodup_range n) _) fun _ _ _ _ => @Fin.ne_of_vne _ ⟨_, _⟩ ⟨_, _⟩
+  (Pairwise.pmap (nodup_range n) _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩
 
 @[simp]
 theorem length_finRange (n : ℕ) : (finRange n).length = n := by