{"textDocument": {"uri": "file:///tacticInduction.lean"},
 "position": {"line": 9, "character": 10}}
{"rendered":
 "```lean\ncase nil\nbs : List Nat\n⊢ ([].append bs).length = [].length + bs.length\n```",
 "goals":
 ["case nil\nbs : List Nat\n⊢ ([].append bs).length = [].length + bs.length"]}
{"textDocument": {"uri": "file:///tacticInduction.lean"},
 "position": {"line": 17, "character": 2}}
{"rendered": "no goals", "goals": []}