# 1.18 Basic Tactic Mode

Tactic mode is an interactive way to build proofs. Instead of writing a proof term directly, you write commands that transform the current goal into simpler goals. Lean checks that the final result is still a proof term of the required proposition.

## Problem

You want to prove simple propositions by inspecting the goal, introducing assumptions, applying known facts, and closing goals step by step.

## Solution

Use `by` to enter tactic mode.

```lean id="sywljd"
theorem identity_example (P : Prop) : P -> P := by
  intro h
  exact h
```

The theorem states that every proposition implies itself. After `intro h`, the local context contains:

```text id="qrg6sb"
P : Prop
h : P
```

and the goal is:

```text id="exlggf"
P
```

The tactic `exact h` closes the goal because `h` has exactly the required type.

## Goals

A goal is the proposition Lean still needs to prove. In tactic mode, the editor displays the current goal and local context.

For example:

```lean id="dqd9wz"
theorem example_goal (P Q : Prop) : P -> Q -> P := by
  intro hp
  intro hq
  exact hp
```

After the two introductions, the context contains:

```text id="db4xdq"
P Q : Prop
hp : P
hq : Q
```

and the goal is:

```text id="m0nrsh"
P
```

The proof closes with `hp`.

## `intro`

The `intro` tactic introduces a hypothesis or parameter.

```lean id="stn02z"
theorem imp_chain (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hpq
  intro hqr
  intro hp
  exact hqr (hpq hp)
```

Each `intro` removes one leading implication or universal quantifier from the goal and adds a named object to the context.

## `exact`

The `exact` tactic closes the goal with a term whose type matches the goal.

```lean id="dci94y"
theorem exact_example (P : Prop) (h : P) : P := by
  exact h
```

If the goal is `P`, then `exact h` succeeds precisely when `h : P`.

## `apply`

The `apply` tactic uses a theorem or function backward.

```lean id="pym34v"
theorem apply_example (P Q : Prop) (hpq : P -> Q) (hp : P) : Q := by
  apply hpq
  exact hp
```

After `apply hpq`, Lean changes the goal from `Q` to `P`, because `hpq` can prove `Q` if given a proof of `P`.

This is backward reasoning: choose a rule that can prove the current goal, then prove its premises.

## `assumption`

The `assumption` tactic searches the local context for a hypothesis that matches the goal.

```lean id="rl3md1"
theorem assumption_example (P : Prop) (h : P) : P := by
  assumption
```

This succeeds because `h : P` is already available.

Use `assumption` when the goal is directly present in the context.

## `constructor`

The `constructor` tactic splits goals whose proof is built by a constructor.

```lean id="gz2o69"
theorem and_intro_example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq
```

The goal `P ∧ Q` becomes two goals:

```text id="dq3d2r"
P
Q
```

The bullets mark the separate subproofs.

## `cases`

The `cases` tactic performs case analysis on data or proofs.

```lean id="z5dw8n"
theorem and_elim_left (P Q : Prop) (h : P ∧ Q) : P := by
  cases h with
  | intro hp hq =>
      exact hp
```

A proof of `P ∧ Q` contains a proof of `P` and a proof of `Q`. The `cases` tactic exposes both components.

For disjunction:

```lean id="cq3wed"
theorem or_comm_example (P Q : Prop) : P ∨ Q -> Q ∨ P := by
  intro h
  cases h with
  | inl hp =>
      right
      exact hp
  | inr hq =>
      left
      exact hq
```

Each branch handles one constructor of the disjunction.

## `left` and `right`

The tactics `left` and `right` choose a side of a disjunction.

```lean id="zl3fba"
theorem left_example (P Q : Prop) (hp : P) : P ∨ Q := by
  left
  exact hp
```

```lean id="zmfo0r"
theorem right_example (P Q : Prop) (hq : Q) : P ∨ Q := by
  right
  exact hq
```

Use these when the goal is an `Or`.

## `have`

The `have` tactic creates an intermediate fact.

```lean id="f5qpi9"
theorem have_example (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) (hp : P) : R := by
  have hq : Q := hpq hp
  have hr : R := hqr hq
  exact hr
```

This makes the proof readable by naming each step.

## `show`

The `show` tactic changes the displayed goal to an equivalent target.

```lean id="woc2rp"
theorem show_example (P : Prop) (h : P) : P := by
  show P
  exact h
```

In simple examples this looks redundant, but it is useful when Lean displays a reducible expression and you want to state the intended goal explicitly.

## `rw`

The `rw` tactic rewrites using equalities.

```lean id="mzum7v"
theorem rw_example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]
```

The equality `h : a = b` replaces `a` with `b`.

## `simp`

The `simp` tactic simplifies expressions using definitional reduction and registered simplification lemmas.

```lean id="l6e55n"
theorem simp_example (n : Nat) : n + 0 = n := by
  simp
```

Use `simp` for standard simplifications. Use `rw` when you want a specific rewrite.

## Combining Tactics

A proof often combines several small tactics.

```lean id="w2q54l"
theorem combined_example (P Q R : Prop)
    (hp : P) (hq : Q) : (P ∧ Q) ∨ R := by
  left
  constructor
  · exact hp
  · exact hq
```

This proof first chooses the left side of the disjunction, then constructs the conjunction.

## Tactic Blocks Produce Terms

A tactic proof is still a term.

```lean id="g9gqg5"
theorem tactic_term_example (P : Prop) : P -> P := by
  intro h
  exact h
```

The corresponding term proof is:

```lean id="ybesza"
theorem term_example (P : Prop) : P -> P :=
  fun h => h
```

Both declarations have the same type:

```lean id="fpcgir"
#check tactic_term_example
#check term_example
```

## Common Pitfalls

If `exact h` fails, check whether the type of `h` exactly matches the goal.

If `apply f` creates unexpected goals, inspect the type of `f`.

If `constructor` creates several goals, use bullets to keep them separated.

If `cases h` removes a hypothesis, remember that it replaces the original object with its constructor fields.

If `simp` closes too much or changes the goal unexpectedly, use `rw` for more control.

## Recipe: Prove by Goal Reduction

Start with the goal:

```lean id="r7v35q"
theorem recipe (P Q : Prop) : P -> Q -> P ∧ Q := by
```

Introduce assumptions:

```lean id="cnzv47"
  intro hp
  intro hq
```

Split the conjunction:

```lean id="do2497"
  constructor
```

Solve each subgoal:

```lean id="wnfn4d"
  · exact hp
  · exact hq
```

Full proof:

```lean id="glghjs"
theorem recipe (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp
  intro hq
  constructor
  · exact hp
  · exact hq
```

## Takeaway

Tactic mode is a controlled proof construction process. Each tactic transforms the current goal or uses information from the context. Basic tactics such as `intro`, `exact`, `apply`, `constructor`, `cases`, `rw`, and `simp` are enough to write many small proofs and to understand the shape of larger ones.