dsimp% […] t runs dsimp […] on term t. If t is a proof, then it runs dsimp […] on the type of t instead.

For instance, instead of

have foo := ...
dsimp at foo
rw [foo]

one can do rw [dsimp% foo].

def Mathlib.Tactic.dsimpPercent : Lean.ParserDescr

dsimp% […] t runs dsimp […] on term t. If t is a proof, then it runs dsimp […] on the type of t instead.

For instance, instead of

have foo := ...
dsimp at foo
rw [foo]

one can write rw [dsimp% foo].

def Mathlib.Tactic.dsimpPercentElaborator : Lean.Elab.Term.TermElab

dsimp% […] t runs dsimp […] on term t. If t is a proof, then it runs dsimp […] on the type of t instead.

For instance, instead of

have foo := ...
dsimp at foo
rw [foo]

one can write rw [dsimp% foo].