Add tools for searching Mathlib

Chap3.qmd

@@ -4021,7 +4021,7 @@ Usually your proof will be more readable if you use the `show` tactic to state e
 
 The `apply?` tactic has not only come up with a suggested tactic, it has applied that tactic, and the proof is now complete.  You can confirm that the tactic completes the proof by replacing the line `apply?` in the proof with `apply?`'s suggested `exact` tactic.
 
-The `apply?` tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn't.  But it is always worth a try.  Another way to try to find theorems is to visit the documentation page for Lean's mathematics library, which can be found at [https://leanprover-community.github.io/mathlib4_docs/](https://leanprover-community.github.io/mathlib4_docs/).
+The `apply?` tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn't.  But it is always worth a try.  There are also tools available on the internet for searching Lean's library, including [LeanSearch](https://leansearch.net), [Moogle](https://www.moogle.ai), and [Loogle](https://loogle.lean-lang.org). Another way to try to find theorems is to visit the documentation page for Lean's mathematics library, which can be found at [https://leanprover-community.github.io/mathlib4_docs/](https://leanprover-community.github.io/mathlib4_docs/).
 
 ### Exercises
 

docs/Chap3.html

@@ -3399,7 +3399,7 @@ <h4 class="anchored" data-anchor-id="to-use-a-given-of-the-form-x-u-p-x-2">To us
 <p>The command <code>#check @Or.comm</code> will tell you that <code>Or.comm</code> is just an alternative name for the theorem <code>or_comm</code>. So the step suggested by the <code>apply?</code> tactic is essentially the same as the step we used earlier to complete the proof.</p>
 <p>Usually your proof will be more readable if you use the <code>show</code> tactic to state explicitly the goal that is being proven. This also gives Lean a chance to correct you if you have become confused about what goal you are proving. But sometimes—for example, if the goal is very long—it is convenient to use the <code>exact</code> tactic instead. You might think of <code>exact</code> as meaning “the following is a term-mode proof that is exactly what is needed to prove the goal.”</p>
 <p>The <code>apply?</code> tactic has not only come up with a suggested tactic, it has applied that tactic, and the proof is now complete. You can confirm that the tactic completes the proof by replacing the line <code>apply?</code> in the proof with <code>apply?</code>’s suggested <code>exact</code> tactic.</p>
-<p>The <code>apply?</code> tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn’t. But it is always worth a try. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at <a href="https://leanprover-community.github.io/mathlib4_docs/">https://leanprover-community.github.io/mathlib4_docs/</a>.</p>
+<p>The <code>apply?</code> tactic is somewhat unpredictable; sometimes it is able to find the right theorem in the library, and sometimes it isn’t. But it is always worth a try. There are also tools available on the internet for searching Lean’s library, including <a href="https://leansearch.net">LeanSearch</a>, <a href="https://www.moogle.ai">Moogle</a>, and <a href="https://loogle.lean-lang.org">Loogle</a>. Another way to try to find theorems is to visit the documentation page for Lean’s mathematics library, which can be found at <a href="https://leanprover-community.github.io/mathlib4_docs/">https://leanprover-community.github.io/mathlib4_docs/</a>.</p>
 </section>
 <section id="exercises-4" class="level3">
 <h3 class="anchored" data-anchor-id="exercises-4">Exercises</h3>