fix test

src/Init/Grind/Cases.lean

@@ -11,4 +11,4 @@ public import Init.Grind.Tactics
 public section
 
 attribute [grind cases eager] And False Empty True PUnit Exists Subtype Prod PProd MProd
-attribute [grind cases] Or
+attribute [grind cases] Or Sum PSum

tests/lean/run/grind_10983.lean

@@ -10,5 +10,4 @@ def sumEquivSigmaBool (α β) : Equiv (α ⊕ β) (Σ b, bif b then β else α)
     | ⟨false, a⟩ => .inl a
     | ⟨true, b⟩ => .inr b
   left_inv := fun s => by
-    fail_if_success grind
-    sorry
+    grind