Documentation

Mathlib.Tactic.ApplyFun

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
        theorem Mathlib.Tactic.ApplyFun.le_of_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
        e x e yx y

        Alias of the forward direction of OrderIso.le_iff_le.

        theorem Mathlib.Tactic.ApplyFun.lt_of_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : α} :
        e x < e yx < y

        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.
          Instances For