The elide n (at ...) tactic hides all subterms of the target goal or hypotheses
beyond depth n by replacing them with hidden, which is a variant
on the identity function. (Tactics should still mostly be able to see
through the abbreviation, but if you want to unhide the term you can use
unelide.)
The unelide (at ...) tactic removes all hidden subterms in the target
types (usually added by elide).