## Examples

Let’s do some examples of predicate logic proofs in Lean to get comfortable with the new syntax and also introduce a few more useful tactics.

First, we prove that `∀ (x : α), P x → ∃ (y : α), P y`

.

From out previous discussion, we would expect the final line to be `exact Exists.intro a h`

. Lean has a shorthard notation for intro rules. We can use French quotes (typed < >) to construct the term. Similarly, if we wanted an `And.intro a b`

, we could `⟨a, b⟩`

. Like most notation it makes thing easier to write but can also make it harder to read.

Let’s look at the proof showing we can exchange quantifiers in one direction.

Note that we can introduce multiple terms just by including a spaced list of labels for them.

Next, if there does not exist a value making the predicate true, we can conclude it is false for all values.

Below we have another example of giving proofs using quantifiers.

Let’s do a basic example using functions and equality.

There a few things to notice in this proof. First, we have `rw [←h₁]`

with the backwards ←. Lean’s convention for rewriting using `x=y`

is to search for occurrences of `x`

and replace them with `y`

. If we tried `rw [h₁]`

, then Lean would return an error

Lean allows you to rewrite hypotheses in addition to goals but you need to specify the assumption to target. The following proof is also valid.

This tells Lean to look for `x`

’s in `h₂`

and replace them with `y`

’s. In both cases, the *assumption* tactic tells Lean: one of the goals is an established fact in the context, figure out which and close the goal.

You can also feed Lean multiple terms to use for rewriting as a list.