mathlib documentation

If e easily implies (%%n < %%b) for some explicit b, return that proof.

If e easily implies (%%n ≥ %%b) for some explicit b, return that proof.

Combine two upper bounds.

Combine two lower bounds.

Inspect a given expression, using it to update a set of upper and lower bounds on n.

Attempt to find a lower bound for the variable n, by evaluating bot_le n.

Attempt to find an upper bound for the variable n, by evaluating le_top n.

Inspect the local hypotheses for upper and lower bounds on a variable n.

The finset of elements of a set s for which we have fintype s.

Call fin_cases on membership of the finset built from an Ico interval corresponding to a lower and an upper bound.

Here hl should be an expression of the form a ≤ n, for some explicit a, and hu should be of the form n < b, for some explicit b.

By default interval_cases_using automatically generates a name for the new hypothesis. The name can be specified via the optional argument n.

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 :=
begin
  interval_cases n,
  all_goals {simp}
end

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ set.Ico a b.

You can specify a name h for the new hypothesis, as interval_cases n with h or interval_cases n using hl hu with h.