| [[Tactics/by_contra-tactic\|by_contra]] *contrary hypotheses* | If the goal is `⊢ P`, then **`by_contra`** `h_notP : ¬P` provides a proof by contradiction. <br>It constructs the hypothesis `h_notP : ¬P` and changes the goal to false, `⊢ False`. | | ------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | | | | ## Description - If the goal `P` is a negation, `⊢ ¬P`, the `hP : P` will be introduced instead of `h_not_notP : ¬¬P`. - The newly constructed contrary hypotheses can be any pattern supported by [[rcases-tactic|rcases]] or [[rintro-tactic|rintro]]`. --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-19