congr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ HEq (f as) (f bs). The optional parameter is the depth of the recursive applications. This is useful when congr is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ x + y = y + x.

gcongr

The gcongr tactic applies "generalized congruence" rules, reducing a relational goal between a LHS and RHS matching the same pattern to relational subgoals between the differing inputs to the pattern. For example,

example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) : x ^ 2 * a + c ≤ x ^ 2 * b + d := bya:ℝb:ℝx:ℝc:ℝd:ℝh1:a + 1 ≤ b + 1h2:c + 2 ≤ d + 2⊢ x ^ 2 * a + c ≤ x ^ 2 * b + d gcongrh₁.ha:ℝb:ℝx:ℝc:ℝd:ℝh1:a + 1 ≤ b + 1h2:c + 2 ≤ d + 2⊢ a ≤ bh₂a:ℝb:ℝx:ℝc:ℝd:ℝh1:a + 1 ≤ b + 1h2:c + 2 ≤ d + 2⊢ c ≤ d ·h₁.ha:ℝb:ℝx:ℝc:ℝd:ℝh1:a + 1 ≤ b + 1h2:c + 2 ≤ d + 2⊢ a ≤ b linarithAll goals completed! 🐙 ·h₂a:ℝb:ℝx:ℝc:ℝd:ℝh1:a + 1 ≤ b + 1h2:c + 2 ≤ d + 2⊢ c ≤ d linarithAll goals completed! 🐙

This example has the goal of proving the relation ≤ between a LHS and RHS both of the pattern

x ^ 2 * ?_ + ?_

(with inputs a, c on the left and b, d on the right); after the use of gcongr, we have the simpler goals a ≤ b and c ≤ d.

A pattern can be provided explicitly; this is useful if a non-maximal match is desired:

example {a b c d x : ℝ} (h : a + c + 1 ≤ b + d + 1) : x ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := bya:ℝb:ℝc:ℝd:ℝx:ℝh:a + c + 1 ≤ b + d + 1⊢ x ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 gcongr x ^ 2 * ?_ + 5bc.ha:ℝb:ℝc:ℝd:ℝx:ℝh:a + c + 1 ≤ b + d + 1⊢ a + c ≤ b + d linarithAll goals completed! 🐙

The "generalized congruence" rules used are the library lemmas which have been tagged with the attribute @[gcongr]. For example, the first example constructs the proof term

add_le_add (mul_le_mul_of_nonneg_left _ (pow_bit0_nonneg x 1)) _

using the generalized congruence lemmas add_le_add and mul_le_mul_of_nonneg_left.

The tactic attempts to discharge side goals to these "generalized congruence" lemmas (such as the side goal 0 ≤ x ^ 2 in the above application of mul_le_mul_of_nonneg_left) using the tactic gcongr_discharger, which wraps positivity but can also be extended. Side goals not discharged in this way are left for the user.

gcongr will descend into binders (for example sums or suprema). To name the bound variables, use with:

example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
  gcongr with i
  exact h i

finiteness

Tactic to solve goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞).

mono

mono applies monotonicity rules and local hypotheses repetitively. For example,

example (x y z k : ℤ) (h : 3 ≤ (4 : ℤ)) (h' : z ≤ y) : (k + 3 + x) - y ≤ (k + 4 + x) - z := byx:ℤy:ℤz:ℤk:ℤh:3 ≤ 4h':z ≤ y⊢ k + 3 + x - y ≤ k + 4 + x - z monoAll goals completed! 🐙

fun_prop

Tactic to prove function properties

continuity

The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the continuity user attribute.

fun_prop is a (usually more powerful) alternative to continuity.

norm_num

Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.