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. (If the goal is x ≠ y, introduce x = y.) Otherwise, for a goal P, replace it with ¬ ¬ P and introduce ¬ P.

def false_or_by_contra : Lean.ParserDescr

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 (attempt to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P. For a non-propositional goal use False.elim.

Equations

• false_or_by_contra = Lean.ParserDescr.node `false_or_by_contra 1024 (Lean.ParserDescr.nonReservedSymbol "false_or_by_contra" false)

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

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 (attempt to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P. For a non-propositional goal use False.elim.

def tacticFalse_or_by_contra : Lean.ParserDescr

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 (attempt to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P. For a non-propositional goal use False.elim.

Equations

• tacticFalse_or_by_contra = Lean.ParserDescr.node `tacticFalse_or_by_contra 1024 (Lean.ParserDescr.nonReservedSymbol "false_or_by_contra" false)