x^2=0 implies x=0 (`cancel` from Heather MacBeth's course)

Stream: new members

[rzeta0]

I apologise for posting a question that is about the cancel tactic which is specific to Heather Macbeth's Mechanics of Proof course.

A sub-problem to the full exercise is that I need to show $x^2=0 \implies x=0$ where $x \in \mathbb{R}$

She says specifically as an exercise hint:

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

However previous uses of cancel require the quantity being cancelled to be positive, that is more than zero.

So the following minimal example fails:

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

The error is:

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

After struggling with this for hours I'm starting to think I don't actually know what she means by "The tactic cancel will be helpful to deduce that quantities are zero when their squares are known to be zero."

[Alexander Hilbert]

#MWE please, cancel is unknown tactic to me. Maybe you can try contrapose! hx which transform to goal to x^2≠0 with hx : x≠0.

[Ruben Van de Velde]

I'm guessing that's a tactic from Heather's course