### Get Setup File Path

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Module.html

Determines the file path for the setup JSON file of a module.

```lean
@[inline]
def Lake.Module.setupFile (self : Module) : System.FilePath
Equations
  * self.setupFile = Lake.Module.irPath "setup.json" self
```

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

### Print Prefix Command Example

Source: https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/PrintPrefix.html

Prints all definitions that start with the 'List' namespace.

```Lean
#print prefix List
```

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

### Start an HTTP/1.1 Server

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Http.html

This snippet shows how to start an HTTP/1.1 server using `Std.Http.Server.serve`. You need to implement the `Std.Http.Server.Handler` type class to define how the server handles requests. This example uses a simple handler that returns 'Hello, World!'.

```Lean
import Std.Http

open Std Async
open Std Http Server

structure MyHandler

instance : Handler MyHandler where
  onRequest _ req := do
    Response.ok |>.text "Hello, World!"

def main : IO Unit := Async.block do
  let addr : Net.SocketAddress := .v4 ⟨.ofParts 127 0 0 1, 8080⟩
  let server ← Server.serve addr MyHandler.mk
  server.waitShutdown

```

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

### List.inits Example

Source: https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/List/Basic.html

Generates all initial segments of a list. Used to get prefixes of a list.

```Lean
inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]
```

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

### Example: Set equality tautology

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates proving a set equality tautology using `tauto_set`.

```lean
example {α} (A B C : Set α) (h1 : A ⊆ B ∪ C) : (A ∩ B) ∪ (A ∩ C) = A :=
  by
  tauto_set
```

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

### Start Loading References

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Server/Watchdog.html

Starts loading .ileans from the search path asynchronously to avoid blocking server startup. Users may receive incomplete results during this process.

```Lean
def Lean.Server.Watchdog.startLoadingReferences (referenceData : Std.Mutex ReferenceData) :
IO Unit
```

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

### Get Character at Start Position

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Basic.html

Retrieves the character at the start position of a non-empty string, using the `get` method.

```Lean
theorem String.get_startPos {
  b : String
} (h : b.startPos ≠ b.endPos) :
  b.startPos.get h = b.toList.head ⋯
```

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

### Lake.Module.setupFile

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Module.html

Returns the file path for the module's setup configuration file (setup.json).

```APIDOC
## Lake.Module.setupFile

### Description
Returns the file path for the module's setup configuration file (setup.json).

### Method
N/A (Function Call)

### Endpoint
N/A

### Parameters
#### Path Parameters
N/A

#### Query Parameters
N/A

#### Request Body
N/A

### Request Example
N/A

### Response
#### Success Response
- **return value** (System.FilePath) - The file path to the setup.json file.
```

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

### Get Syntax Start Position

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html

Gets the starting position of the syntax element. If `canonicalOnly` is true, synthetic nodes are ignored. Defaults to `false`.

```lean
def Lean.Syntax.getPos? (stx : Syntax) (canonicalOnly : Bool := false) :
Option String.Pos.Raw
Get the starting position of the syntax, if possible. If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying position information.
Equations
  * stx.getPos? canonicalOnly = stx.getHeadInfo.getPos? canonicalOnly
```

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

### Mapping Get over Forward Positions from Start

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Lemmas/Iterate.html

Relates the result of mapping the `get` operation over all positions starting from `s.startPos` to the `toList` representation of the entire slice.

```Lean
theorem String.Slice.Model.map_get_positionsFrom_startPos {s : Slice} :
List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom s.startPos) = s.copy.toList
```

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

### mstart Tactic for Stateful Proofs

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Starts the stateful proof mode of `Std.Do.SPred`. It transforms a stateful goal `H ⊢ₛ T` into `⊢ₛ H → T`, allowing `mintro` to re-introduce `H` with a name. Often, `mintro` can be used directly as it attempts `mstart` automatically.

```Lean
mstart
```

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

### Get Start Position of HeaderSyntax

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Import.html

Retrieves the starting position of a HeaderSyntax object.

```Lean
def Lean.Elab.HeaderSyntax.startPos (header : HeaderSyntax) :
String.Pos.Raw
Equations
  * header.startPos = header.raw.getPos?.getD 0
```

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

