fix: decide tactic transparency

closes #4644

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -378,7 +378,7 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     -- Get instance from `d`
     let s := d.appArg!
     -- Reduce the instance rather than `d` itself, since that gives a nicer error message on failure.
-    let r ← withDefault <| whnf s
+    let r ← withAtLeastTransparency .default <| whnf s
     if r.isAppOf ``isFalse then
       throwError "\
         tactic 'decide' proved that the proposition\

tests/lean/run/4644.lean

@@ -0,0 +1,37 @@
+-- NB: well-founded recursion, so irreducible
+def sorted_from_var [x: LE α] [DecidableRel x.le] (a: Array α) (i: Nat): Bool :=
+  if h: i + 1 < a.size then
+    have : i < a.size := Nat.lt_of_succ_lt h
+    a[i] ≤ a[i+1] && sorted_from_var a (i + 1)
+  else
+    true
+termination_by a.size - i
+
+def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
+  sorted_from_var a 0
+
+-- works (because `rfl` of closed terms resorts to kernel defeq, see #3772)
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
+  rfl
+
+/--
+error: tactic 'decide' failed for proposition
+  check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
+since its 'Decidable' instance reduced to
+  match check_sorted #[0, 3, 3, 5, 8, 10, 10, 10], true with
+  | false, false => isTrue ⋯
+  | false, true => isFalse ⋯
+  | true, false => isFalse ⋯
+  | true, true => isTrue ⋯
+rather than to the 'isTrue' constructor.
+-/
+#guard_msgs in
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
+  decide -- fails because `decide` uses `.default` transparency, and `sorted_from_var` is marked as irreducible
+
+unseal sorted_from_var in
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
+  decide -- works
+
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
+  with_unfolding_all decide -- should work