# Documentation

Mathlib.Tactic.Propose

# 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 Std.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

def Mathlib.Tactic.Propose.solveByElim (orig : Lean.MVarId) (goals : ) (use : ) (required : ) (depth : Nat) :

Shortcut for calling solveByElim.

Instances For
def Mathlib.Tactic.Propose.propose {s : Bool} (lemmas : ) (type : Lean.Expr) (required : ) (solveByElimDepth : ) :

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.

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.

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.

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.

Instances For