fix: use match with Decidable. (#7232)

This works around leanprover/lean4#2552 - fix found by @b-mehta. I changed the `Nat` instance where the issue was found, and some `List` instances in hope it fixes mysterious slowdowns with `Finset` decidability. Any more instances changed would probably be good.

Mathlib/Data/Nat/Basic.lean

@@ -934,23 +934,24 @@ end FindGreatest
 
 /-! ### decidability of predicates -/
 
+-- To work around lean4#2552, we use `match` instead of `if/casesOn` with decidable instances.
 instance decidableBallLT :
-    ∀ (n : Nat) (P : ∀ k < n, Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
-| 0, P, _ => isTrue fun n h => by cases h
-| (n+1), P, H => by
-  cases' decidableBallLT n fun k h => P k (lt_succ_of_lt h) with h h
-  · refine' isFalse (mt _ h)
-    intro hn k h
-    apply hn
-  by_cases p : P n (lt_succ_self n)
-  · exact
-      isTrue fun k h' =>
-        (le_of_lt_succ h').lt_or_eq_dec.elim (h _) fun e =>
-          match k, e, h' with
-          | _, rfl, _ => p
-  · exact isFalse (mt (fun hn => hn _ _) p)
+  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
+| 0, _, _ => isTrue fun _ => (by cases ·)
+| (n+1), P, H =>
+  match decidableBallLT n (P · <| lt_succ_of_lt ·) with
+  | isFalse h => isFalse (h fun _ _ => · _ _)
+  | isTrue h =>
+    match H n Nat.le.refl with
+    | isFalse p => isFalse (p <| · _ _)
+    | isTrue p => isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)
 #align nat.decidable_ball_lt Nat.decidableBallLT
 
+-- To verify we don't have a regression on the speed, we put a difficult example.
+-- any regression should take a huge amount of heartbeats -- we are currently at 187621.
+-- For reference, the instance using `casesOn` took 44544 for 4; this one takes 1299 for 4.
+example : ∀ a, a < 25 → ∀ b, b < 25 → ∀ c, c < 25 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide
+
 instance decidableForallFin {n : ℕ} (P : Fin n → Prop) [DecidablePred P] :
     Decidable (∀ i, P i) :=
   decidable_of_iff (∀ k h, P ⟨k, h⟩) ⟨fun a ⟨k, h⟩ => a k h, fun a k h => a ⟨k, h⟩⟩

Mathlib/Init/Data/List/Instances.lean

@@ -58,12 +58,14 @@ instance instAlternative : Alternative List.{u} where
 
 variable {α : Type u} {p : α → Prop} [DecidablePred p]
 
+-- To work around lean4#2552, we call specific `Decidable` instances and use `match` on them,
+-- as opposed to using `if`.
 instance decidableBex : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
   | []    => isFalse (by simp)
   | x::xs =>
-    if h₁ : p x
-    then isTrue ⟨x, mem_cons_self _ _, h₁⟩
-    else match decidableBex xs with
+    match ‹DecidablePred p› x with
+    | isTrue h₁ => isTrue ⟨x, mem_cons_self _ _, h₁⟩
+    | isFalse h₁ => match decidableBex xs with
       | isTrue h₂  => isTrue <| by
         cases' h₂ with y h; cases' h with hm hp
         exact ⟨y, mem_cons_of_mem _ hm, hp⟩
@@ -75,10 +77,11 @@ instance decidableBex : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
 #align list.decidable_bex List.decidableBex
 
 instance decidableBall (l : List α) : Decidable (∀ x ∈ l, p x) :=
-  if h : ∃ x ∈ l, ¬ p x then
-    isFalse $ let ⟨x, h, np⟩ := h; fun al => np (al x h)
-  else
-    isTrue $ fun x hx => if h' : p x then h' else False.elim $ h ⟨x, hx, h'⟩
+  match (inferInstance : Decidable <| ∃ x ∈ l, ¬ p x) with
+  | isFalse h => isTrue $ fun x hx => match ‹DecidablePred p› x with
+    | isTrue h' => h'
+    | isFalse h' => False.elim $ h ⟨x, hx, h'⟩
+  | isTrue h => isFalse <| let ⟨x, h, np⟩ := h; fun al => np (al x h)
 #align list.decidable_ball List.decidableBall
 
 end List