We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 1410cd8 commit b5074f0Copy full SHA for b5074f0
tests/lean/run/grind_11515.lean
@@ -3,9 +3,9 @@ example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
3
4
/--
5
info: Try these:
6
- [apply] grind only [usr Nat.div_pow_of_pos, usr Nat.mod_eq_of_lt, usr Nat.dvd_mul_right_of_dvd]
+ [apply] grind only [usr Nat.div_pow_of_pos, usr Nat.dvd_mul_right_of_dvd]
7
[apply] grind =>
8
- instantiate only [usr Nat.div_pow_of_pos, usr Nat.mod_eq_of_lt]
+ instantiate only [usr Nat.div_pow_of_pos]
9
instantiate only [usr Nat.dvd_mul_right_of_dvd]
10
lia
11
-/
0 commit comments