cases tactic needs to check full body before updating infoview

Prerequisites

• [ X] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [X ] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ X] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The cases tactic seems to need to check the full proof of its body until the infoview shows any intermediate goals, altough it seems that all the neccessary information is already there.
This produces considerable slow downs when writing proofs if the rest of the body is slow
or the editing breaks proofs below which makes them time out (e.g. a grind).

The same behaviour applies to the suggestions of try? in such a cases.
The error-lens extension shows that a proof has already been found, but one doesn't get the suggestion pop-up
until the full body is elaborated.

Steps to Reproduce

/- Issue:
   In the following, modify the simp to make it recheck, then put your cursor on
   the next line.
   `Expected behaviour`: The infoview updates almost immediately.
   `Current behaviour`: All the proof steps below the cursor are checked, and
   only when this is finished (after the 8 second sleep) the infoview updates.
   This can take a very long time when developing real world proofs. -/

/-- This structure only exsists, to produce a `cases` in the following proof. -/
structure myNat where
  num : Nat

theorem slow1 (m : myNat): True := by
  rcases m with num
  have : True := by simp
  -- <-- put cursor here after modifing the `simp` above to recheck
  sleep 8000
  exact this

-- /-- Without cases, it is fast. -/
-- theorem fast1 (m : myNat): True := by
--   have : True := by simp
--   -- <-- put cursor here after modifing the `simp` above to recheck
--   sleep 8000
--   exact this

-- /-- rcases doesn't have this problem. -/
-- theorem fast2 (m : myNat): True := by
--   rcases m with num
--   have : True := by simp
--   -- <-- put cursor here after modifing the `simp` above to recheck
--   sleep 8000
--   exact this


-- /-- A variation on slow1. -/
-- theorem slow2 : True := by
--   have : True ∨ True := by sorry
--   cases this with
--   | inl h =>
--     simp
--     -- <-- put cursor here after modifing the `simp` above to recheck
--   | inr h =>
--     sleep 8000
--     simp

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal slow1 reproduction and compare it with the fast1 and fast2 variations. Trace the cases tactic and infoview update path, including the related try? suggestion behavior described in the issue. Done means intermediate goals and suggestions appear without waiting for the later sleep 8000 or other downstream proof steps.