I noticed notations can be treated differently. For example < is just notation for a regular definition and unfold "<" does work as in the following example:
Theorem a : 4 < 5.
Proof.
unfold "<".
However, <= is notation associated with the type le and for some reason unfold "<=" doesn't work, as in the following example:
Theorem a : 4 <= 5
Proof.
unfold "<=".
which fails with Unable to interpret "<=" as a reference.
Can I convert 4 <= 5 into le 4 5 with some ltac command?
Adding to Anton's answer: If you already know how the notation is defined and only want to make it visible in the goal, you could do something like
Definition make_visible {X} (f : X) := f.
Notation "` f" := (make_visible f) (at level 5, format "` f").
Tactic Notation "unfold" "notation" constr(f) :=
change f with (`f).
Tactic Notation "fold" "notation" constr(f) :=
unfold make_visible.
Theorem a : 4 <= 5.
Proof.
unfold notation le.
fold notation le.
(Edit: My first solution was Definition make_visible {X} (f : X) := (fun _ => f) tt., but, as Anton pointed out, this is easier.)