Question on real numbers error in Lean

Stream: new members

[Ryan Dau]

I am new to Lean and to Zulip, so I apologize in advance if what follows is poorly formatted or if I've misunderstood something really elementary.

I am independently working through Heather Macbeth's Mechanics of Proof to acquaint myself with Lean. When working on the following problem, Infoview says "failed to synthesize instance HDiv ℤ ℕ" for "-1/2" in the calc block. What I have written so far is given below ("numbers" is a custom tactic, but I don't think it's causing the issue and so can be ignored).

import Mathlib.Data.Real.Basic
import Library.Basic

example : ∃ x : ℝ, x < 0 ∧ x ^ 2 < 1 := by
  use -1/2
  constructor
  · numbers
  · calc
      (-1/2) ^ 2 = 1/4 := by numbers
       _ < 1/2 := by numbers

I know real numbers in Lean are not identical with floating-point numbers, which was my initial thought for what went wrong. Beyond that, though, I'm not sure how to interpret the error. Any push in the right direction would be greatly appreciated!

[Ruben Van de Velde]

First of all, calc with just a single line doesn't work

[Ryan Dau]

Oh, whoops - my apologies. Let me edit my post, I did not include everything.

[Ruben Van de Velde]

Second, you can write (-1/2 : ℝ) instead

[Robin Arnez]

The problem is that -1/2 is interpreted as integer division here and it rounds down (if the denominator is positie). So you have -1 / 2 = -1, (-1) ^ 2 = 1, 1 / 4 = 0, 1 / 2 = 0 so your first line says 1 = 0 and your second 0 < 0.

[Robin Arnez]

Ruben Van de Veldes suggestion makes it interpret them as real numbers instead of integers.

[Ryan Dau]

Ah, I see! Changing it along the lines suggested has resolved the issue. Thanks to both of you!