mathlib documentation

tactic.elide

source
meta def tactic.elide.replace  :
ℕ → expr → tactic expr
source
meta def tactic.elide.unelide (e : expr) :
expr
source
meta def tactic.interactive.elide (n : interactive.parse lean.parser.small_nat) (loc : interactive.parse interactive.types.location) :
tactic unit

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.)

source
meta def tactic.interactive.unelide (loc : interactive.parse interactive.types.location) :
tactic unit

The unelide (at ...) tactic removes all hidden subterms in the target types (usually added by elide).