### List All Options with #help option

Source: https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/HelpCmd.html

Use `#help option` to list all defined options in the current environment. Each option is displayed with its type, default value, and a description. Modified options show their current value.

```lean
option pp.all : Bool := false
  (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names,
  universe, and disable beta reduction and notations during pretty printing
```

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

### Get Lake Installation Details

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the detected Lake installation information.

```APIDOC
## GET /api/lake/install

### Description
Get the detected Lake installation.

### Method
GET

### Endpoint
/api/lake/install

### Response
#### Success Response (200)
- **home** (string) - The root directory of the Lake installation.
- **srcDir** (string) - The source directory of the Lake installation.
- **libDir** (string) - The Lean library directory of the Lake installation.
- **lake** (string) - The path to the `lake` binary.
```

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

### Example: Set inclusion tautology

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates proving a set inclusion tautology using `tauto_set`.

```lean
example {α} (A B C D : Set α) (h1 : A ⊆ B) (h2 : C ⊆ D) : C \ B ⊆ D \ A :=
  by
  tauto_set
```

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

### Get Lake Installation

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/InstallPath.html

Heuristically validates if `getLakeBuildHome?` points to a proper Lake installation by checking for `Lake.olean` in the installation's `lib` directory.

```Lean
def Lake.getLakeInstall? (lake : System.FilePath) :
  BaseIO (Option LakeInstall)
```

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

### Example of expand_binders% usage

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Util/Notation3.html

Demonstrates how `expand_binders%` expands binders into nested combinators, similar to Lean 3's `∃` notation.

```Lean
def Mathlib.Notation3.«termExpand_binders%(_=>_)_,_» : Lean.ParserDescr
Expands binders into nested combinators. For example, the familiar exists is given by: `expand_binders% (p => Exists p) x y : Nat, x < y` which expands to the same expression as `∃ x y : Nat, x < y`
```

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

### Configure SolveByElim to intro goals before applying lemmas

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/SolveByElim.html

The `intros` configuration calls `intro` on each goal before applying lemmas. This can help simplify goals before further processing.

```Lean
def Lean.Meta.SolveByElim.SolveByElimConfig.intros (cfg : SolveByElimConfig := { }) :
SolveByElimConfig
```

```Lean
cfg.intros = cfg.mainGoalProc fun (g : Lean.MVarId) => do let __do_lift ← g.intro1P pure [__do_lift.snd]
```

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

### Create GET Request Builder

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Http/Data/Request.html

Creates a new HTTP GET Request builder with the specified URI. Use this to start building a GET request.

```lean
def Std.Http.Request.get (uri : RequestTarget) :
Builder
Creates a new HTTP GET Request with the specified URI.
Equations
  * Std.Http.Request.get uri = (Std.Http.Request.new.method Std.Http.Method.get).uri uri
```

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

### TCP Socket Server Example

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Http/Server/Connection.html

Demonstrates how to create a TCP socket server, bind it to an address, listen for connections, and handle incoming clients in a background task.

```Lean
-- Create a TCP socket server instance
let server ← Socket.Server.mk
server.bind addr
server.listen backlog

-- Enter an infinite loop to handle incoming client connections
while true do
  let client ← server.accept
  background (serveConnection client handler config)
```

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

### Getting Start Position from Info

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Server/InfoUtils.html

Safely retrieves the starting position of the syntax associated with an `Info` object.

```Lean
def Lean.Elab.Info.pos? (i : Info) : Option String.Pos.Raw
Equations
  * i.pos? = i.stx.getPos? true
```

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

### Lean.MVarId.intros

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Intro.html

Introduce as many binders as possible.

```APIDOC
## Lean.MVarId.intros

### Description
Introduce as many binders as possible without unfolding definitions.

### Parameters
#### Path Parameters
- **mvarId** (MVarId) - Required - The goal identifier.

### Response
- **Array FVarId × MVarId** - Returns the array of new FVarIds and the updated MVarId.
```

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

### Elan Installation Path Information

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/InstallPath.html

Defines the structure for holding information about a local Elan setup, including installation directories.

