# `qify` tactic #

The `qify` tactic is used to shift propositions from `ℕ` or `ℤ` to `ℚ`. This is often useful since `ℚ` has well-behaved division.

    example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
      qify
      qify at h
      /-
      h : ¬↑x * ↑y * ↑z < 0
      ⊢ ↑c < ↑a + 3 * ↑b
      -/
      sorry

source
def Mathlib.Tactic.Qify.qify :
Lean.ParserDescr

The `qify` tactic is used to shift propositions from `ℕ` or `ℤ` to `ℚ`. This is often useful since `ℚ` has well-behaved division.

    example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
      qify
      qify at h
      /-
      h : ¬↑x * ↑y * ↑z < 0
      ⊢ ↑c < ↑a + 3 * ↑b
      -/
      sorry

`qify` can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing `≤` arguments will allow `push_cast` to do more work.

    example (a b c : ℤ) (h : a / b = c) (hab : b ∣ a) (hb : b ≠ 0) : a = c * b := by
      qify [hab] at h hb ⊢
      exact (div_eq_iff hb).1 h

`qify` makes use of the `@[zify_simps]` and `@[qify_simps]` attributes to move propositions, and the `push_cast` tactic to simplify the `ℚ`-valued expressions.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Mathlib.Tactic.Qify.intCast_eq (a b : ℤ) :
a = b ↔ ↑a = ↑b
source
theorem Mathlib.Tactic.Qify.intCast_le (a b : ℤ) :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem Mathlib.Tactic.Qify.intCast_lt (a b : ℤ) :
a < b ↔ ↑a < ↑b
source
theorem Mathlib.Tactic.Qify.intCast_ne (a b : ℤ) :
a ≠ b ↔ ↑a ≠ ↑b