adapt hint

Author: mhuisi

Mathlib/Tactic/Hint.lean

@@ -69,9 +69,18 @@ Extracts the `MessageData` from the first clickable `Try This:` diff widget in t
 Preserves (only) contexts and tags.
 -/
 private def getFirstTryThisFromMessage? : MessageData → Option MessageData
-  | .ofWidget w msg => if w.id == ``Meta.Hint.tryThisDiffWidget then msg else none
+  | .ofWidget w msg =>
+    if w.id == ``Meta.Hint.tryThisDiffWidget then
+      msg
+    else
+      none
   | .nest _ msg
   | .group msg => getFirstTryThisFromMessage? msg
+  | .compose (.ofWidget w _) msg =>
+    if w.id == ``Meta.Hint.textInsertionWidget then
+      msg
+    else
+      getFirstTryThisFromMessage? msg
   | .compose msg₁ msg₂ => getFirstTryThisFromMessage? msg₁ <|> getFirstTryThisFromMessage? msg₂
   | .withContext ctx msg => (getFirstTryThisFromMessage? msg).map <| .withContext ctx
   | .withNamingContext ctx msg => (getFirstTryThisFromMessage? msg).map <| .withNamingContext ctx