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

def exactSubsetOfSSubset : Mathlib.Tactic.GCongr.ForwardExt

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.

<, /

≤, ⁻¹

≤, ^

<, ^

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