Hidden goal

Stream: general

[Patrick Johnson]

Just discovered this:

import tactic

example {f : ℚ → ℚ} {a : ℚ} {n : ℕ}
  (h₁ : ∀ {a b : ℚ}, b ≠ 0 → a * b / b = a)
  (h₂ : ∀ {a b : ℚ}, b ≠ 0 → a / b * b = a)
  (h₃ : (n : ℚ) ≠ 0)
  (h₄ : f (a / n) * n = f (a / n * n)) :
  f (a / n) = f a / n :=
begin
  rw h₂ at h₄,
  replace h₄ : f (a / n) * n / n = f a / n,
  { exact congr_fun (congr_arg has_div.div h₄) n },
  rw h₁ h₃ at h₄; assumption,
  assumption,
end

After replace {...} only 1 goal is displayed. Then rw creates one extra goal, which is 2 goals in total and ;assumption should close both goals. However, it seems like the second goal remains hidden and it needs to be closed with additional assumption. Is this a bug?

[Ruben Van de Velde]

I suspect that this is expected behaviour in the sense that one of the new goals doesn't count as a goal produced by this tactic as understood by the semicolons combinator

[Patrick Johnson]

Everything after replace {...} is a distraction. We can see that before replace there are 2 goals. Tactic replace creates additional goal, so 3 goals in total. Then, after {...} only 1 goal remains. That doesn't make sense to me.

[Eric Wieser]

Try adding some skips

[Eric Wieser]

; makes the goal view behave strangely at the previous comma