Documentation

Mathlib.Tactic.Replace

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
→ β
h : α
⊢ goal
⊢ goal

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

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

whereas have h := f h would result in:

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

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

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

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
→ β
h : α
⊢ β

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

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

whereas have h : β would result in:

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

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

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

f : α → β
h✝ : α
h : β
⊢ goal
→ β
h✝ : α
h : β
⊢ goal
✝ : α
h : β
⊢ goal
⊢ goal
Equations
  • One or more equations did not get rendered due to their size.