# Propose #

This file defines a tactic `have? using a, b, c`

that tries to find a lemma which makes use of each of the local hypotheses `a, b, c`

.

The variant `have? : t using a, b, c`

restricts to lemmas with type `t`

(which may contain `_`

).

Note that in either variant `have?`

does not look at the current goal at all.
It is a relative of `apply?`

but for *forward reasoning* (i.e. looking at the hypotheses)
rather than backward reasoning.

```
import Batteries.Data.List.Basic
import Mathlib.Tactic.Propose
example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
have? using w, m -- Try this: `List.disjoint_of_subset_left m w`
trivial
```

Configuration for `DiscrTree`

.

## Equations

- Mathlib.Tactic.Propose.discrTreeConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

## Instances For

Shortcut for calling `solveByElim`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Attempts to find lemmas which use all of the `required`

expressions as arguments, and
can be unified with the given `type`

(which may contain metavariables, which we avoid assigning).
We look up candidate lemmas from a discrimination tree using the first such expression.

Returns an array of pairs, containing the names of found lemmas and the resulting application.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`have? using a, b, c`

tries to find a lemma which makes use of each of the local hypotheses`a, b, c`

, and reports any results via trace messages.`have? : h using a, b, c`

only returns lemmas whose type matches`h`

(which may contain`_`

).`have?! using a, b, c`

will also call`have`

to add results to the local goal state.

Note that `have?`

(unlike `apply?`

) does not inspect the goal at all,
only the types of the lemmas in the `using`

clause.

`have?`

should not be left in proofs; it is a search tool, like `apply?`

.

Suggestions are printed as `have := f a b c`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`have? using a, b, c`

tries to find a lemma which makes use of each of the local hypotheses`a, b, c`

, and reports any results via trace messages.`have? : h using a, b, c`

only returns lemmas whose type matches`h`

(which may contain`_`

).`have?! using a, b, c`

will also call`have`

to add results to the local goal state.

Note that `have?`

(unlike `apply?`

) does not inspect the goal at all,
only the types of the lemmas in the `using`

clause.

`have?`

should not be left in proofs; it is a search tool, like `apply?`

.

Suggestions are printed as `have := f a b c`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`have? using a, b, c`

tries to find a lemma which makes use of each of the local hypotheses`a, b, c`

, and reports any results via trace messages.`have? : h using a, b, c`

only returns lemmas whose type matches`h`

(which may contain`_`

).`have?! using a, b, c`

will also call`have`

to add results to the local goal state.

Note that `have?`

(unlike `apply?`

) does not inspect the goal at all,
only the types of the lemmas in the `using`

clause.

`have?`

should not be left in proofs; it is a search tool, like `apply?`

.

Suggestions are printed as `have := f a b c`

.

## Equations

- One or more equations did not get rendered due to their size.