Introduce new hypotheses (and apply by_contra
) until goal is of the form ... ⊢ False
Equations
- Lean.Meta.Grind.intros generation goal = do let __discr ← (Lean.Meta.Grind.intros.go generation goal).run #[] match __discr with | (fst, goals) => pure goals.toList
Instances For
Asserts a new fact prop
with proof proof
to the given goal
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Asserts next fact in the goal
fact queue.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Asserts all facts in the goal
fact queue.