ink

def «tacticDwi{_}» : Lean.ParserDescr

dwi t (deal with it) is a tactic that runs t and then tries to solve the goal using contradiction, assumption, simp, and simpa.

Equations

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