exfalso
converts a goal ⊢ tgt
into ⊢ False
by applying False.elim
.
Equations
- Std.Tactic.tacticExfalso = Lean.ParserDescr.node `Std.Tactic.tacticExfalso 1024 (Lean.ParserDescr.nonReservedSymbol "exfalso" false)
_
in tactic position acts like the done
tactic: it fails and gives the list
of goals if there are any. It is useful as a placeholder after starting a tactic block
such as by _
to make it syntactically correct and show the current goal.
Equations
- Std.Tactic.tactic_ = Lean.ParserDescr.node `Std.Tactic.tactic_ 1024 (Lean.ParserDescr.nonReservedSymbol "_" false)
fail_if_success t
fails if the tactic t
succeeds.
Equations
- One or more equations did not get rendered due to their size.
rwa
calls rw
, then closes any remaining goals using assumption
.
Equations
- One or more equations did not get rendered due to their size.
Like exact
, but takes a list of terms and checks that all goals are discharged after the tactic.
Equations
- One or more equations did not get rendered due to their size.
by_contra h
proves ⊢ p
by contradiction,
introducing a hypothesis h : ¬p
and proving False
.
- If
p
is a negation¬q
,h : q
will be introduced instead of¬¬q
. - If
p
is decidable, it usesDecidable.byContradiction
instead ofClassical.byContradiction
. - If
h
is omitted, the introduced variable_: ¬p
will be anonymous.
Equations
- One or more equations did not get rendered due to their size.
iterate n tac
runs tac
exactly n
times.
iterate tac
runs tac
repeatedly until failure.
To run multiple tactics, one can do iterate (tac₁; tac₂; ⋯)
or
iterate
tac₁
tac₂
⋯
Equations
- One or more equations did not get rendered due to their size.
repeat' tac
runs tac
on all of the goals to produce a new list of goals,
then runs tac
again on all of those goals, and repeats until tac
fails on all remaining goals.
Equations
- One or more equations did not get rendered due to their size.
repeat1 tac
applies tac
to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
Equations
- One or more equations did not get rendered due to their size.
subst_eqs
applies subst
to all equalities in the context as long as it makes progress.
Equations
- Std.Tactic.tacticSubst_eqs = Lean.ParserDescr.node `Std.Tactic.tacticSubst_eqs 1024 (Lean.ParserDescr.nonReservedSymbol "subst_eqs" false)
split_ands
applies And.intro
until it does not make progress.
Equations
- Std.Tactic.tacticSplit_ands = Lean.ParserDescr.node `Std.Tactic.tacticSplit_ands 1024 (Lean.ParserDescr.nonReservedSymbol "split_ands" false)
fapply e
is like apply e
but it adds goals in the order they appear,
rather than putting the dependent goals first.
Equations
- One or more equations did not get rendered due to their size.
eapply e
is like apply e
but it does not add subgoals for variables that appear
in the types of other goals. Note that this can lead to a failure where there are
no goals remaining but there are still metavariables in the term:
example (h : ∀ x : Nat, x = x → True) : True := by
eapply h
rfl
-- no goals
-- (kernel) declaration has metavariables '_example'
Equations
- One or more equations did not get rendered due to their size.
Tries to solve the goal using a canonical proof of True
, or the rfl
tactic.
Unlike trivial
or trivial'
, does not use the contradiction
tactic.
Equations
- Std.Tactic.triv = Lean.ParserDescr.node `Std.Tactic.triv 1024 (Lean.ParserDescr.nonReservedSymbol "triv" false)
conv
tactic to close a goal using an equality theorem.
Equations
- One or more equations did not get rendered due to their size.