Possible bug in `cancel` tactic?

[jdfm]

Given the ways that we see cancel being used in the book, and given some discussions in the Zulip lean community, I think maybe there is a bug in the cancel tactic.

Would the following not have allowed us to arrive at the goal x = y?

example {x y : ℝ} (hx: 0 ≤ x) (hy: 0 ≤ y) (hs: x^2 = y^2) : x = y := by
  cancel 2 at hs

The original context where I ran into this was when trying to do the following:

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
  have h3 :=
    calc
      x^2 = 4 := by rw [h1]
      _ = 2^2 := by numbers
  cancel 2 at h3

[mcol]

I had the same expectation too, and the proof mentioned above failed for me with this error, which I find rather baffling:

application type mismatch
  pow_eq_zero h3
argument
  h3
has type
  x ^ 2 = 2 ^ 2 : Prop
but is expected to have type
  x ^ 2 = 0 : Prop

[rzeta0]

I'm interested in this too.

I have a related problem:

example {x : ℝ} (hx: x^2 = 0) : x = 0 := by
  cancel x at hx

gives the error

cancel failed, could not verify the following side condition:
x : ℝ
hx : x ^ 2 = 0
⊢ 0 < x

Section 2.4.4 says

The tactic cancel will be helpful to deduce that quantities are zero when their squares are known to be zero.