**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