Extending replace

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

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:

f : α → β
h : α
⊢ goal

Then after replace h := f h the state will be:

f : α → β
h : β
⊢ goal

whereas have h := f h would result in:

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

This can be used to simulate the specialize and apply at tactics of Coq.

Extensions:

• replace h : t, without a subsequent proof, creates a new main goal case h : ... ⊢ t. This form is considered deprecated in Mathlib: use replace h : t := _ instead.

Equations

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