chore: add grind tests that fail with grind.debug

tests/elab/grind_ac_inv_crash_1.lean

@@ -0,0 +1,10 @@
+module
+
+open List
+
+set_option grind.debug true in
+theorem getLast_getLast_eq_getLast_flatten {l : List (List α)}
+    (hl : l ≠ []) (hl' : l.getLast hl ≠ []) :
+    (l.getLast hl).getLast hl' =
+      l.flatten.getLast (flatten_ne_nil_iff.2 ⟨_, getLast_mem hl, hl'⟩) := by
+  cases eq_nil_or_concat l with grind

tests/elab/grind_ac_inv_crash_2.lean

@@ -0,0 +1,7 @@
+public section
+
+namespace List
+
+set_option grind.debug true in
+theorem take_eq_self_iff (x : List α) {n : Nat} : x.take n = x → x.length ≤ n := by
+  grind

tests/elab/grind_def_eq_1.lean

@@ -0,0 +1,26 @@
+namespace Sigma
+
+def map (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : Sigma β₁) : Sigma β₂ :=
+  ⟨f₁ x.1, f₂ x.1 x.2⟩
+
+end Sigma
+
+public section
+
+namespace List
+
+variable {α : Type} {α' : Type} {β : α → Type} {β' : α' → Type} {l l₁ l₂ : List (Sigma β)}
+
+def keys : List (Sigma β) → List α :=
+  sorry
+
+variable [DecidableEq α] [DecidableEq α']
+
+set_option grind.debug true in
+omit [DecidableEq α] in
+theorem map₂_keys {β β' : α → Type} (f : (a : α) → β a → β' a) (l : List (Σ a, β a)) :
+    (l.map (.map id f)).keys = l.keys := by
+  induction l
+  · sorry
+  · grind [Sigma.map]
+

tests/elab/grind_eqc_check_crash_1.lean

@@ -0,0 +1,5 @@
+module
+
+set_option grind.debug true in
+theorem mwe2 (n : Nat) : [d][n]?.getD d = d := by
+  grind

tests/elab/grind_not_internalized_1.lean

@@ -0,0 +1,7 @@
+module
+
+set_option grind.debug true in
+theorem test {β α} {γ : β → Sort v} {f : α → β} {g : β → α}
+    (h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :
+    cast (congrArg (fun a ↦ γ (f a)) (h a)) (C (g (f a))) = C a := by
+  grind

tests/elab/grind_not_internalized_2.lean

@@ -0,0 +1,17 @@
+module
+
+namespace List
+
+def reverseRec {motive : List α → Sort _} (nil : motive [])
+    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : ∀ l, motive l
+  | [] => nil
+  | a :: l => (dropLast_concat_getLast (cons_ne_nil a l)) ▸
+    append_singleton _ _ ((a :: l).dropLast.reverseRec nil append_singleton)
+  termination_by l => l.length
+
+set_option grind.debug true in
+theorem reverseRec_concat {motive : List α → Sort _} (x : α) (xs : List α) (nil : motive [])
+    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
+    (xs ++ [x]).reverseRec nil append_singleton =
+    append_singleton xs x (xs.reverseRec nil append_singleton) := by
+  grind [reverseRec, cases List]

tests/elab/grind_structure_member_1.lean

@@ -0,0 +1,24 @@
+module
+
+@[expose] public section
+
+open Function
+
+structure Equiv (α : Sort _) (β : Sort _) where
+  toFun : α → β
+  invFun : β → α
+  left_inv : LeftInverse invFun toFun
+  right_inv : RightInverse invFun toFun
+
+
+infixl:25 " ≃ " => Equiv
+
+namespace Equiv
+
+set_option grind.debug true in
+protected def cast {α β : Sort _} (h : α = β) : α ≃ β where
+  toFun := cast h
+  invFun := cast h.symm
+  left_inv := by grind
+  right_inv := by grind
+