adapt says

Author: mhuisi

Mathlib/Tactic/Says.lean

@@ -93,7 +93,9 @@ def evalTacticCapturingTryThis (tac : TSyntax `tactic) : TacticM (TSyntax ``tact
   let tryThis ← match msg.dropPrefix? "Try this:" with
   | none => throwError m!"Tactic output did not begin with 'Try this:': {msg}"
   | some S => pure S.toString.removeLeadingSpaces
-  match parseAsTacticSeq (← getEnv) tryThis.trim with
+  let tryThis := tryThis.trim
+  let tryThis := tryThis.dropPrefix? "[apply] " |>.map (·.toString) |>.getD tryThis
+  match parseAsTacticSeq (← getEnv) tryThis with
   | .ok stx => return stx
   | .error err => throwError m!"Failed to parse tactic output: {tryThis}\n{err}"