```Lean
structure Lake.ElanInstall :
Type
Information about the local Elan setup.
  * home : System.FilePath
  * elan : System.FilePath
  * binDir : System.FilePath
  * toolchainsDir : System.FilePath
```

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

### Example of IO.println Specialization Key

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Compiler/LCNF/Specialize.html

Illustrates the constructed key for a specialized IO.println application, showing replaced arguments.

```Lean
@IO.println Nat instToStringNat lcErased lcErased
```

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

### Get Start Position of SearchStep

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Pattern/Basic.html

Defines the `startPos` function to extract the starting position from a `SearchStep`. This function works for both `rejected` and `matched` steps, returning the stored start position.

```lean
@[inline]
def String.Slice.Pattern.SearchStep.startPos {s : Slice} (st : SearchStep s) :
s.Pos
The start position of a `SearchStep`.
Equations
  * (String.Slice.Pattern.SearchStep.rejected startPos endPos).startPos = startPos
  * (String.Slice.Pattern.SearchStep.matched startPos endPos).startPos = startPos
```

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

### Get Lake Installation Details

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the detected Lake installation configuration. This function requires a monadic context with `MonadLakeEnv` and `Functor` instances.

```Lean
@[inline]
def Lake.getLakeInstall {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] :
m LakeInstall
Get the detected Lake installation.
Equations
  * Lake.getLakeInstall = (fun (x : Lake.Env) => x.lake) <$> Lake.getLakeEnv
```

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

### Configure SolveByElim to intro goals after no lemmas apply

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/SolveByElim.html

The `introsAfter` configuration calls `intro` on any goal for which no lemma applies. This is useful for simplifying goals that were not directly solved by lemma application.

```Lean
def Lean.Meta.SolveByElim.SolveByElimConfig.introsAfter (cfg : SolveByElimConfig := { }) :
SolveByElimConfig
```

```Lean
cfg.introsAfter = cfg.withDischarge fun (g : Lean.MVarId) => do let __do_lift ← g.intro1P pure (some [__do_lift.snd])
```

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

### Example Function f(x) = floor(x) - fractional_part(x)

Source: https://leanprover-community.github.io/mathlib4_docs/Archive/Imo/Imo2024Q6.html

Provides an example of a function `f(x) = ⌊x⌋ - Int.fract x` over rational numbers. This function is shown to achieve the maximum possible number of distinct values for `f(r) + f(-r)`.

```Lean
def Imo2024Q6.fExample (x : ℚ) :
ℚ
-- An example of a function achieving the maximum number of values of `f(r)+f(-r)`.
Equations
  * Imo2024Q6.fExample x = ↑⌊x⌋ - Int.fract x
```

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

### Get Start Position of String Slice

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Defs.html

Returns the start position of a string slice, which is always at offset 0 and is a valid position within the slice.

```Lean
@[inline]
def String.Slice.startPos (s : Slice) :
s.Pos
The start position of `s`, as an `s.Pos`.
Equations
  * s.startPos = { offset := 0, isValidForSlice := ⋯ }
```

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

### Linear Integer Arithmetic (LIA) Examples

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates using the 'grind' tactic with its integrated LIA solver for various integer arithmetic problems, including equalities, inequalities, and divisibility.

```lean
example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
  grind
```

```lean
example {x y : Int} :
    2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
  grind
```

```lean
example (a b : Int) :
    2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
  grind
```

```lean
example (x y : Int) :
    27 ≤ 11*x + 13*y →
    11*x + 13*y ≤ 45 →
    -10 ≤ 7*x - 9*y →
    7*x - 9*y ≤ 4 → False := by
  grind
```

```lean
example (a b c : UInt64)
    : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
  grind
```

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

### Lean.MVarId.intros!

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Lean/Meta.html

Repeatedly applies intro to a goal.

```APIDOC
## Lean.MVarId.intros!

### Description
Applies `intro` repeatedly until it fails, allowing for unfolding of definitions (e.g., `¬p` to `p → False`).

### Method
MetaM

### Parameters
- **mvarId** (MVarId) - Required - The target metavariable goal.
```

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

### Lean Parser: Example Command

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Command.html

Parses the 'example' command for providing examples.

