- [[apply-at-tactic|apply <Conditional> at <Premise>]] : Apply modus ponens using assumed hypotheses for the conditional and premise terms. **IDIOM:** When the [[apply-at-tactic]] refer to the LeanNotes idiom, [[apply-at-relabeled]], which corrects the misspelled conclusion term Refer to the wiki page: [[apply-tactic]] for a description and some examples. # More examples #TODO