# 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.

Apply a function to a hypothesis.

## Equations

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

## Instances For

Failure message for `applyFunTarget`

.

## Equations

- Mathlib.Tactic.applyFunTargetFailure f = Lean.throwError (Lean.toMessageData "`apply_fun` could not apply `" ++ Lean.toMessageData f ++ Lean.toMessageData "` to the main goal.")

## Instances For

Given a metavariable `ginj`

of type `Injective f`

, try to prove it.
Returns whether it was successful.

## Equations

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

## Instances For

**Alias** of the forward direction of `OrderIso.le_iff_le`

.

**Alias** of the forward direction of `OrderIso.lt_iff_lt`

.

Apply a function to the main goal.

## Equations

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

## Instances For

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 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`StrictMono f`

and behaves as in the previous case. - 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`Injective f`

and behaves as in the previous two cases. - 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
```

The function `f`

is handled similarly to how it would be handled by `refine`

in that `f`

can contain
placeholders. Named placeholders (like `?a`

or `?_`

) will produce new goals.

## Equations

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