diff --git a/Mathlib.lean b/Mathlib.lean
index c8a2f776afe82..8e4751136a7f5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2791,7 +2791,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
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 937ec7c6da20d..bb29c0f7e1ad9 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -78,6 +78,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⟩
 
diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
index 5bfb47206bb95..f5d371b85b7ad 100644
--- a/Mathlib/Data/List/Nodup.lean
+++ b/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 :=
diff --git a/Mathlib/Data/List/Range.lean b/Mathlib/Data/List/Range.lean
index 64aec7b5b00f9..4f1ef5b6229a7 100644
--- a/Mathlib/Data/List/Range.lean
+++ b/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
diff --git a/Mathlib/Init/Data/Fin/Basic.lean b/Mathlib/Init/Data/Fin/Basic.lean
deleted file mode 100644
index 65540086b8caa..0000000000000
--- a/Mathlib/Init/Data/Fin/Basic.lean
+++ /dev/null
@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Mathlib.Data.Nat.Notation
-
-/-!
-# Note about `Mathlib/Init/`
-The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
-(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
-
-We intend to move all the content of these files out into the main `Mathlib` directory structure.
-Contributions assisting with this are appreciated.
-
-# Theorems about equality in `Fin`.
--/
-
-namespace Fin
-
-variable {n : ℕ} {i j : Fin n}
-
-@[deprecated eq_of_val_eq (since := "2024-02-15")]
-theorem eq_of_veq : i.val = j.val → i = j := eq_of_val_eq
-
-@[deprecated val_eq_of_eq (since := "2024-02-15")]
-theorem veq_of_eq : i = j → i.val = j.val := val_eq_of_eq
-
--- These two aren't deprecated because `ne_of_val_ne` and `val_ne_of_ne`
--- use `¬a = b` instead of `a ≠ b`. TODO: fix or rename in Lean core.
-theorem ne_of_vne (h : i.val ≠ j.val) : i ≠ j := ne_of_val_ne h
-theorem vne_of_ne (h : i ≠ j) : i.val ≠ j.val := val_ne_of_ne h
-
-end Fin