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
, 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 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
Equations
- One or more equations did not get rendered due to their size.