From 95db616cb63ed5557ebf42b6e4b1171cb6f5941c Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 20 Jun 2024 02:00:45 +0100
Subject: [PATCH] chore: cherry-pick stray test from #3850 (#4509)

#3850 included a commit that added an extra test for `exact?`, but was
otherwise unrelated the to PR. It also removed a test. I've
cherry-picked that test over, and restored the deleted test, and next
will remove the commit from #3850.
---
 tests/lean/librarySearch.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
index c762e037f4..4825837a4e 100644
--- a/tests/lean/librarySearch.lean
+++ b/tests/lean/librarySearch.lean
@@ -156,7 +156,23 @@ end synonym
 #guard_msgs in
 example : ∀ P : Prop, ¬(P ↔ ¬P) := by apply?
 
+-- Copy of P for testing purposes.
+inductive Q : Nat → Prop
+  | gt_in_head {n : Nat} : n < 0 → Q n
+
+theorem p_iff_q (i : Nat) : P i ↔ Q i :=
+  Iff.intro (fun ⟨i⟩ => Q.gt_in_head i) (fun ⟨i⟩ => P.gt_in_head i)
+
 -- We even find `iff` results:
+
+/-- info: Try this: exact (p_iff_q a).mp h -/
+#guard_msgs in
+example {a : Nat} (h : P a) : Q a := by apply?
+
+/-- info: Try this: exact (p_iff_q a).mpr h -/
+#guard_msgs in
+example {a : Nat} (h : Q a) : P a := by apply?
+
 /-- info: Try this: exact (Nat.dvd_add_iff_left h₁).mpr h₂ -/
 #guard_msgs in
 example {a b c : Nat} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b := by apply?