How does a noob learn to write tactics?

Stream: new members

[ROCKY KAMEN-RUBIO]

MWE:

 example : can_write_tactics Rocky := sorry,

More Context
I want to learn how to write tactics. I have ideas for tactics that could be useful, and it seems like tactic writing is a scarce skill in the community. I've read the tactic writing guide a few times, but a lot of it still goes over my head. I don't have an extensive background in functional programming or type theory. Are there any other resources I should look at? Should I wait until I understand Lean better by writing more proofs? General advice for learning how to write tactics? I've heard a chapter of Mathematics in Lean will cover tactic writing eventually.

[Bryan Gin-ge Chen]

There's some more info on tactic writing in the Hitchhiker's guide. I can't say what will make you into a tactic writer since I'm not such a person myself, but I've certainly learned a lot from studying the code of various tactics in core Lean and mathlib.

[Scott Morrison]

Start reading the source code of tactic implemented in mathlib.

[Scott Morrison]

Start telling us (here, for example), ideas for new tactics, and we can tell you "sounds hard"/"ill-specified"/"sounds like a good first project". :-)

[Kevin Buzzard]

Write some simple examples. Write an assumption tactic. Go through the logic solver example in Programming In Lean and fix it up!