feat: use try? in some grind_constProp.lean examples

tests/lean/run/grind_constProp.lean

@@ -207,6 +207,11 @@ def evalExpr (e : Expr) : EvalM Val := do
 @[grind] theorem UnaryOp.simplify_eval (op : UnaryOp) : (op.simplify a).eval σ = (Expr.una op a).eval σ := by
   grind [UnaryOp.simplify.eq_def]
 
+/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind? -/
+#guard_msgs (info) in
+example (e : Expr) : e.simplify.eval σ = e.eval σ := by
+  try?
+
 @[simp, grind =] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by
   induction e, σ using Expr.simplify.induct <;> grind
 
@@ -293,14 +298,19 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
   grind
 
 @[grind] theorem State.erase_le (σ : State) : σ.erase x ≼ σ := by
-  induction σ, x using State.erase.induct <;> grind
+  grind
 
 @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by
   induction σ₁, σ₂ using State.join.induct <;> grind
 
 @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by
   grind
 
+/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind? -/
+#guard_msgs (info) in
+example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
+  try?
+
 @[grind] theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
   induction σ₁, σ₂ using State.join.induct <;> grind