intros

Summary

The intros tactic is a variant of the intro tactic, which can be used if the user wants to use intro several times. The tactic intros a b c is equivalent to intro a, intro b, intro c.

Examples

intros h turns

⊢ P → Q

into

h : P
⊢ Q

just as intro h would do. However

intros hP hQ hR turns

⊢ P → Q → R → S

into

hP : P
hQ : Q
hR : R
⊢ S

Similarly, intros x y z turns

⊢ ∀ (a b c : ℕ), a + b + c = c + b + a

into

x y z : ℕ
⊢ x + y + z = z + y + x

Further notes

A variant of intros is rintro, which also enables multiple intros at once, as well as allowing the user do case splits on variables.