# Extending `have`

, `let`

and `suffices`

#

This file extends the `have`

, `let`

and `suffices`

tactics to allow the addition of hypotheses to
the context without requiring their proofs to be provided immediately.

As a style choice, this should not be used in mathlib; but is provided for downstream users who preferred the old style.

A parser for optional binder identifiers

## Equations

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

## Instances For

Retrieves the name of the optional identifier, if provided. Returns `this`

otherwise

## Equations

- Mathlib.Tactic.optBinderIdent.name id = if id.raw[0].isIdent = true then id.raw[0].getId else Lean.TSyntax.getId (Lean.HygieneInfo.mkIdent { raw := id.raw[0] } `this)

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

def
Mathlib.Tactic.haveLetCore
(goal : Lean.MVarId)
(name : Lean.TSyntax `Mathlib.Tactic.optBinderIdent)
(bis : Array (Lean.TSyntax `Lean.Parser.Term.letIdBinder))
(t : Option Lean.Term)
(keepTerm : Bool)
:

Adds hypotheses to the context, turning them into goals to be proved later if their proof terms
aren't provided (`t: Option Term := none`

).

If the bound term is intended to be kept in the context, pass `keepTerm : Bool := true`

. This is
useful when extending the `let`

tactic, which is expected to show the proof term in the infoview.

## Equations

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