`false_or_by_contra`

tactic #

Changes the goal to `False`

, retaining as much information as possible:

- If the goal is
`False`

, do nothing. - If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is
`x ≠ y`

, introduce`x = y`

.) - Otherwise, for a propositional goal
`P`

, replace it with`¬ ¬ P`

(attempting to find a`Decidable`

instance, but otherwise falling back to working classically) and introduce`¬ P`

. - For a non-propositional goal use
`False.elim`

.

partial def
Lean.MVarId.falseOrByContra
(g : Lean.MVarId)
(useClassical : optParam (Option Bool) none)
:

Changes the goal to `False`

, retaining as much information as possible:

- If the goal is
`False`

, do nothing. - If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is
`x ≠ y`

, introduce`x = y`

.) - Otherwise, for a propositional goal
`P`

, replace it with`¬ ¬ P`

(attempting to find a`Decidable`

instance, but otherwise falling back to working classically) and introduce`¬ P`

. - For a non-propositional goal use
`False.elim`

.

## Equations

- One or more equations did not get rendered due to their size.