Lean4
/-- 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:
```lean
open Function
example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : Injective <| g ∘ f) :
Injective f := by
intro 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.
-/
@[tactic_parser 1000]
public meta def applyFun : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.applyFun 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "apply_fun " false✝) (ParserDescr.cat✝ `term 0))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.cat✝ `term 0))))