```Lean
def Lean.Parser.Command.example : Parser := parser! `example
```

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

### Example of mySum with mvcgen invariant suggestion

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html

An example demonstrating the 'invariants?' feature of mvcgen with a custom function 'mySum'. The suggested invariant is a starting point and may require interpolation.

```Lean
def mySum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for x in l do
    acc := acc + x
  return acc

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/ 
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen invariants?
  all_goals admit
```

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

### List.tails Example

Source: https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/List/Basic.html

Generates all terminal segments of a list. Used to get suffixes of a list.

```Lean
tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]
```

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

### Lean mspecialize Tactic Example 2

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html

This example demonstrates `mspecialize` with multiple arguments, showing how to specialize a hypothesis using values from both pure and stateful contexts.

```lean
example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ
```

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

### Introduce Single Binder and Clear

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Intro.html

Given a goal `... |- β → α`, returns a goal `... ⊢ α`. This is equivalent to `intro h; clear h` but avoids appending to the local context.

```Lean
def Lean.MVarId.intro1_ (mvarId : MVarId) :
MetaM MVarId
```

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

### GET /List.finRange

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/FinRange.html

Retrieves a list of all elements of Fin n in order, starting from 0.

```APIDOC
## GET /List.finRange

### Description
Generates a list of all elements of `Fin n` in order, starting at `0`.

### Method
GET

### Parameters
#### Query Parameters
- **n** (Nat) - Required - The upper bound for the finite type Fin n.

### Response
#### Success Response (200)
- **result** (List (Fin n)) - A list containing all elements of Fin n.

### Response Example
{
  "result": [0, 1]
}
```

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

### Lean Tactic: Intro with Pattern Matching

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Tactic.html

Shows how to use the 'intro' tactic to introduce hypotheses and pattern match them. This is useful for deconstructing data structures like pairs.

```Lean
-- ... ⊢ α × β → ...
intro (a, b)
-- ..., a : α, b : β ⊢ ...
```

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

### Get Lake Source Directory

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the source directory of the detected Lake installation.

```APIDOC
## GET /api/lake/src-dir

### Description
Get the source directory of the detected Lake installation.

### Method
GET

### Endpoint
/api/lake/src-dir

### Response
#### Success Response (200)
- **srcDir** (string) - The source directory of the Lake installation.
```

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

### String.foldl Example 3

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Iterate.html

Demonstrates String.foldl to build a new string.

```lean
"coffee tea water".foldl (·.push ·) "" = "coffee tea water"
```

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

### Example with Division and Simplifier

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/FDeriv/Basic.html

Shows how to use the simplifier for a function involving division, requiring an explicit proof that the denominator does not vanish.

```lean
example (x : ℝ) (h : 1 + sin x ≠ 0) : DifferentiableAt ℝ (fun x ↦ exp x / (1 + sin x)) x := by
  simp [h]
```

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

### Get Lake Home Directory

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the root directory of the detected Lake installation.

```APIDOC
## GET /api/lake/home

### Description
Get the root directory of the detected Lake installation (e.g., `LAKE_HOME`).

### Method
GET

### Endpoint
/api/lake/home

### Response
#### Success Response (200)
- **home** (string) - The root directory of the Lake installation.
```

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

### Algebraic Solver (Ring) Examples

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Showcases the 'grind' tactic's algebraic solver for polynomial equations over commutative rings, semirings, and fields, including examples with built-in types and field inverses.

```lean
example [CommRing α] (x : α) : (x + 1) * (x - 1) = x^2 - 1 := by
  grind
```

```lean
-- Characteristic 256 means 16 * 16 = 0.
example [CommRing α] [IsCharP α 256] (x : α) :
    (x + 16) * (x - 16) = x^2 := by
  grind
```

```lean
-- Works on built-in rings such as `UInt8`.
example (x : UInt8) : (x + 16) * (x - 16) = x^2 := by
  grind
```

```lean
example [CommRing α] (a b c : α) :
    a + b + c = 3 →
    a^2 + b^2 + c^2 = 5 →
    a^3 + b^3 + c^3 = 7 →
    a^4 + b^4 = 9 - c^4 := by
  grind
```

```lean
example [Field α] [NoNatZeroDivisors α] (a : α) :
    1 / a + 1 / (2 * a) = 3 / (2 * a) := by
  grind
