intro

In general, the intro tactic changes a goal of type P → Q into a hypothesis of type P and a goal of type Q. Here is a simple example.

try it!

example (P Q : Prop) (HQ : Q) : P → Q :=
begin
  intro HP,
  exact HQ
end

When this proof begins, the state is

P Q : Prop,
HQ : Q
⊢ P → Q

After intro HP the state is

P Q : Prop,
HQ : Q,
HP : P
⊢ Q

and the goal is then solved with the exact tactic.

∀ is a function

Terms of type ∀ x, P x can be regarded as functions which eat a variable x and spit out a proof of P x; here is an example of what this looks like.

try it!

example (X : Type) (a : X) (P : X → Prop) (H : ∀ x, P x) : P a :=
begin
  /-
  X : Type,
  a : X,
  P : X → Prop,
  H : ∀ (x : X), P x
  ⊢ P a
  -/
  exact (H a), -- H is a function; evaluate it at a
end

¬ is a function

In Lean, ¬ P is notation for not P, which is defined to mean P → false. So one can work with ¬ P as if it were a function.

try it!

example (P Q : Prop) : ¬ P → ¬ (P ∧ Q) :=
begin
  intro HnP,
    -- goal is now ⊢ ¬ (P ∧ Q)
  intro HPQ,
    -- state now
    -- HnP : ¬ P
    -- HPQ : P ∧ Q
    -- goal is ⊢ false
  apply HnP, -- think of HnP : P → false
    -- goal now P
  cases HPQ with HP HQ,
  exact HP
end