intro

Summary

The intro tactic makes progress on goals of the form ⊢ P → Q or ⊢ ∀ x, P x (where P x is any proposition that depends on x). Mathematically, it says “to prove that P implies Q, we can assume that P is true and then prove Q”, and also “to prove that P x is true for all x, we can let x be arbitrary and then prove P x.

Examples

intro h turns

⊢ P → Q

into

h : P
⊢ Q

Similarly, intro x turns

⊢  ∀ a, a + a = 2 * a

into

x : X
⊢ x + x = 2 * x

where X is the type of x and a (for example X could be the naturals or the reals, or some other type equipped with an addition and multiplication).

Details

intro works when the goal is what is known as a “Pi type”. This is a fancy computer science word for some kind of generalised function type. One Pi type goal which mathematicians often see is an implication type of the form P → Q where P and Q are propositions. The other common Pi type goal is a “for all” goal of the form ∀ a, a + a = 2 * a. Read more about Pi types in the Part B explanation of Lean’s three different types.

Variants of intro include the intros tactic (which enables you to intro several variables at once) and the rintro tactic (which enables you to do case splits on variables whilst introducing them).