mathlib documentation

core / init.meta.comp_value_tactics

meta constant mk_nat_val_ne_proof  :
meta constant mk_nat_val_lt_proof  :
meta constant mk_nat_val_le_proof  :
meta constant mk_fin_val_ne_proof  :
meta constant mk_char_val_ne_proof  :
meta constant mk_string_val_ne_proof  :
meta constant mk_int_val_ne_proof  :

Close goals of the form n ≠ m when n and m have type nat, char, string, int or subtypes {i : ℕ // p i}, and they are literals. It also closes goals of the form n < m, n > m, n ≤ m and n ≥ m for nat. If the goal is of the form n = m, then it tries to close it using reflexivity.