Trying out various things with grind

Changes

1 changed files (+11/-0)

• Grind.lean (new)
  • @@ -0,0 +1,11 @@
    + import Mathlib + + -- https://lean-lang.org/doc/reference/latest//The--grind--tactic/#grind + + example (n : ℕ) (h : n > 5) : ∃ a b, 3 * a + 4 * b = n := by + use (n - (n % 3) * 4) / 3, n % 3 + grind + + example (n x y : ℕ) (h : n > x * y - x - y) (hp : gcd x y = 1) : ∃ a b, a * x + b * y = n := by + use (n - (n % x) * y) / x, n % x + grind