fix: add expected type hint

Other tactics (e.g., `simp_all`) may try to infer the type of the
proof, and `Nat.Linear.eq_of_toNormPoly_eq` has a messy resulting type.

src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean

@@ -22,7 +22,7 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let r ← c₂.toArith ctx
     if r != e then
       let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
-      return some (r, p)
+      return some (r, ← mkExpectedTypeHint p (← mkEq e r))
     else
       return none
 

tests/lean/run/shrinkFn.lean

@@ -0,0 +1,9 @@
+abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x }
+
+class Sampleable (α : Type u) [SizeOf α] where
+  shrink : shrinkFn α := fun _ => []
+
+def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := fun (fst, snd) =>
+  let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨.mk x snd, by simp_all_arith⟩
+  let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨.mk fst x, by simp_all_arith⟩
+  shrink1 ++ shrink2