- **`eBook:`** [Mehta - Lean 4](https://b-mehta.github.io/formalising-mathematics-notes/index.html#formalising-mathematics) [Tactics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/Part_2.html) - **`Videos:`** [Buzzard - Lean 3](https://www.youtube.com/playlist?list=PLVZep5wTamMmRPvCLO4WVpCwkTi1F6OyF) - **`Github Repos:`** [LeanNotes](https://github.com/dducoff/LeanNotes-Formalising-Mathematics-2026) [Metha](https://github.com/b-mehta/formalising-mathematics-notes) [Solution files - Metha](https://github.com/b-mehta/formalising-mathematics-notes/blob/main/FormalisingMathematics2026/Solutions/Section01logic/Sheet1.lean) ## Solutions - **`1 Logic Solutions:`** [[Courses and eBooks/Formalising Mathematics - Metha/Table of Contents#1 Logic Sheet 1|LeanNotes]] [Metha](https://github.com/b-mehta/formalising-mathematics-notes/blob/main/FormalisingMathematics2026/Solutions/Section01logic/Sheet1.lean) ### 1 Logic Sheet 1 **GitHub link to the .lean file:** [Sheet1-LeanNotes.lean](https://github.com/dducoff/LeanNotes-Formalising-Mathematics-2026/blob/main/LeanNotesFormalisingMathematics2026/Section01logic/Sheet1-LeanNotes.lean) ###### Tactics introduced ![[apply-tactic#apply *conditional*]] ![[apply-at-tactic#apply *conditional* at *premise*]] ![[Tactics/exact-tactic#exact *hypothesis*|exact-tactic]] ![[Tactics/intro-tactic#intro *conditional-premise*]] ###### LeanNotes idioms used - [[apply-at-relabeled]] : Correct the misspelled conclusion term. - [[intro-format]] : Provide a description, as needed, for each hypotheses, one per line. - [[exact-show]] : Include the `term : type` information when closing a goal. ###### Other Tactics used: - [[assumption-tactic|assumption]] : Search the hypotheses for a match with the goal. - [[assumption-loop-tactic|assumption-loop]] : Loop through subgoals to match with a hypotheses within the subgoal context. - [[clear-tactic|clear]] : Remove unused hypotheses from the local context. * [[rename'-tactic|rename']] : Rename a hypothesis. --- **`LeanNotes curator:`** [[dducoff]] **`Posted Date:`** 2026-08-11