fix: silence aesop in cfc_cont_tac (#15847)

If `aesop` fails to discharge a goal in one branch of `fun_prop`, as implemened in `cfc_cont_tac`, it can emit a warning saying it failed to close the goal. If `fun_prop (disch := aesop)` then *succeeds* in a later branch of the same call, then the proof succeeds, but the warning is still emitted, causing the file to be noisy. Even worse, because this is called as an `autoParam`, there is no syntax in the file on which to emit the warning, so it just gets emitted at the top of the file.

This changes the configuration of `aesop` to `warnOnNonterminal := false` when used in `cfc_cont_tac`.

Note: this won't affect debugging or proof writing, because in that case the user will need to disable the use of the `autoParam` anyway by writing their own terms (or `fun_prop` calls).

Mathlib/Tactic/ContinuousFunctionalCalculus.lean

@@ -26,7 +26,10 @@ macro_rules
 specifically concerning continuity of the functions involved. -/
 syntax (name := cfcContTac) "cfc_cont_tac" : tactic
 macro_rules
-  | `(tactic| cfc_cont_tac) => `(tactic| try (first | fun_prop (disch := aesop) | assumption))
+  | `(tactic| cfc_cont_tac) =>
+    `(tactic| try (first
+      | fun_prop (disch := aesop (config := {warnOnNonterminal := false}))
+      | assumption))
 
 /-- A tactic used to automatically discharge goals relating to the non-unital continuous functional
 calculus, specifically concerning whether `f 0 = 0`. -/