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 : MVarId) (useClassical : Option Bool := none) : MetaM (Option 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 (attempting to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P.
• For a non-propositional goal use False.elim.

def Lean.MVarId.elabFalseOrByContra : Elab.Tactic.Tactic

Equations

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