strange behavior of `erw`

Stream: lean4

[Junyan Xu]

When porting homotopy groups to mathlib4 I observed the following strange behavior of erw:

theorem homotopicFrom (i : N) {p q : Ω^ N X x} :
    (toLoop i p).Homotopic (toLoop i q) → Homotopic p q := by
  refine' Nonempty.map fun H => ⟨⟨homotopyFrom i H, _, _⟩, _⟩
  pick_goal 3
  · rintro t y ⟨j, jH⟩
    erw [homotopyFrom_apply]

After the refine' there are three goals, and I pick the third to work on. After the · only goal 3 appears, as expected, but after the erw, goal 1 and 2 reappear in the scope. Any idea why this happens? I'm unable to minimize this further, since the following behaves normally:

import Mathlib.Tactic.PermuteGoals

example : 1 + 1 = 1 := by
  cases Classical.em (0 = 0)
  pick_goal 2
  · erw [eq_comm]
    -- case inl doesn't appear here
    sorry
  sorry

So I guess you will have to check out my branch at !4#4939 (look here specifically) to further investigate this.

(Update: I realize this probably has nothing to do with pick_goal)