tutorial bugs

Stream: new members

[Matthew Pocock]

I am working through https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html and noticed that there are a bunch of links like Section Implicit Arguments, where the link is named Section * -- it doesn't flow grammatically, and looks like some template is expanding badly when rendering the documents.

[Alex J. Best]

At present it is written exactly like that in the source https://github.com/leanprover/theorem_proving_in_lean4/blob/master/interacting_with_lean.md?plain=1#L324 but that was autogenerated from the old rst version https://github.com/leanprover/theorem_proving_in_lean4/commit/82d7ca067a43e669e06f2954fc5a6acce191a682#diff-1ecebb0c2af87d51e1e3fc1e41017f5f8aa3651a91fb551a871606358090bf71 which probably explains why it looks like this

[Jason Yuen]

This link can be fixed by changing #implicit_arguments to #implicit-arguments. It may be time to contribute to https://github.com/leanprover/theorem_proving_in_lean4 again.

[Jason Yuen]

I submitted https://github.com/leanprover/theorem_proving_in_lean4/pull/73

I fixed the links, but not the grammar. I wasn't sure how to fix the grammar.