mathlib documentation


meta def tactic.apply_fun_to_hyp (e : pexpr) (mono_lem : option pexpr) (hyp : expr) :

Apply the function f given by e : pexpr to the local hypothesis hyp, which must either be of the form a = b or a ≤ b, replacing the type of hyp with f a = f b or f a ≤ f b. If hyp names an inequality then a new goal monotone f is created, unless the name of a proof of this fact is passed as the optional argument mono_lem, or the mono tactic can prove it.

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.

Typical usage is:

open function

example (X Y Z : Type) (f : X  Y) (g : Y  Z) (H : injective $ g  f) :
  injective f :=
  intros x x' h,
  apply_fun g at h,
  exact H h