Tariq on Nostr: Dear #lean4 #maths community, Where can I read a beginner friendly introduction to ...

Dear #lean4 #maths community,

Where can I read a beginner friendly introduction to what the "gcongr" tactic is and is not?

Genuinely I haven't found anything over the last few weeks.

( The official docs are effectively the source code annotations and birna beginner tutorial)