## Game mode

All the proofs we have seen so far have been a little hard for a person to read. As mentioned, Lean can serve as an *interactive* theorem prover. There is more interactive mode to write proofs called *tactic mode*. Tactic mode also allows us to structure our proofs in more human-readable form.

To enter tactic mode, we add the keyword `by`

after the `:=`

like so.

In the Infoview pane, you will see something like

You can `sorry`

this and notice that `Goals accomplished π`

appears for the goal state; though Lean still gives a warning that we are using `sorry`

.

Inside tactic mode, you can use tactics. Each tactic is a built-in helper function for constructing a proof. Letβs look at some in an example step by step.

Suppose we wanted to prove the formula `(A β B β§ C) β (A β B) β§ (A β C)`

. We start with

and the infoview provides the current state

We have assumptions `A B C`

which are propositions and our goal is `(A β B β§ C) β (A β B) β§ (A β C)`

.

Next we would normally start with `fun (h : A β B β§ C) =>`

. In tactic mode, we can use the tactic `intro`

. When our goal is of the for `X β Y`

, `intro h`

will introduce an assumption `h : X`

and change our goal to `Y`

. Here

and the infoview provides the current state

While Lean can infer the type of `h`

from the goal, it is good practice to provide the type yourself. When you disagree with Lean, then its good chance to check your understanding.

Next we want to make proofs of `A β B`

and `A β C`

. Previously, we would jam that into an `And.intro`

making the resulting expression dense. The tactic `have`

allows us to introduce new assumptions into the context if we provide proofs.

and the infoview provides the current state

Now just need to combine `f`

and `g`

with `And.intro`

. Since `And.intro f g`

is *exactly* our goal. We use the `exact`

tactic to tell Lean.

The infoview celebrates with us: `Goals accomplished π`

.

Another useful tactic is called `apply`

. It applies a function to the goal to get a new goal. For example,

gives

in the infoview. We can tackle each `case`

.

To simplify proofs with or elimination, Lean has the tactic `cases`

.

Each line labelled with `|`

is a case of or elimination. `inl`

tells Lean you are taking the left branch of the or while `inr`

is the right.