Jeremy Avigad

simp * at * does not preserve validity

2

### Prerequisites * [x ] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues)....

Ideas from LFTCM

1

These are notes I wrote to myself during the meeting: - Describe the tactics `suggest` and `hint` - Talk about ctrl+space for better tab completion - `show_term` - `specialize`

choose tactic

2

There is an example of the `choose` tactic commented out in the chapter _Sets, Functions, and Relations_. We should decide whether to discuss it there or wait until a later...

From Filippo A. E. Nuccio: Add a couple of lines about apply_fun in the second section of Chapter 4, when discussing functions. It seems appropriate to be in that section,...

#121 added a comment about structural eta reduction to Chapter 6, Section 1, without explaining it.

We should set the autoImplicit flag to false, to match mathlib. See Eric Wieser's comments at #110.

The linter currently complains about unused variables e.g. in `fun a b aleb ↦ mf (mg aleb)`. We should probably explain this somewhere and then replace unused variables by underscores.

Introduce the suffices tactic somewhere

We got off to a good start with building an index, but then we fell off the wagon. We should go through systematically and add index entries.

As noted on Zulip, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/experiment.20making.20.60succ_eq_add_one.60.20.40.5Bsimp.5D.60/near/446392853.