# Extending `replace` #

This file extends the `replace` tactic from `Batteries` 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.

source
def Mathlib.Tactic.replace' :
Lean.ParserDescr

Acts like `have`, but removes a hypothesis with the same name as this one if possible. For example, if the state is:

Then after `replace h : β` the state will be:

    case h
    f : α → β
    h : α
    ⊢ β

    f : α → β
    h : β
    ⊢ goal

whereas `have h : β` would result in:

    case h
    f : α → β
    h : α
    ⊢ β

    f : α → β
    h✝ : α
    h : β
    ⊢ goal

Equations

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

Instances For