dunfold in lean4

Stream: lean4

[Felipe]

How are typeclass methods unfolded in tactic mode in lean4? It seems in lean3 dunfold would handle that. E.g., how to show that Nat.succ Nat.zero - 1 is just Nat.zero?