generating lemma suggestions, given the the shortlist of candidate lemmas

def Mathlib.Tactic.ClickSuggestions.librarySearchSuggestions (rootExpr subExpr : Lean.Expr) (lctx : Lean.LocalContext) (rwKind : RwKind) (parentDecl? : Option Lean.Name) (token : ProofWidgets.RefreshToken) : ClickSuggestionsM Unit

Compute the library rearch suggestions. This uses token to incrementally udpate the output.

Equations

• One or more equations did not get rendered due to their size.