mathlib documentation

tactic.apply_fun

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

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.

source
meta def tactic.apply_fun_to_goal (e : pexpr) (lem : option pexpr) :
tactic unit

Attempt to "apply" a function f represented by the argument e : pexpr to the goal.

If the goal is of the form a ≠ b, we obtain the new goal f a ≠ f b. If the goal is of the form a = b, we obtain a new goal f a = f b, and a subsidiary goal injective f. (We attempt to discharge this subsidiary goal automatically, or using the optional argument.) If the goal is of the form a ≤ b (or similarly for a < b), and f is an order_iso, we obtain a new goal f a ≤ f b.

source
meta def tactic.interactive.apply_fun (q : interactive.parse interactive.types.texpr) (locs : interactive.parse interactive.types.location) (lem : interactive.parse (lean.parser.tk "using" *> interactive.types.texpr)?) :
tactic unit

Apply a function to an equality or inequality in either a local hypothesis or the goal.

  • If we have h : a = b, then apply_fun f at h will replace this with h : f a = f b.
  • If we have h : a ≤ b, then apply_fun f at h will replace this with h : f a ≤ f b, and create a subsidiary goal monotone f. apply_fun will automatically attempt to discharge this subsidiary goal using mono, or an explicit solution can be provided with apply_fun f at h using P, where P : monotone f.
  • If the goal is a ≠ b, apply_fun f will replace this with f a ≠ f b.
  • If the goal is a = b, apply_fun f will replace this with f a = f b, and create a subsidiary goal injective f. apply_fun will automatically attempt to discharge this subsidiary goal using local hypotheses, or if f is actually an equiv, or an explicit solution can be provided with apply_fun f using P, where P : injective f.
  • If the goal is a ≤ b (or similarly for a < b), and f is actually an order_iso, apply_fun f will replace the goal with f a ≤ f b. If f is anything else (e.g. just a function, or an equiv), apply_fun will fail.

Typical usage is:

open function

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