# Apply at #

A tactic for applying functions at hypotheses.

`apply t at i`

will use forward reasoning with `t`

at the hypothesis `i`

.
Explicitly, if `t : α₁ → ⋯ → αᵢ → ⋯ → αₙ`

and `i`

has type `αᵢ`

, then this tactic will add
metavariables/goals for any terms of `αⱼ`

for `j = 1, …, i-1`

,
then replace the type of `i`

with `αᵢ₊₁ → ⋯ → αₙ`

by applying those metavariables and the
original `i`

.

## Equations

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