```

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

### Fail If No Progress Tactic Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Shows how to use `fail_if_no_progress` to ensure that a sequence of tactics makes some demonstrable progress.

```Lean
fail_if_no_progress tacs
```

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

### Get element from range'

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Range.html

Retrieves the i-th element of a range starting at n with length m.

```lean
theorem List.getElem_range'_1 {n m : ℕ} (i : ℕ) (H : i < (range' n m).length) :
(range' n m)[i] = n + i
```

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

### Lean.Meta.Sym.intros

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Sym/Intro.html

Introduces leading binders from the goal's target type, optionally using provided names.

```APIDOC
## Lean.Meta.Sym.intros

### Description
Introduces leading binders (universal quantifiers and let-expressions) from the goal's target type. If `names` is non-empty, introduces at most `names.size` binders. If `names` is empty, introduces all leading binders using inaccessible names.

### Parameters
#### Arguments
- **mvarId** (MVarId) - Required - The goal to process.
- **names** (Array Name) - Optional - Names to use for the introduced binders.

### Response
- **IntrosResult** - Returns `.goal newDecls mvarId` containing new free variable IDs and the updated goal, or `.failed` if no new declaration was introduced.
```

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

### Match Scalars Example 2

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Illustrates match_scalars with multiple atoms and different coefficients, resulting in multiple goals.

```Lean
example [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :
    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
  match_scalars
  -- two goals:
  -- `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom)
  -- `⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom)
```

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

### String.Slice.Model.map_get_revPositionsFrom_endPos

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Lemmas/Iterate.html

Maps the `get` operation over the positions returned by `revPositionsFrom` starting from the end position of a slice.

```Lean
theorem String.Slice.Model.map_get_revPositionsFrom_endPos {
  s : Slice
} :
List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.revPositionsFrom s.endPos) = s.copy.toList.reverse
```

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

### Run SimpAll Tactic at Each Proof Step

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/TacticAnalysis/Declarations.html

Configures the `tryAtEachStepSimpAll` linter to run `simp_all` at every proof step and report where it succeeds.

```Lean
def tryAtEachStepSimpAll :
Mathlib.TacticAnalysis.Config
```

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

### Get Lake Binary Path

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the path of the `lake` binary in the detected Lake installation.

```APIDOC
## GET /api/lake/binary

### Description
Get the path of the `lake` binary in the detected Lake installation.

### Method
GET

### Endpoint
/api/lake/binary

### Response
#### Success Response (200)
- **lake** (string) - The path to the `lake` binary.
```

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

### Using linarith with configuration options

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates how to use the linarith tactic with custom configuration for discharging, transparency, hypothesis splitting, and exfalso behavior.

```Lean
linarith (config := { discharger := sorry, transparency := .all, splitHypotheses := true, splitNe := true, exfalso := false, minimize := false })
```

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

### Using existsi with rfl

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Shows how to use the `existsi` tactic to instantiate existential quantifiers in a goal. This example instantiates the existential variable with `42` and then uses `rfl` to prove the resulting equality.

```Lean
example : ∃ x : Nat, x = x :=
by
  existsi 42
  rfl
