### Loogle Command Examples

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Demonstrates various ways to use the #loogle command for type pattern search, constant mention search, lemma name substring search, subexpression pattern search, and main conclusion search. It also shows how to combine filters and use non-linear patterns.

```lean
-- Search by type signature pattern
#loogle List ?a → ?a
-- Finds functions that take a List and return an element
```

```lean
-- Search by constant mention
#loogle Real.sin
-- Finds all lemmas mentioning the sine function
```

```lean
-- Search by lemma name substring
#loogle "differ"
-- Finds lemmas with "differ" in the name
```

```lean
-- Search by subexpression pattern
#loogle _ * (_ ^ _)
-- Finds lemmas involving products with powers
```

```lean
-- Search by main conclusion (using turnstile)
#loogle ⊢ tsum _ = _ * tsum _
-- Finds lemmas where the conclusion matches the pattern
```

```lean
-- Combine multiple filters with commas
#loogle Option ?a → ?a, "get!"
-- Results: Option.get! : {α : Type u} [Inhabited α] : Option α → α
```

```lean
-- Non-linear patterns with repeated metavariables
#loogle Real.sqrt ?a * Real.sqrt ?a
```

```lean
-- Term mode usage
example := #loogle List ?a → ?a
```

```lean
-- Tactic mode: filters to valid tactics for current goal
set_option loogle.queries 1

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  -- Shows applicable tactics derived from the found lemma
  sorry
```

```lean
-- Configure number of results
set_option loogle.queries 10
```

```lean
-- Custom API URL via environment variable
-- LEANSEARCHCLIENT_LOOGLE_API_URL="https://custom-server.com/json"
```

--------------------------------

### Add LeanSearchClient Dependency

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Add LeanSearchClient as a dependency in your lakefile.toml to install the library.

```toml
[[require]]
name = "LeanSearchClient"
git = "https://github.com/leanprover-community/LeanSearchClient"
```

--------------------------------

### Import LeanSearchClient in Lean Files

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Import the LeanSearchClient library in your Lean files to use its features.

```lean
import LeanSearchClient
```

--------------------------------

### Query Command

Source: https://github.com/leanprover-community/leansearchclient/blob/main/README.md

Use the #search or #leansearch command to perform a search as a top-level command.

```lean
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

```lean
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

--------------------------------

### Universal Search with #search Command

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Use the #search command for a unified interface to search backends. In tactic mode without a query, it defaults to LeanStateSearch based on the current goal.

```lean
-- Command mode: search for theorems by natural language
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

```lean
-- Term mode: use in an expression context
example := #search "Every prime greater than 2 is odd."
```

```lean
-- Tactic mode with query: search LeanSearch with natural language
example : 3 ≤ 5 := by
  #search "Natural number less than implies successor less than successor."
  sorry
```

```lean
-- Tactic mode without query: automatically searches LeanStateSearch based on goal state
example : 0 < 1 := by
  #search  -- Searches based on the goal "0 < 1"
  sorry
```

--------------------------------

### Goal-Based Premise Search with #statesearch

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Query LeanStateSearch using the current proof goal. Automatically formats and sends the goal to find relevant lemmas and tactics. Configure the Lean version/revision and number of results.

```lean
-- Configure the Lean version/revision to search against
set_option statesearch.revision "v4.22.0"

-- Configure number of results
set_option statesearch.queries 6

example : 0 < 1 := by
  #statesearch  -- Sends goal state "⊢ 0 < 1" to LeanStateSearch
  -- Results include:
  -- • #check zero_lt_one
  -- • #check one_pos
  -- • #check zero_lt_one'
  sorry
```

```lean
-- The revision must match a supported Lean version
set_option statesearch.revision "v4.15.0"  -- May error if unsupported

example : 0 ≤ 1 := by
  #statesearch  -- Error: "Lean State Search does not support the specified revision"
```

```lean
-- Custom API URL via environment variable
-- LEANSEARCHCLIENT_LEANSTATESEARCH_API_URL="https://custom-server.com/api/search"
```

--------------------------------

### LeanSearchClient Configuration Options

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Configures LeanSearchClient behavior using Lean options for number of results, backend selection, and API revision targeting. These options control the default backend and the number of results fetched from each search backend.

```lean
-- Set number of results for each backend (default 6)
set_option leansearch.queries 10
set_option loogle.queries 8
set_option statesearch.queries 5
```

```lean
-- Set the default backend for #search command
set_option leansearchclient.backend "leansearch"
```

```lean
-- Set the Lean revision for LeanStateSearch
set_option statesearch.revision "v4.22.0"
```

```lean
-- Set custom user agent string
set_option leansearchclient.useragent "MyProject"
```

```lean
-- Example: combining options for targeted search
set_option leansearch.queries 3
set_option statesearch.revision "v4.22.0"
set_option statesearch.queries 1

example : 0 < 1 := by
  #search  -- Uses statesearch with 1 result for v4.22.0
  sorry
```

--------------------------------

### Query Term

Source: https://github.com/leanprover-community/leansearchclient/blob/main/README.md

Use the #search or #leansearch command within a term definition.

```lean
example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

```lean
example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

--------------------------------

### Query Tactic

Source: https://github.com/leanprover-community/leansearchclient/blob/main/README.md

Use search commands within a tactic block to find valid tactics based on the current state or a query string.

```lean
example : 3 ≤ 5 := by
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry
```

```lean
example : 3 ≤ 5 := by
  #search
  sorry
```

```lean
example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry
```

```lean
example : 3 ≤ 5 := by
  #statesearch
  sorry
```

--------------------------------

### Loogle Search

Source: https://github.com/leanprover-community/leansearchclient/blob/main/README.md

Use the #loogle command to search for theorems or definitions in all modes.

```lean
#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry
```

--------------------------------

### LeanSearch Natural Language Search with #leansearch

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Directly query the LeanSearch API using natural language. Queries must end with a period or question mark. In tactic mode, it filters for tactics applicable to the current goal.

```lean
-- Command mode: standalone search
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
```

```lean
-- Term mode: returns suggestions for use as terms
example := #leansearch "The sum of two even numbers is even."
```

```lean
-- Tactic mode: only shows tactics valid for current goal
-- Configure number of results (default 6)
set_option leansearch.queries 3

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  -- Results show clickable suggestions like:
  -- • apply Nat.le_of_succ_le_succ
  -- • have : ∀ {n m : Nat}, LE.le n.succ m.succ → LE.le n m := Nat.le_of_succ_le_succ
  sorry
```

```lean
-- Custom API URL via environment variable
-- LEANSEARCHCLIENT_LEANSEARCH_API_URL="https://custom-server.com/search"
```

--------------------------------

### SearchResult Structure Definition

Source: https://context7.com/leanprover-community/leansearchclient/llms.txt

Defines the internal SearchResult structure used to capture search results, including name, type, documentation, and metadata. This structure is used for generating suggestions in tactic mode.

```lean
-- SearchResult fields (internal API)
structure SearchResult where
  name : String           -- Fully qualified name (e.g., "Nat.succ_le_succ")
  type? : Option String   -- Type signature
  docString? : Option String  -- Documentation string
  doc_url? : Option String    -- URL to documentation
  kind? : Option String       -- Kind (theorem, def, etc.)

-- Generated suggestions in tactic mode include:
-- • apply {name}
-- • have : {type} := {name}
-- • rw [{name}]
-- • rw [← {name}]
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.