"Try this" doesn't work correctly when there is an end in the line

[shingtaklam1324]

import tactic

-- Before

example (X : Type) (p : X → Prop) : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin library_search end

-- After clicking the `Try this:`

example (X : Type) (p : X → Prop) : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin exact not_forall_not.symm

It's probably to do with https://github.com/leanprover/vscode-lean/blob/master/src/tacticsuggestions.ts#L79-L109 since the current heuristics don't seem to take end into account.

---

Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/squeeze_simp.20eating.20the.20end/near/240570377