diff --git a/src/Init/Data/Order/FactoriesExtra.lean b/src/Init/Data/Order/FactoriesExtra.lean
index d1285acde4..ec37baacca 100644
--- a/src/Init/Data/Order/FactoriesExtra.lean
+++ b/src/Init/Data/Order/FactoriesExtra.lean
@@ -65,7 +65,6 @@ public theorem compare_eq_gt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrder
 
 public theorem compare_eq_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α]
     {a b : α} : compare a b = .eq ↔ a == b := by
-  open Classical.Order in
   rw [LawfulOrderBEq.beq_iff_le_and_ge, ← isLE_compare, ← isGE_compare]
   cases compare a b <;> simp
 
diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean
index 6af6f80086..be3834235c 100644
--- a/src/Init/Ext.lean
+++ b/src/Init/Ext.lean
@@ -84,7 +84,7 @@ end Lean
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq Array.ext
 
-attribute [grind ext] Array.ext
+attribute [grind ext] funext Array.ext
 
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
diff --git a/src/Init/Grind/Ext.lean b/src/Init/Grind/Ext.lean
index 03344387ad..fa1d7ba87a 100644
--- a/src/Init/Grind/Ext.lean
+++ b/src/Init/Grind/Ext.lean
@@ -11,4 +11,4 @@ public import Init.Grind.Tactics
 
 public section
 
-attribute [grind ext] funext Prod Subtype Sigma PSigma
+attribute [grind ext] Prod Subtype Sigma PSigma