Apply at #
A tactic for applying functions at hypotheses.
apply t at i will use forward reasoning with
t at the hypothesis
t : α₁ → ⋯ → αᵢ → ⋯ → αₙ and
i has type
αᵢ, then this tactic will add
metavariables/goals for any terms of
j = 1, …, i-1,
then replace the type of
αᵢ₊₁ → ⋯ → αₙ by applying those metavariables and the
- One or more equations did not get rendered due to their size.