chore: remove unnecessary deprecated alias

erdkocak · erdkocak · commit 455edf8fe9af · 2026-07-04T12:19:24.000+03:00
diff --git a/Mathlib/ModelTheory/PartialEquiv.lean b/Mathlib/ModelTheory/PartialEquiv.lean
@@ -575,8 +575,6 @@ theorem equiv_between_cg (M_cg : Structure.CG L M) (N_cg : Structure.CG L N)
   rw [toEquivOfEqTop_toEmbedding]
   apply Embedding.toPartialEquiv_toEmbedding
 
-@[deprecated (since := "2026-06-13")] alias equiv_from_cg := equiv_between_cg
-
 end FGEquiv
 
 end Language
