diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
index f201698022..75bd1b4a8a 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
+++ b/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
 
diff --git a/tests/lean/run/shrinkFn.lean b/tests/lean/run/shrinkFn.lean
new file mode 100644
index 0000000000..aa4e71fba6
--- /dev/null
+++ b/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