Lean4
/-- `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`.
-/
@[tactic_parser 1000]
public meta def tacticApply_At_ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.tacticApply_At_ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "apply" false✝) (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "at"))
(ParserDescr.const✝ `ident))
