Apply a function to some local assumptions which are either equalities or inequalities. For instance, if the context contains h : a = b and some function f then apply_fun f at h turns h into h : f a = f b. When the assumption is an inequality h : a ≤ b, a side goal monotone f is created, unless this condition is provided using apply_fun f at h using P where P : monotone f, or the mono tactic can prove it.