Error when using rewrite that solves the goal

[dranov]

@[simp] theorem size_nseq n (x : α) : size (nseq x n) = n := by
  elim: n=>[ // | n /= ->]

There is an error highlighted at -> ("no goals to be solved") and by ("unsolved goals").

However, #print size_nseq then actually prints a term without sorry, so this might be an issue just with how the errors are attributed.

I've slightly modified the code in IntroPats.lean to try to figure out what's going on:

    | `(ssrIntro| ->) => do
      let name ← fresh "H"
      run `(tactic| intros $name)
      let nGoals := (← getUnsolvedGoals).length
      dbg_trace s!"goals before rw: {nGoals}"
      run `(tactic| rw [$name:ident])
      let nGoals := (← getUnsolvedGoals).length
      dbg_trace s!"goals left after rw: {nGoals}"
      if (← getUnsolvedGoals).length != 0 then
        dbg_trace "clear"
        run `(tactic| try clear $name)

The issue doesn't seem to be related to try clear – the error shows up even if that doesn't run as in the above code.

[volodeyka]

I think we have solved this