How to use `in` keyword?

Stream: new members

[Karol Ołtarzewski]

I am trying to understand how to use in keyword.
GPT chatbot told me that "the in keyword is used in conjunction with the let keyword to define local variables within an expression."

But none of the examples that I found online seems to work. For example, if I try to test:

example : {x : nat // x = 0} :=
let x := 0 in ⟨x, rfl⟩

(from https://stackoverflow.com/a/74977875)
by just copy-pasting it to https://lean.math.hhu.de/ I get:

MathlibLatest.lean:2:11
expected ';' or line break

When I am trying to check (on my local computer) if 3 points are collinear via this code:

import Mathlib
import Mathlib.Data.Real.Basic

def collinear (p q r : ℝ × ℝ) : Prop :=
  let ⟨x1, y1⟩ := p,
      ⟨x2, y2⟩ := q,
      ⟨x3, y3⟩ := r in
  (y2-y1)/(x2-x1) = (y3-y1)/(x3-x1)

I get very similar error:

Geotest.lean:5:19
expected ';' or line break

How can I get this stuff working?

[Kevin Buzzard]

Commas are lean 3, as is nat.

[Karol Ołtarzewski]

But if try to run:

import Mathlib
import Mathlib.Data.Real.Basic

def collinear (p q r : ℝ × ℝ) : Prop :=
  let ⟨x1, y1⟩ := p in
  x1 = y1

I get identical error:

Geotest.lean:5:20
expected ';' or line break

[Ruben Van de Velde]

Remove the in altogether

[Ruben Van de Velde]

And don't trust anything gpt claims

[Chris Wong]

The error message is correct. You should use ; or a line break. Please read the error message, not GPT.

example : {x : Nat // x = 0} :=
  let x := 0; ⟨x, rfl⟩

example : {x : Nat // x = 0} :=
  let x := 0
  ⟨x, rfl⟩

[Karol Ołtarzewski]

Thanks a lot for help, so as I understand in keyword is legacy code.

[Patrick Massot]

This is not the important piece of information. The crucial thing is the advice to not trust chatgpt (or not use it at all).

[Kevin Buzzard]

one big issue with language models is that they're typically trained on Lean 3 code, and another one is that they're typically trained on far less code than is required to be accurate (because not enough Lean code exists out there).