```

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

### Peel Tactic Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

This example demonstrates the `peel` tactic's ability to handle complex quantifier structures involving `∀` and `∃`, showing the transformation of the tactic state.

```lean
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε
```

```lean
peel h with ε hε N n hn h_peel
```

```lean
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
ε : ℝ
hε : 0 < ε
N n : ℕ
hn : N ≤ n
h_peel : 1 / (n + 1 : ℝ) < ε
⊢ 1 / (n + 1 : ℝ) ≤ ε
```

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

### Creating First Calc Step View

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Calc.html

Elaborates the initial step of a 'calc' proof into a CalcStepView. This is the entry point for processing 'calcFirstStep' syntax.

```Lean
def Lean.Elab.Term.mkCalcFirstStepView (step0 : TSyntax `Lean.calcFirstStep) :
TermElabM CalcStepView
Equations
  * One or more equations did not get rendered due to their size.
```

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

### Get Lake Library Directory

Source: https://leanprover-community.github.io/mathlib4_docs/Lake/Config/Monad.html

Retrieves the Lean library directory of the detected Lake installation.

```APIDOC
## GET /api/lake/lib-dir

### Description
Get the Lean library directory of the detected Lake installation.

### Method
GET

### Endpoint
/api/lake/lib-dir

### Response
#### Success Response (200)
- **libDir** (string) - The Lean library directory of the Lake installation.
```

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

### Example of change? tactic

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates how to use the `change?` tactic to suggest explicit `change` syntax. It unifies a term with the current goal and provides the necessary `change` command.

```Lean
example : (fun x : Nat => x) 0 = 1 := by
  change? 0 = _  -- `Try this: change 0 = 1`

```

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

### Providing Review Feedback

Source: https://leanprover-community.github.io/contribute/pr-review.html

An example of a constructive review comment suggesting style guide adherence.

```markdown
In case you're unaware, please familiarize yourself with the mathlib
[style guide](https://leanprover-community.github.io/contribute/style.html).
You need spaces around `*`, `:` at the end of the line and the `rw` to 
be on the same line.
```

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

### Lean.MVarId.intro

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Intro.html

Introduce one binder using a specific name.

```APIDOC
## Lean.MVarId.intro

### Description
Introduce one binder using `name` as the new hypothesis name.

### Parameters
#### Path Parameters
- **mvarId** (MVarId) - Required - The goal identifier.
- **name** (Name) - Required - The name for the new hypothesis.

### Response
- **FVarId × MVarId** - Returns the new FVarId and the updated MVarId.
```

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

### Example of find tactic

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Illustrates the `find` tactic, which searches for applicable definitions and theorems for the current goal. The output lists potential candidates like `True.intro` and `trivial`.

```lean
example : True := by
  find
  -- True.intro: True
  -- trivial: True
  -- ...
```

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

### Using eapply with rfl

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates the use of `eapply` which is similar to `apply` but does not add subgoals for variables in other goals. This example shows a case where `eapply` can lead to a state with no goals but remaining metavariables.

```Lean
example (h : ∀ x : Nat, x = x → True) : True :=
by
  eapply h
  rfl
  -- no goals
-- (kernel) declaration has metavariables '_example'
```

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

### Introduce binders with intros

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Sym/Intro.html

Introduces leading binders from the goal's target type, optionally using provided names.

```lean
def Lean.Meta.Sym.intros (mvarId : MVarId) (names : Array Name := #[]) :
SymM IntrosResult
```

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

### Get positions from a starting position in a string slice

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Iterate.html

Creates an iterator over the valid positions within a string slice, starting at a specified position. The iterator yields positions that are not equal to the end position of the slice.

```lean
def String.Slice.positionsFrom {s : Slice} (p : s.Pos) : Std.Iter { p : s.Pos // p ≠ s.endPos }
Creates an iterator over the valid positions within `s`, starting at `p`.
Equations
  * String.Slice.positionsFrom p = { internalState := { currPos := p } }
```

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

### Proving an equality using linear_combination

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Example of using the linear_combination tactic to prove an equality by expressing it as a linear combination of hypotheses.

```Lean
example {a b : ℚ} (h1 : a = 1) (h2 : b = 3) : (a + b) / 2 = 2 := by
  linear_combination (h1 + h2) / 2
```

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

### nth_rewrite Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates rewriting the 2nd and 3rd occurrences of an expression using nth_rewrite.

```Lean
example (h : a = 1) : a + a + a + a + a = 5 := by
  nth_rewrite 2 3 [h]
/- 
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/ 

```

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

### Match Scalars Example 1

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates basic usage of match_scalars for a linear combination of terms with the same atom.

```Lean
example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  match_scalars
  -- one goal: `⊢ a * 1 + b * 1 = (b + a) * 1`
```

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

### Using casesm* for Case Splits with Patterns

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

This example shows how to use `casesm*` with patterns to destruct conjunctions and disjunctions. It clears specific hypotheses and then proceeds with trivial cases, similar to `cases_type*` but with pattern matching.

```lean
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```

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

### Interval Cases Analysis Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

The `interval_cases` tactic splits goals based on upper and lower bounds of a variable. This example shows splitting a goal for a natural number `n` bounded by `n ≥ 3` and `n < 5`.

```Lean
example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := by
  interval_cases n
  all_goals simp
```

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

### Get Initial Heartbeats

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Util/Heartbeats.html

Returns the current `initHeartbeats` value. This represents the starting number of heartbeats for a computation.

```Lean
def Lean.getInitHeartbeats :
CoreM Nat
Returns the current `initHeartbeats`.
Equations
  * Lean.getInitHeartbeats = do let __do_lift ← read pure __do_lift.initHeartbeats
```

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

### GCongr Tactic Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates the use of the `gcongr` tactic to prove inequalities involving functions, particularly when dealing with binders like supremum.

```Lean
example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
  gcongr with i
  exact h i
```

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

### Field Simp Tactic Example 2

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates `field_simp` clearing denominators in a field equality, simplifying the expression before further proof.

```Lean
-- `field_simp` will clear the `x` denominators in the following equation
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  field_simp
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
  sorry
```

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

### Std.Http.Server.new

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Http/Server.html

Creates a new `Server` structure with optional configuration and a listening socket address. This is the entry point for initializing the server.

```APIDOC
## Std.Http.Server.new

### Description
Create a new `Server` structure with an optional configuration.

### Signature
def Std.Http.Server.new (config : Config := { }) (localAddr : Option Net.SocketAddress := none) : IO Server
```

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

### String.Model.map_get_positionsFrom_of_splits

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Lemmas/Iterate.html

Maps the `get` operation over positions from `positionsFrom` when the starting position splits the string into two parts.

```Lean
theorem String.Model.map_get_positionsFrom_of_splits {
  s : String
} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) :
List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom p) = t₂.toList
```

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

### Using cases' for disjunctions

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates the use of the cases' tactic to split a disjunction (p ∨ q). It shows how to name the resulting hypotheses and provides equivalent examples using the preferred cases and rcases tactics.

```Lean
example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq
```

```Lean
example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq
```

```Lean
example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq
```

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

### Configure SimpAll Linter for tryAtEachStep

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/TacticAnalysis/Declarations.html

Enables running the `simp_all` tactic at every step in proofs and reporting successes.

```Lean
opaque linter.tacticAnalysis.tryAtEachStepSimpAll :
Lean.Option Bool
```

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

### Get Current Option Name of ConfigItem

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/ConfigEval/Basic.html

Gets the current name of the option after any shifting. For example, if an option is named `a.b.c.d` and there is a handler for `a.b.*`, then the handler receives a `ConfigItem` whose current option name is `c.d`.

```Lean
def Lean.Elab.ConfigEval.ConfigItem.getCurrOptionName (item : ConfigItem) :
Name
Gets the current name of the option after any shifting. For example, if an option is named `a.b.c.d` and there is a handler for `a.b.*`, then the handler receives a `ConfigItem` whose current option name is `c.d`.
Equations
  * item.getCurrOptionName = List.foldl Lean.Name.appendCore Lean.Name.anonymous (List.map (fun (x : Lean.Syntax) => x.getId) item.optionComps)
```

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

### Match Scalars Example 3

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Shows match_scalars handling of negative coefficients and different scalar types.

```Lean
example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
    -(2:R) • a • x = a • (-2:ℤ) • x := by
  match_scalars
  -- one goal: `⊢ -2 * (a * 1) = a * (-2 * 1)`
```

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

### Get First Character of Substring.Raw

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Substring.html

Returns the first character in the substring. If the substring is empty but its start position is valid, the character at that start position is returned. Otherwise, a fallback character 'A' is returned. Does not panic. This is a legacy API.

```lean
def Substring.Raw.front (s : Raw) : Char
Returns the first character in the substring.
If the substring is empty, but the substring's start position is a valid position in the underlying string, then the character at the start position is returned. If the substring's start position is not a valid position in the string, the fallback value `(default : Char)`, which is `'A'`, is returned. Does not panic.
Equations
  * s.front = s.get 0
```

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

### Using intros with Let-bindings

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html

Shows how `intros` handles hypotheses introduced by `let`-bindings. The tactic state displays the bound variables `n` and `k` with their values. This example is self-contained.

```lean
example : let n := 1; let k := 2; n + k = 3 := by
  intros
  /- n✝ : Nat := 1
     k✝ : Nat := 2
     ⊢ n✝ + k✝ = 3 -/
  rfl
```

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

### nth_rewrite Order of Precedence Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Illustrates the importance of order of precedence when using nth_rewrite with multiple rules.

```Lean
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c

```

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

### Using cases_type* for Case Splits

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

This example demonstrates how to use `cases_type*` to destruct all conjunctions and disjunctions in the context. It clears specific hypotheses and then proceeds with trivial cases.

```lean
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```

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

### Contradiction Tactic Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Demonstrates the use of the `existsi` tactic to provide existential witnesses and `rfl` to prove reflexivity.

```Lean
example : ∃ x : Nat, ∃ y : Nat, x = y := by
  existsi 42, 42
  rfl
```

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

### Fail Tactic Example

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Illustrates how to use the `fail` tactic to explicitly cause a tactic to fail with a custom error message.

```Lean
fail "This tactic always fails."
```

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

### Using qify to shift propositions to ℚ

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Illustrates the use of `qify` to rewrite goals and hypotheses by shifting propositions involving `ℕ` or `ℤ` to `ℚ`. This example shows `qify` applied to both the main goal and a specific hypothesis.

```Lean
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  qify
  qify at h
  /- 
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/ 
  sorry

```

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

### Lean.Lsp.LeanILeanHeaderSetupInfoParams Structure

Source: https://leanprover-community.github.io/mathlib4_docs/Lean/Data/Lsp/Internal.html

Contains status information about `lake setup-file` and direct imports for `$/lean/ileanHeaderSetupInfo` watchdog notifications.

```APIDOC
## Lean.Lsp.LeanILeanHeaderSetupInfoParams

### Description
Used in the `$/lean/ileanHeaderSetupInfo` watchdog <- worker notifications. Contains status information about `lake setup-file` and the direct imports of the file managed by a worker.

### Fields
- **version** (Nat) - Version of the file these imports are from.
- **isSetupFailure** (Bool) - Whether setting up the header using `lake setup-file` has failed.
- **directImports** (Array ImportInfo) - Direct imports of this file.

### Instances
- Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams
- Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams
```

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

### String.Model.map_get_positionsFrom_startPos

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Lemmas/Iterate.html

Maps the `get` operation over all positions starting from `s.startPos`, resulting in the string's entire list of characters.

```Lean
theorem String.Model.map_get_positionsFrom_startPos {
  s : String
} :
List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom s.startPos) = s.toList
```

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

### Pure Function Examples

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html

Provides examples of using the `pure` function with different types like `Option`, `Except`, and `StateM`.

```lean
(pure "hello" : Option String) = some "hello"
```

```lean
(pure "hello" : Except (Array String) String) = Except.ok "hello"
```

```lean
(pure "hello" : StateM Nat String).run 105 = ("hello", 105)
```

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

### String.Pos.prev? API

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Lemmas/FindPos.html

Provides functions to get the previous position of a string position, handling the start position case.

```APIDOC
## GET /api/string/pos/prev?

### Description
Retrieves the previous position of a given string position. Returns `some` the previous position if it exists, otherwise `none`.

### Method
GET

### Endpoint
`/api/string/pos/prev?`

### Parameters
#### Query Parameters
- **s** (String) - Required - The string containing the position.
- **p** (s.Pos) - Required - The current position within the string.

### Response
#### Success Response (200)
- **result** (Option<s.Pos>) - The previous position or none if at the start.

#### Response Example
```json
{
  "result": "some(prev_pos_value)"
}
```

#### Error Response (400)
- **error** (string) - Description of the error.

#### Response Example
```json
{
  "error": "Invalid position"
}
```
```

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

### Field Simp Tactic Example 1

Source: https://leanprover-community.github.io/mathlib4_docs/tactics.html

Shows how `field_simp` normalizes expressions by rewriting them to a common denominator, clearing denominators in inequalities.

```Lean
-- `x / (1 - y) / (1 + y / (1 - y))` is reduced to `x / (1 - y + y)`
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
    ⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
  field_simp
  -- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
  sorry
```