**GitHub LeanNotes annotated solutions .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>]] : If - a conditional term is assumed, and - the goal is its conclusion type, - then change the goal to its premise type, so that it suffices to prove the premise. - [[apply-at-tactic|apply <Conditional> at <Premise>]] : Apply modus ponens when hypotheses for the conditional and premise terms are available. - [[Tactics/exact-tactic|exact]] : If a hypotheses has the type defined in the goal, then close the goal. - [[Tactics/intro-tactic|intro]] : Reduce a conditional goal to its conclusion by assuming its premises. # 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. # See also: [Tactics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/Part_2.html) [Formalising Mathematics - Mehta Lean 4](https://b-mehta.github.io/formalising-mathematics-notes/index.html#formalising-mathematics) [Original solutions file - Metha](https://github.com/b-mehta/formalising-mathematics-notes/blob/main/FormalisingMathematics2026/Solutions/Section01logic/Sheet1.lean) [[LeanNotes coding style]] # Credits [[Bhavik Mehta]] / [[Formalising Mathematics - Metha]] [[dducoff]] / LeanNotes author --- Author: [[dducoff]] Posted Date: 2026-06-26