[[apply-relabeling]] : Correct the mislabeled conclusion term after applying Modus Ponens. The [[apply-at-tactic|apply-at]] tactic invokes modus ponens, `P → Q, P ⊢ Q`, but unfortunately, it mislabels the conclusion term. BEFORE the `apply`tactic is invoked, all of the term labels align with their types: `hPimpQ : P → Q` `hP : PremiseType` When the `apply at` tactic is invoked: `apply hPimpQ at hP` Then the resulting the premise term mislabels a witness of the conclusion type: <font color="#ff0000">hP</font> `: Q ` This mislabeling is corrected by applying the [[rename'-tactic|rename']] tactic immediately after the `apply` tactic: `apply hPimpQ at hP`<font color="#00b050">; rename' (hP : Q) => hQ</font> So, now the conclusion term has a corrected label: `hQ : Q` --- **`LeanNotes curator:`** [[dducoff]] **`Posted Date:`** 2026-08-11