# Documentation

Mathlib.Tactic.ApplyFun

# The apply_fun tactic. #

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

## Porting notes #

When the mono tactic has been ported we can attempt to automatically discharge Monotone f goals.

When Logic.Equiv.Basic and Order.Hom.Basic have been ported some additional testing is required.

def Mathlib.Tactic.applyFunHyp (f : Lean.TSyntax term) (using? : ) (h : Lean.FVarId) (g : Lean.MVarId) :

Apply a function to a hypothesis.

Equations
• One or more equations did not get rendered due to their size.

Failure message for applyFunTarget.

Equations
• One or more equations did not get rendered due to their size.

Apply a function to the main goal.

Equations
• One or more equations did not get rendered due to their size.

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 OrderIso, 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 := by
intros x x' h
apply_fun g at h
exact H h
`
Equations
• One or more equations did not get rendered due to their size.