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
- One or more equations did not get rendered due to their size.
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
, thenapply_fun f at h
will replace this withh : f a = f b
. - If we have
h : a ≤ b
, thenapply_fun f at h
will replace this withh : f a ≤ f b
, and create a subsidiary goalMonotone f
.apply_fun
will automatically attempt to discharge this subsidiary goal usingmono
, or an explicit solution can be provided withapply_fun f at h using P
, whereP : Monotone f
. - If we have
h : a < b
, thenapply_fun f at h
will replace this withh : f a < f b
, and create a subsidiary goalStrictMono f
and behaves as in the previous case. - If we have
h : a ≠ b
, thenapply_fun f at h
will replace this withh : f a ≠ f b
, and create a subsidiary goalInjective f
and behaves as in the previous two cases. - If the goal is
a ≠ b
,apply_fun f
will replace this withf a ≠ f b
. - If the goal is
a = b
,apply_fun f
will replace this withf a = f b
, and create a subsidiary goalinjective f
.apply_fun
will automatically attempt to discharge this subsidiary goal using local hypotheses, or iff
is actually anEquiv
, or an explicit solution can be provided withapply_fun f using P
, whereP : Injective f
. - If the goal is
a ≤ b
(or similarly fora < b
), andf
is actually anOrderIso
,apply_fun f
will replace the goal withf a ≤ f b
. Iff
is anything else (e.g. just a function, or anEquiv
),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.