Documentation

Mathlib.Tactic.GCongr

Setup for the gcongr tactic #

The core implementation of the gcongr ("generalized congruence") tactic is in the file Tactic.GCongr.Core. In this file we set it up for use across the library by tagging a minimal set of lemmas with the attribute @[gcongr] and by listing positivity as a first-pass discharger for side goals (gcongr_discharger).

≤, - #

<, - #

≤, + #

<, + #

≤, - #

<, - #

≤, * #

<, * #

≤, / #

theorem Nat.div_le_div {a : } {b : } {c : } {d : } (h1 : a b) (h2 : d c) (h3 : d 0) :
a / c b / d

See if the term is a ⊂ b and the goal is a ⊆ b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    <, / #

    ≤, ⁻¹ #

    ≤, ^ #

    <, ^ #

    theorem zpow_lt_of_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (hx : 1 < a) (h : m < n) :
    a ^ m < a ^ n

    coercions #

    theorem Nat.cast_le_cast {α : Type u_1} [OrderedSemiring α] [CharZero α] {x : } {y : } (h : x y) :
    x y