restore Subtype.eq_iff

kim-em · kim-em · commit 905c960f169b · 2025-10-28T01:44:42.000+01:00
diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean
@@ -84,6 +84,9 @@ end Lean
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.ext Array.ext Char.ext
 
+@[deprecated Subtype.ext_iff (since := "2025-10-26")]
+protected def Subtype.eq_iff := @Subtype.ext_iff
+
 attribute [grind ext] funext Array.ext
 
 attribute [ext] PUnit.ext
