add test file

src/Init/Data/Prod.lean

@@ -43,6 +43,7 @@ theorem map_comp_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ
 Composing a `Prod.map` with another `Prod.map` is equal to
 a single `Prod.map` of composed functions, fully applied.
 -/
+@[grind _=_]
 theorem map_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
     Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x :=
   rfl
@@ -56,19 +57,19 @@ Examples:
 -/
 @[expose] def swap : α × β → β × α := fun p => (p.2, p.1)
 
-@[simp]
+@[simp, grind =]
 theorem swap_swap : ∀ x : α × β, swap (swap x) = x
   | ⟨_, _⟩ => rfl
 
-@[simp]
+@[simp, grind =]
 theorem fst_swap {p : α × β} : (swap p).1 = p.2 :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem snd_swap {p : α × β} : (swap p).2 = p.1 :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) :=
   rfl
 

tests/lean/run/grind_prod.lean

@@ -0,0 +1,8 @@
+open Prod
+
+theorem swap_swap : ∀ x : α × β, swap (swap x) = x
+  | ⟨_, _⟩ => by grind
+
+theorem fst_swap {p : α × β} : (swap p).1 = p.2 := by grind
+
+theorem snd_swap {p : α × β} : (swap p).2 = p.1 := by grind