fix: add infotree context to classical tactic (#10332)

This PR ensures that the infotree recognizes `Classical.propDecidable`
as an instance, when below a `classical` tactic.

The `classical` tactic modifies the environment that the subsequent
sequence of tactics runs in (by making `Classical.propDecidable` an
instance). However, it does not add a corresponding `InfoTree.context`
node, so its effects are not visible when we want to replay a tactic
sequence (for example when running a tactic in the tactic analysis
framework). We should add a call to `Lean.Elab.withSafeInfoContext` to
remedy this issue.

There are two potential places to add this class: in the meta-level
`Lean.Elab.Tactic.classical` wrapper, or the tactic-level
`evalClassical` tactic elaborator. I chose the latter since meta-level
does not have access to info tree operations (unless we add many
parameters to `Lean.Elab.Tactic.classical`: `[MonadNameGenerator m]
[MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m]`).

A testcase that uses the tactic analysis framework is available here:
https://github.com/leanprover-community/mathlib4/pull/29501

src/Lean/Elab/Tactic/Classical.lean

@@ -30,6 +30,7 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
 
 @[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
 def evalClassical : Tactic := fun stx =>
-  classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
+  classical <| withSaveInfoContext <|
+    Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
 
 end Lean.Elab.Tactic