chore: further cleanup from shaking Init (#10658)

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
 

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

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