fix: grind invalid universe level regression

This PR fixes the `grind` invalid universe level regression reported
in #11036

Closes #11036

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -171,7 +171,7 @@ def getStructId? (type : Expr) : GoalM (Option Nat) := do
     return id?
 where
   go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
+    let some u ← getDecLevel? type | return none
     let ringId? ← CommRing.getCommRingId? type
     let leInst? ← getInst? ``LE u type
     let ltInst? ← getInst? ``LT u type

tests/lean/run/grind_11036.lean

@@ -0,0 +1,22 @@
+variable {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α]
+  {f : (a : α) → β a} {a : α} {b : β a}
+
+/-- Replacing the value of a function at a given point by a given value. -/
+def Function.update (f : ∀ a, β a) (a' : α) (v : β a') (a : α) : β a :=
+  if h : a = a' then Eq.ndrec v h.symm else f a
+
+@[simp]
+theorem Function.update_self (a : α) (v : β a) (f : ∀ a, β a) : update f a v a = v :=
+  dif_pos rfl
+
+@[simp]
+theorem Function.update_of_ne {a a' : α} (h : a ≠ a') (v : β a') (f : ∀ a, β a) : update f a' v a = f a :=
+  dif_neg h
+
+theorem domDomRestrict_aux {ι : Sort u_1} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type u_2}
+    [DecidableEq {a // P a}]
+    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // P a})
+    (c : M₁ i) : (fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
+    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c := by
+  ext j
+  by_cases h : j = i <;> grind only [Function.update_self, Function.update_of_ne]