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

replace h := e is like have h := e, but it removes a previous hypothesis of 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

The tactic specialize h a₁ ... aₙ is a way to write replace h := h a₁ ... aₙ, automatically inferring which hypothesis should be replaced.

The replace tactic can be used to simulate Rocq's apply at tactic.

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.