# Simple tactics that are used throughout Std. #

_ 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
Instances For

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.
Instances For

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 uses Decidable.byContradiction instead of Classical.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.
Instances For

Given a proof h of p, absurd h changes the goal to ⊢ ¬ p. If p is a negation ¬q then the goal is changed to ⊢ q instead.

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

split_ands applies And.intro until it does not make progress.

Equations
Instances For

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.
Instances For

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.
Instances For

Deprecated variant of trivial.

Equations
Instances For

conv tactic to close a goal using an equality theorem.

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

The conv tactic equals claims that the currently focused subexpression is equal to the given expression, and proves this claim using the given tactic.

example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
conv in (_ - _) => equals 0 =>
-- current goal: ⊢ n - n = 0
apply Nat.sub_self
-- current goal: P (fun n => 0)

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