Term Mode vs. Tactic Mode

Stream: new members

[William Sealy Gosset]

When building out new areas of Mathlib, is there a preference for proofs in term mode or proofs in tactic mode?

[Mario Carneiro]

No, but most authors develop their own preference

[Mario Carneiro]

As a general rule of thumb, we use term mode for "one-liners" and tactic mode for longer proofs

[William Sealy Gosset]

@Mario Carneiro Thank you

[Ralf Stephan]

I would like to learn to use Term Mode. Which texts/exercises are recommended?

[Yaël Dillies]

#tpil

[Ralf Stephan]

All of it?

[Yaël Dillies]

No, more like Propositions and Proofs and Quantifiers and Equality

[Ralf Stephan]

Thank you.