Importing Packages using Web-version of Lean

Stream: new members

[Mark Santa Clara Munro]

screenshotleanimport.png

When I tried to copy this from the book "Mathematics in Lean", it did not work, which makes sense because their next sentence is: "The import lines at the beginning of the associated examples file import the theory of the real numbers from Mathlib, as well as useful automation. For the sake of brevity, we generally suppress information like this in the textbook."

So, how do I know what to import and use in general and on that example?

[Shreyas Srinivas]

There's a lot that's wrong here. For starters, please copy and paste these code into a multi-line code block like below and paste it in the chat.

```
your code here
```

[Shreyas Srinivas]

This should give you what we call an #mwe and make it easier to help you

[Mark Santa Clara Munro]

import Webeditor.Tools
import Mathlib

example (a b c : R) : a * b * c = b * (a * c) := by
rw [mul_comm a b]
rw [mul_assoc b a c]

[Ruben Van de Velde]

As far as I can tell, the MIL code block has ℝ (as in, the real numbers), not R

[Mark Santa Clara Munro]

I didn't realize thank you so much

[Mark Santa Clara Munro]

In general, though, do I need to import everything or is what imported good enough?

[Shreyas Srinivas]

You don't need WebEditor.Tools 9/10 times

[Shreyas Srinivas]

and this works:

import Mathlib

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b, mul_assoc b a c]

Although the indentation is not strictly necessary, I'd recommend having it for code organisation

[Mark Santa Clara Munro]

Thank you!