17.1. Quick Start

Availability – grind ships with Lean 4 (no extra installation) and is usable in any Lean file—just write by grind. No extra import is required beyond what your own definitions already need.
Library support – Lean’s standard library is already annotated with [grind] attributes, so common lemmas are discovered automatically. Mathlib will be annotated gradually, starting with its most frequently used theories.
First proof

example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) :
    a = c := bya:Natb:Natc:Nath₁:a = bh₂:b = c⊢ a = c
  grindAll goals completed! 🐙

This succeeds instantly using congruence closure.

Power examples – showcasing grind's satellite solvers:
- Algebraic reasoning (commutative‑ring solver):
  example [CommRing α] [NoNatZeroDivisors α] (a b c : α) : a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 → a^4 + b^4 = 9 - c^4 := byα:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors αa:αb:αc:α⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4 grind +ringAll goals completed! 🐙
- Finite‑field style reasoning (works in Fin 11):
  example (x y : Fin 11) : x^2*y = 1 → x*y^2 = y → y*x = 1 := byx:Fin 11y:Fin 11⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 grind +ringAll goals completed! 🐙
- Linear integer arithmetic with case analysis:
  example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -10 ≤ 7*x - 9*y → 7*x - 9*y ≤ 4 → False := byx:Inty:Int⊢ 27 ≤ 11 * x + 13 * y → 11 * x + 13 * y ≤ 45 → -10 ≤ 7 * x - 9 * y → 7 * x - 9 * y ≤ 4 → False grindAll goals completed! 🐙
Useful flags
- by grind (splits := 3) (ematch := 2) – limit case splits / E‑matching rounds.