# 2.20 Using Assumptions Effectively

An assumption is a local term that Lean may use to solve the current goal or produce another proof. In simple proofs, assumptions are often the whole proof. In larger proofs, the main work is to recognize which assumption should be applied, destructured, rewritten, or contradicted.

## Problem

You have several hypotheses in the local context, and you need to decide how to use them.

A typical context may look like this:

```lean
P Q R : Prop
hp : P
hPQ : P -> Q
hQR : Q -> R
⊢ R
```

The goal is `R`. No hypothesis has type `R` directly, but the context contains a path from `P` to `R`.

## Solution

Use assumptions according to their type.

```lean
theorem use_assumptions_chain
    (P Q R : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    R := by
  have hq : Q := hPQ hp
  exact hQR hq
```

The assumption `hp` proves `P`. The assumption `hPQ` turns `P` into `Q`. The assumption `hQR` turns `Q` into `R`.

## Direct Assumptions

If an assumption has exactly the target type, use `exact`.

```lean
theorem exact_assumption
    (P : Prop)
    (hp : P) :
    P := by
  exact hp
```

Lean also has the tactic `assumption`.

```lean
theorem assumption_tactic
    (P : Prop)
    (hp : P) :
    P := by
  assumption
```

The tactic searches the local context for a hypothesis whose type matches the goal.

## Applying Implication Assumptions

If an assumption is an implication, apply it to a proof of its premise.

```lean
theorem apply_implication_assumption
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp
```

You can also use `apply` backward.

```lean
theorem apply_backward_assumption
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  apply hPQ
  exact hp
```

After `apply hPQ`, the goal changes from `Q` to `P`.

## Destructuring Conjunction Assumptions

A conjunction assumption contains two proofs.

```lean
theorem use_and_assumption
    (P Q : Prop)
    (h : P ∧ Q) :
    Q ∧ P := by
  exact ⟨h.right, h.left⟩
```

For longer proofs, destructure it first.

```lean
theorem use_and_assumption_rcases
    (P Q : Prop)
    (h : P ∧ Q) :
    Q ∧ P := by
  rcases h with ⟨hp, hq⟩
  exact ⟨hq, hp⟩
```

This makes the context easier to read.

## Splitting Disjunction Assumptions

A disjunction assumption must be handled by cases.

```lean
theorem use_or_assumption
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq
```

A disjunction does not give both sides. It gives one side in each branch.

## Using Negated Assumptions

A negated assumption is a function into `False`.

```lean
theorem use_not_assumption
    (P R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    R := by
  have hf : False := hnp hp
  cases hf
```

The direct form is:

```lean
theorem use_not_assumption_direct
    (P R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    R := by
  exact False.elim (hnp hp)
```

Use this when contradiction is immediate.

## Using Equality Assumptions

An equality assumption rewrites the goal or another hypothesis.

```lean
theorem use_eq_assumption
    (a b : Nat)
    (hAB : a = b) :
    a + 1 = b + 1 := by
  rw [hAB]
```

Rewrite in a hypothesis when the useful fact has the wrong shape.

```lean
theorem use_eq_in_hypothesis
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  rw [hAB] at ha
  exact ha
```

## Using Universal Assumptions

A universal assumption is a function. Apply it to a value.

```lean
theorem use_forall_assumption
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (h : ∀ x : α, P x) :
    P a := by
  exact h a
```

For multiple quantifiers, apply arguments in order.

```lean
theorem use_forall_two
    (α : Type)
    (P : α -> α -> Prop)
    (a b : α)
    (h : ∀ x y : α, P x y) :
    P a b := by
  exact h a b
```

## Using Existential Assumptions

An existential assumption contains a hidden witness. Unpack it.

```lean
theorem use_exists_assumption
    (P : Nat -> Prop)
    (h : ∃ n : Nat, P n) :
    ∃ m : Nat, P m := by
  rcases h with ⟨n, hn⟩
  use n
  exact hn
```

After destructuring, the witness and its proof become ordinary assumptions.

## Combining Assumption Types

Real proofs often combine several kinds of assumptions.

```lean
theorem combined_assumption_use
    (P Q R S : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R)
    (hRS : R -> S) :
    P ∧ S := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  have hs : S := hRS hr
  exact ⟨hp, hs⟩
```

The proof first extracts useful assumptions, then applies implications, then constructs the final conjunction.

## The `assumption` Tactic

The tactic `assumption` solves a goal if the exact proposition is already present.

```lean
theorem assumption_exact
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P := by
  assumption
```

It does not apply implications automatically.

```lean
-- This does not work:
-- theorem assumption_not_enough
--     (P Q : Prop)
--     (hp : P)
--     (hPQ : P -> Q) :
--     Q := by
--   assumption
```

Here no assumption has type `Q`. You must apply `hPQ` to `hp`.

## The `first | assumption` Pattern

In larger tactic scripts, you may use `first` to try simple assumptions before other tactics.

```lean
theorem first_assumption_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · first | assumption | exact hp
  · first | assumption | exact hq
```

This is rarely needed in beginner proofs. It becomes useful when writing reusable tactic scripts.

## Avoiding Assumption Ambiguity

When several assumptions have similar types, use explicit names.

```lean
theorem explicit_assumption_choice
    (P Q : Prop)
    (hp₁ : P)
    (hp₂ : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp₁
```

Both `hp₁` and `hp₂` prove `P`, so either works. Choosing explicitly makes the proof deterministic and readable.

## Common Patterns

Use a direct hypothesis:

```lean
exact hp
```

Search for a direct hypothesis:

```lean
assumption
```

Apply an implication:

```lean
exact hPQ hp
```

Destructure conjunction:

```lean
rcases h with ⟨hp, hq⟩
```

Split disjunction:

```lean
cases h with
| inl hp => ...
| inr hq => ...
```

Use contradiction:

```lean
exact False.elim (hnp hp)
```

Rewrite with equality:

```lean
rw [hAB]
```

Apply universal hypothesis:

```lean
exact h a
```

Unpack existential:

```lean
rcases h with ⟨x, hx⟩
```

## Common Pitfalls

Do not expect `assumption` to apply implications or destructure hypotheses.

Do not use a disjunction assumption as if both sides were available.

Do not leave useful information hidden inside a conjunction or existential when the proof needs its components.

Do not rewrite with an equality before checking its direction.

Do not rely on generic names when several assumptions have similar types.

## Takeaway

An assumption is useful according to its type. Direct assumptions solve goals, implications are applied, conjunctions are projected, disjunctions are split, negations produce contradictions, equalities rewrite, universals are applied to values, and existentials are unpacked. Reading the type of each assumption determines the next proof move.