Make try this replacement not mis-replace on lines with unicode.

It's easier to use this lsp helper (which I had previously avoided)
because the char-to-byte-offset stuff is half behind private functions
and I never remember what is actual public API...

lua/lean/widgets.lua

@@ -120,14 +120,10 @@ implement('Lean.Meta.Tactic.TryThis.tryThisWidget', function(_, props, uri)
           if not vim.api.nvim_buf_is_loaded(bufnr) then
             return
           end
-          vim.api.nvim_buf_set_text(
-            bufnr,
-            props.range.start.line,
-            props.range.start.character,
-            props.range['end'].line,
-            props.range['end'].character,
-            { each.suggestion }
-          )
+
+          ---@type lsp.TextEdit
+          local edit = { range = props.range, newText = each.suggestion }
+          vim.lsp.util.apply_text_edits({ edit }, bufnr, 'utf-16')
 
           local this_infoview = require('lean.infoview').get_current_infoview()
           local this_info = this_infoview and this_infoview.info

spec/infoview/widgets_spec.lua

@@ -77,6 +77,35 @@ describe('widgets', function()
     )
   )
 
+  it(
+    'replaces ranges without being confused by unicode',
+    helpers.clean_buffer(
+      [[
+        example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact?
+      ]],
+      function()
+        helpers.move_cursor { to = { 1, 100 } }
+        assert.infoview_contents.are [[
+          ▶ goals accomplished 🎉
+
+          ▶ suggestion:
+          exact rfl
+
+          ▶ 1:62-1:68: information:
+          Try this: exact rfl
+        ]]
+
+        infoview.go_to()
+        helpers.move_cursor { to = { 4, 1 } }
+        helpers.feed '<CR>'
+
+        assert.contents.are [[
+          example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact rfl
+        ]]
+      end
+    )
+  )
+
   it(
     'supports try this widgets with multiple suggestions',
     helpers.clean_buffer(