Is there a tutorial for basic algebra?

Stream: general

[ChosunOne]

I'm going through the Mathematics in Lean online book and starting to get a little bit lost around Section 2.3-2.4, where the exercises open up around proving stuff about min and max. Perhaps this is because you need to prove several intermediate results before you can prove the exercises. I'm also finding these sections a little difficult since you start needing to know the names of a bunch of theorems in Lean to make progress, and the apply? command is not very helpful since it returns like a hundred results. In addition, the Mathematics in Lean book has already started talking about several abstract algebraic concepts and group theory, which is a bit beyond what I am comfortable with.

I'm wondering, is there a good tutorial for doing math in lean that starts with basic algebraic manipulation in a context that might be familiar to someone with high-school algebra to intro college level math? I'm not particularly interested in proving properties of specific operators, but would like to get a feel for how to do things like multipy/divide both sides of an equation, simplify terms, add or subtract a term from both sides etc. If there isn't a good tutorial, then I would appreciate some pointers in how to achieve these things in Lean. Ultimately, I want to use Lean as a tool to learn and "check my work" as I do so.

[Kim Morrison]

@ChosunOne, have you tried going through Heather Macbeth's book https://hrmacbeth.github.io/math2001/? It may be at a more suitable level.

[ChosunOne]

Kim Morrison said:

ChosunOne, have you tried going through Heather Macbeth's book https://hrmacbeth.github.io/math2001/? It may be at a more suitable level.

I haven't seen that one! I'll go through it and see how it goes. Thanks for the recommendation.