fix: missing grind normalization rule (#7724)

This PR adds `dite_eq_ite` normalization rule to `grind`. This rule is
important to adjust mismatches between a definition and its function
induction principle.

src/Init/Grind/Norm.lean

@@ -106,6 +106,7 @@ init_grind_norm
   or_true true_or or_false false_or or_assoc
   -- ite
   ite_true ite_false ite_true_false ite_false_true
+  dite_eq_ite
   -- Forall
   forall_and
   -- Exists

tests/lean/run/grind_t1.lean

@@ -393,3 +393,6 @@ example [Decidable p] : a = true → p → decide p = a := by
 
 example [Decidable p] : false = a → ¬p → decide p = a := by
   grind
+
+example (a : Nat) (p q r : Prop) (h₁ : if _ : a < 1 then p else q) (h₂ : r) : (if a < 1 then p else q) ↔ r := by
+  grind (splits := 0)