why does this fail?

Stream: new members

[JK]

I would love to know what syntax I am getting wrong here:

example (a b : ℚ) (hb : b ≠ 0) : a / b = 1 ↔ a = b :=
  div_eq_one_iff_eq a hb

[JK]

(Sorry, wrong thread. There doesn't seem to be any way to delete a message?)

[JK]

I would love to know what syntax I am getting wrong here:

example (a b : ℚ) (hb : b ≠ 0) : a / b = 1 ↔ a = b :=
  div_eq_one_iff_eq a hb

[Anthony Fernandes]

Looking at the type of div_eq_one_iff_eq with #check div_eq_one_iff_eq, you can see that a and b are implicit parameters (they are in curly brackets). So you don't need to specify a and this works

import Mathlib

example (a b : ℚ) (hb : b ≠ 0) : a / b = 1 ↔ a = b :=
  div_eq_one_iff_eq hb

[JK]

Thank you. But I don't see why providing the extra parameter a makes it fail...?

[Robin Arnez]

You can "delete" messages by editing them to (deleted)

[Anthony Fernandes]

It's just invalid syntax, if you need to specify extra parameters (for example if lean is not able to find them by itself), you can use thm_name (extra_param_name := value) .... So here it would be

import Mathlib

example (a b : ℚ) (hb : b ≠ 0) : a / b = 1 ↔ a = b :=
  div_eq_one_iff_eq (a := a) hb

[JK]

OK. FWIW, the syntax with the additional parameter was what apply? suggested.

[Ruben Van de Velde]

import Mathlib

example (a b : ℚ) (hb : b ≠ 0) : a / b = 1 ↔ a = b :=
  by apply?

Output:

Try this: exact div_eq_one_iff_eq hb

[Notification Bot]

3 messages were moved here from #new members > How do tactics "reach into" quantifiers. by Ruben Van de Velde.

[Ruben Van de Velde]

Anyway, this isn't so much incorrect syntax, but passing an argument that doesn't match the function you're passing it to