{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 0, "character": 20}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
 "goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 0, "character": 21}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
 "goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 3, "character": 2}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
 "goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 3, "character": 3}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
 "goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 7, "character": 3}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
 "goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 10, "character": 20}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
 "goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 15, "character": 9}}
{"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",
 "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 17, "character": 5}}
{"rendered":
 "```lean\ncase succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```",
 "goals":
 ["case succ\nn✝ : Nat\nn_ih✝ : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 21, "character": 9}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
 "goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 25, "character": 3}}
{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
 "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 25, "character": 9}}
{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m\n```",
 "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 25, "character": 13}}
{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
 "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
{"textDocument": {"uri": "file://plainGoal.lean"},
 "position": {"line": 32, "character": 3}}
{"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",
 "goals": ["case zero\n⊢ 0 + Nat.zero = Nat.zero"]}