# 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? : Option Lean.Expr)
(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.