`by_contra h` proves `⊢ p` by contradiction, introducing a hypothesis `h : ¬p` and proving `False`. - If `p` is a negation `¬q`, `h : q` will be introduced instead of `¬¬q`. - If `p` is decidable, it uses `Decidable.byContradiction` instead of `Classical.byContradiction`. - If `h` is omitted, the introduced variable will be called `this`. - `h` can be any pattern supported by `rcases`/`rintro`. # absurd-tactic absurd.{v} {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b Anything follows from two contradictory hypotheses. Example: example (hp : p) (hnp : ¬p) : q := absurd hp hnp # Lean prompt [Zaffer/lean-gpt: Pre-prompt for ChatGPT-4 AI Assistant to do Lean Theorem Prover proofs.](https://github.com/Zaffer/lean-gpt) # rcases-tactic