# Tactics introduced: [[Tactics/apply - tactic|apply]], [[exact - tactic|exact]], [[zSkunkworks/zA - J/__LeanNotes staging/intro - tactic|intro]] # Tactic patterns: [[intro-apply pattern|intro-apply pattern]] # Lean Note code guidelines: [Shadowed identifiers guideline](https://leannotes.wiki/Articles/Lean+Notes+code+guidelines#Shadowed+identifiers+have+single+quote+suffixes) # Credits [[Bhavik Mehta]] / [[Formalising Mathematics - Metha]] --- **Creation Date:** 2026-01-17