Lean 4 Documentation

https://imperialcollegelondon.github.io/FLT/docs/
Admin
Comprehensive documentation for Lean 4, including the Mathlib mathematics library, standard...
Tokens:23,875,762
Snippets:155,955
Trust Score:9.7
Update:6 months ago
Show doc for...
Tokens:
Raw
### Parse Example Command

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Parser/Command.html

Parses the `example` command for providing examples.

```Lean
def Lean.Parser.Command.example :
Parser
Equations
  * One or more equations did not get rendered due to their size.
```

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

### Lean Installation Directories and Binaries

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Config/Monad.html

Provides functions to get paths for Lean's library, include directory, system library directory, and the 'lean' and 'leanc' binaries.

```APIDOC
## GET /lean/lib-dir

### Description
Returns the Lean library directory of the detected Lean installation.

### Method
GET

### Endpoint
/lean/lib-dir

### Response
#### Success Response (200)
- **filePath** (System.FilePath) - The path to the Lean library directory.

#### Response Example
{
  "filePath": "/path/to/lean/lib"
}

## GET /lean/include-dir

### Description
Returns the C include directory of the detected Lean installation.

### Method
GET

### Endpoint
/lean/include-dir

### Response
#### Success Response (200)
- **filePath** (System.FilePath) - The path to the Lean include directory.

#### Response Example
{
  "filePath": "/path/to/lean/include"
}

## GET /lean/system-lib-dir

### Description
Returns the system library directory of the detected Lean installation.

### Method
GET

### Endpoint
/lean/system-lib-dir

### Response
#### Success Response (200)
- **filePath** (System.FilePath) - The path to the Lean system library directory.

#### Response Example
{
  "filePath": "/path/to/lean/system/lib"
}

## GET /lean/binary

### Description
Returns the path of the `lean` binary in the detected Lean installation.

### Method
GET

### Endpoint
/lean/binary

### Response
#### Success Response (200)
- **filePath** (System.FilePath) - The path to the `lean` binary.

#### Response Example
{
  "filePath": "/path/to/lean/bin/lean"
}

## GET /leanc/binary

### Description
Returns the path of the `leanc` binary in the detected Lean installation.

### Method
GET

### Endpoint
/leanc/binary

### Response
#### Success Response (200)
- **filePath** (System.FilePath) - The path to the `leanc` binary.

#### Response Example
{
  "filePath": "/path/to/lean/bin/leanc"
}
```

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

### mvcgen Invariant Suggestion Example

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Shows how to use `invariants?` with mvcgen to get invariant suggestions. The suggested invariant is a starting point and may require user 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
```

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

### Retrieve Lean Installation Details

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Config/Monad.html

Functions to access Lean installation paths and directories.

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

```Lean
@[inline]
def Lake.getLeanSysroot {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] :
m System.FilePath
Returns the root directory of the detected Lean installation.
Equations
  * Lake.getLeanSysroot = (fun (x : Lake.LeanInstall) => x.sysroot) <$> Lake.getLeanInstall
```

```Lean
@[inline]
def Lake.getLeanSrcDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] :
m System.FilePath
Returns the Lean source directory of the detected Lean installation.
Equations
  * Lake.getLeanSrcDir = (fun (x : Lake.LeanInstall) => x.srcDir) <$> Lake.getLeanInstall
```

```Lean
@[inline]
def Lake.getLeanLibDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] :
m System.FilePath
Returns the Lean library directory of the detected Lean installation.
Equations
  * Lake.getLeanLibDir = (fun (x : Lake.LeanInstall) => x.libDir) <$> Lake.getLeanInstall
```

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

### Install Test Installer

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Compiler/LCNF/Testing.html

Installs a TestInstaller by providing the necessary context, including the pass under test name and the test name.

```Lean
def Lean.Compiler.LCNF.Testing.TestInstaller.install (x : TestInstaller) (passUnderTestName testName : Name) :
PassInstaller
Equations
  * x.install passUnderTestName testName = x { passUnderTestName := passUnderTestName, testName := testName }
```

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

### Execute setupFile

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Server/FileWorker/SetupFile.html

Uses lake setup-file to compile dependencies and update the environment.

```lean
def Lean.Server.FileWorker.setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr : String → IO Unit) :
IO FileSetupResult
```

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

### Example with Let-bindings in Lean

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Demonstrates the use of let-bindings within an example in Lean. The bindings `n` and `k` are defined and then used in an assertion.

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

```

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

### Setup File Function

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Server/FileWorker/SetupFile.html

Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`.

```APIDOC
## Lean.Server.FileWorker.setupFile

### Description
Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. Compilation progress is reported to `handleStderr`. Returns the search path for source files and the options for the file.

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
None

### Response
#### Success Response (200)
- **FileSetupResult** (FileSetupResult): The result of the file setup process.

#### Response Example
None
```

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

### Create Range Array with Start and Step

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Array/Basic.html

Constructs an array of numbers with a specified start, size, and step. Examples illustrate different start, size, and step combinations.

```Lean
def Array.range' (start size : Nat) (step : Nat := 1) :
Array Nat
Constructs an array of numbers of size `size`, starting at `start` and increasing by `step` at each element.
In other words, `Array.range' start size step` is `#[start, start+step, ..., start+(len-1)*step]`.
Examples:
  * `Array.range' 0 3 (step := 1) = #[0, 1, 2]`
  * `Array.range' 0 3 (step := 2) = #[0, 2, 4]`
  * `Array.range' 0 4 (step := 2) = #[0, 2, 4, 6]`
  * `Array.range' 3 4 (step := 2) = #[3, 5, 7, 9]`

Equations
  * Array.range' start size step = Array.ofFn fun (i : Fin size) => start + step * ↑i
```

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

### mstart

Source: https://imperialcollegelondon.github.io/FLT/docs/Std/Tactic/Do/Syntax.html

Starts the stateful proof mode of Std.Do.SPred.

```APIDOC
## mstart

### Description
Starts the stateful proof mode of Std.Do.SPred. This transforms a stateful goal of the form H ⊢ₛ T into ⊢ₛ H → T.
```

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

### GET /String.Slice/revSplit

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Slice.html

Splits a slice at each subslice that matches the pattern `pat`, starting from the end of the slice and traversing towards the start.

```APIDOC
## GET /String.Slice/revSplit

### Description
Splits a slice at each subslice that matches the pattern `pat`, starting from the end of the slice and traversing towards the start. The matched subslices are not included in the results.

### Parameters
#### Request Body
- **s** (Slice) - Required - The input slice to split.
- **pat** (ρ) - Required - The pattern to match against.

### Response
#### Success Response (200)
- **result** (Std.Iter Slice) - An iterator over the resulting subslices.
```

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

### Run Lake Setup File Function

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Server/FileWorker/SetupFile.html

Executes the `lake setup-file` command and returns its output.

```APIDOC
## Lean.Server.FileWorker.runLakeSetupFile

### Description
Executes the `lake setup-file` command and returns its output.

### Parameters
#### Path Parameters
- **lakePath** (System.FilePath) - Required - The path to the Lake project.
- **filePath** (System.FilePath) - Required - The path to the file to set up.

#### Query Parameters
None

#### Request Body
None

### Request Example
None

### Response
#### Success Response (200)
- **LakeSetupFileOutput** (LakeSetupFileOutput): The output of the `lake setup-file` command.
  - **spawnArgs** (IO.Process.SpawnArgs): Arguments used to spawn the process.
  - **exitCode** (UInt32): The exit code of the process.
  - **stdout** (String): The standard output of the process.
  - **stderr** (String): The standard error of the process.

#### Response Example
None
```

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

### String.startPos and String.endPos

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Defs.html

Functions to get the start and end positions of a string.

```APIDOC
## String Start and End Positions

### `String.startPos`

#### Description
Returns the start position of `s`, as an `s.Pos`.

#### Definition
`@[inline] def String.startPos (s : String) : s.Pos :=
  { offset := 0, isValid := ⋯ }

#### Theorem
- **String.offset_startPos {s : String}**: `s.startPos.offset = 0`

### `String.endPos`

#### Description
Returns the past-the-end position of `s`, as an `s.Pos`.

#### Definition
`@[inline] def String.endPos (s : String) : s.Pos :=
  { offset := s.rawEndPos, isValid := ⋯ }

#### Theorem
- **String.offset_endPos {s : String}**: `s.endPos.offset = s.rawEndPos`
```

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

### Get First Character

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Substring.html

Returns the first character in the substring, or 'A' if the start position is invalid.

```lean
@[inline]
def Substring.Raw.front (s : Raw) :
Char
```

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

### Process Lean File with Header Setup

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Language/Lean.html

Entry point for the Lean language processor. It calls `setupImports` after header parsing to supply metadata or abort. `old?` allows for incremental processing.

```Lean
def Lean.Language.Lean.process (setupImports : Elab.HeaderSyntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult)) (old? : Option InitialSnapshot) : ProcessingM InitialSnapshot
Entry point of the Lean language processor.
The `setupImports` function is called after the header has been parsed and before the first command is parsed in order to supply additional file metadata (or abort with a given terminal snapshot); see `SetupImportsResult`.
`old?` is a previous resulting snapshot, if any, to be reused for incremental processing.
Equations
  * Lean.Language.Lean.process setupImports old? = (Lean.Language.Lean.process.parseHeader✝ setupImports old?).run (Option.map (fun (x : Lean.Language.Lean.InitialSnapshot) => x.ictx) old?)
```

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

### Array.foldrM Example (Partial Array)

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Array/Basic.html

Demonstrates folding a monadic function over a specific range of the array using `start` and `stop` parameters. Folding proceeds from `start` (exclusive) to `stop` (inclusive).

```Lean
example [Monad m] (f : α → β → m β) :
  Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do
    let x₁ ← f b x₀
    let x₂ ← f a x₁
    pure x₂)
  := by rfl
```

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

### Run Lake setup file

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Server/FileWorker/SetupFile.html

Executes the lake setup-file command for a given document.

```lean
def Lean.Server.FileWorker.runLakeSetupFile (m : DocumentMeta) (lakePath filePath : System.FilePath) (header : ModuleHeader) (handleStderr : String → IO Unit) :
IO LakeSetupFileOutput
```

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

### Lean.Elab.Tactic.Do.ProofMode.mStartMainGoal

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Elab/Tactic/Do/ProofMode/Basic.html

Initializes the proof mode using the current main goal.

```APIDOC
## FUNCTION Lean.Elab.Tactic.Do.ProofMode.mStartMainGoal

### Description
Initializes the proof mode using the current main goal in the TacticM monad.

### Response
- **(MVarId × MGoal)** - Returns a tuple containing the metavariable ID and the resulting MGoal.
```

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

### Array.foldlM Example (Partial Array)

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Array/Basic.html

Demonstrates folding a monadic function over a specific range of the array using `start` and `stop` parameters. Folding proceeds from `start` (inclusive) to `stop` (exclusive).

```Lean
example [Monad m] (f : α → β → m α) :
    Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
      let x₁ ← f x₀ b
      let x₂ ← f x₁ c
      pure x₂)
  := by rfl
```

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

### Get Lake Build Home

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Config/InstallPath.html

Determines the root of a Lake installation based on the executable path.

```Lean
def Lake.lakeBuildHome? (lake : System.FilePath) :
Option System.FilePath
Equations
  * Lake.lakeBuildHome? lake = do let __do_lift ← lake.parent let __do_lift ← __do_lift.parent let __do_lift ← __do_lift.parent __do_lift.parent
```

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

### Call Lean Setup LibUV

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Compiler/IR/EmitLLVM.html

Sets up the LibUV environment for Lean.

```Lean
def Lean.IR.EmitLLVM.callLeanSetupLibUV {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (argc argv : LLVM.Value llvmctx) :
M llvmctx (LLVM.Value llvmctx)
```

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

### GET /Lean/Parser/checkColGe

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Parser/Basic.html

The checkColGe parser ensures that the next token starts at or after the column of the saved position.

```APIDOC
## GET /Lean/Parser/checkColGe

### Description
The `checkColGe` parser ensures that the next token starts at or after the column of the saved position.

### Method
GET

### Endpoint
/Lean/Parser/checkColGe

### Parameters
#### Query Parameters
- **errorMsg** (String) - Optional - Custom error message to return if the column check fails. Defaults to "checkColGe".
```

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

### Get Indentation and Column

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/TryThis.html

Calculates the initial indentation and starting column for a given syntax range.

```Lean
def Lean.Meta.Tactic.TryThis.getIndentAndColumn (map : FileMap) (range : Syntax.Range) :
Nat × Nat
```

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

### Configure SolveByElim to Intro Goals

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Tactic/SolveByElim.html

Use this to call `intro` on each goal before applying lemmas. It modifies the `mainGoalProc` to include this step.

```Lean
def Lean.Meta.SolveByElim.SolveByElimConfig.intros (cfg : SolveByElimConfig := { }) :
SolveByElimConfig
Create or modify a `Config` which calls `intro` on each goal before applying lemmas.
Equations
  * cfg.intros = cfg.mainGoalProc fun (g : Lean.MVarId) => do let __do_lift ← g.intro1P pure [__do_lift.snd]
```

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

### Get Range of Alternatives

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Match/MatcherInfo.html

Calculates the range (start and end position) for the alternative arguments in a matcher.

```lean
def Lean.Meta.Match.MatcherInfo.getAltRange (info : MatcherInfo) :
Std.Rco Nat
Equations
  * info.getAltRange = info.getFirstAltPos...info.getFirstAltPos + info.numAlts
```

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

### Using simp_intro in a Lean proof

Source: https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Tactic/SimpIntro.html

Demonstrates the basic usage of simp_intro to introduce a variable while simplifying the goal.

```lean
example : x + 0 = y → x = z := by
  simp_intro h
  -- h: x = y ⊢ y = z
  sorry
```

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

### Setup Server Module

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Build/Module.html

Computes the module setup for the Lean language server, building its imports and dependencies. Used by `lake setup-file`.

```Lean
def Lake.setupServerModule (fileName : String) (path : System.FilePath) (header? : Option Lean.ModuleHeader) :
FetchM (Job Lean.ModuleSetup)
```

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

### Get Range of Discriminators

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Match/MatcherInfo.html

Calculates the range (start and end position) for the discriminator arguments in a matcher.

```lean
def Lean.Meta.Match.MatcherInfo.getDiscrRange (info : MatcherInfo) :
Std.Rco Nat
Equations
  * info.getDiscrRange = info.getFirstDiscrPos...info.getFirstDiscrPos + info.numDiscrs
```

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

### Start Stateful Proof Mode with mstart

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Initiates the stateful proof mode for Std.Do.SPred goals. It transforms `H ⊢ₛ T` to `⊢ₛ H → T`, allowing `mintro` to re-introduce `H`. `mintro` often calls `mstart` automatically.

```Lean
mstart
```

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

### Get Position of First Discriminator

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Match/MatcherInfo.html

Determines the starting position of the discriminators within the matcher's arguments.

```lean
def Lean.Meta.Match.MatcherInfo.getFirstDiscrPos (info : MatcherInfo) :
Nat
Equations
  * info.getFirstDiscrPos = info.numParams + 1
```

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

### Lean.Elab.Tactic.Do.ProofMode.mStart

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Elab/Tactic/Do/ProofMode/Basic.html

Initializes the proof mode starting from a given expression.

```APIDOC
## FUNCTION Lean.Elab.Tactic.Do.ProofMode.mStart

### Description
Initializes the proof mode starting from a given expression, returning an MStartResult containing the goal and optional proof.

### Parameters
- **goal** (Expr) - Required - The expression to start the proof mode from.

### Response
- **MStartResult** (Type) - Contains the goal (MGoal) and an optional proof (Option Expr).
```

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

### Additional Grind Examples

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Miscellaneous examples demonstrating list operations, bit vectors, and array bounds reasoning.

```Lean
example {a b} {as bs : List α} : (as ++ bs ++ [b]).getLastD a = b := by
  grind

example (x : BitVec (w+1)) : (BitVec.cons x.msb (x.setWidth w)) = x := by
  grind

example (as : Array α) (lo hi i j : Nat) :
    lo ≤ i → i < j → j ≤ hi → j < as.size → min lo (as.size - 1) ≤ i := by
  grind
```

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

### Lean.mkEmptyEnvironment

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Environment.html

Initializes a new, empty Lean environment.

```APIDOC
## Lean.mkEmptyEnvironment

### Description
Creates a new empty Lean environment with a specified trust level.

### Parameters
#### Query Parameters
- **trustLevel** (UInt32) - Optional - The trust level for the environment (default: 0).
```

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

### Get Package Definition Name

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/DSL/DeclUtil.html

Retrieves the name of the definition created by the `package` syntax. No specific setup is required.

```Lean
def Lake.DSL.packageDeclName :
Lean.Name
Equations
  * Lake.DSL.packageDeclName = `_package
```

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

### Get Position of First Alternative

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Match/MatcherInfo.html

Determines the starting position of the alternative (case) arguments within the matcher's arguments.

```lean
def Lean.Meta.Match.MatcherInfo.getFirstAltPos (info : MatcherInfo) :
Nat
Equations
  * info.getFirstAltPos = info.numParams + 1 + info.numDiscrs
```

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

### Usage examples for use and use!

Source: https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Tactic/Use.html

Demonstrates the syntax and behavior of the use and use! tactics for various inductive types.

```Lean
example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
```

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

### GET /String/Pos/Raw/substrEq

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Basic.html

Checks whether substrings of two strings are equal based on starting positions and a size in UTF-8 bytes.

```APIDOC
## GET /String/Pos/Raw/substrEq

### Description
Checks whether substrings of two strings are equal. Substrings are indicated by their starting positions and a size in UTF-8 bytes. Returns false if the indicated substring does not exist in either string.

### Method
GET

### Endpoint
/String/Pos/Raw/substrEq

### Parameters
#### Query Parameters
- **s1** (String) - Required - First string.
- **pos1** (Raw) - Required - Starting position in s1.
- **s2** (String) - Required - Second string.
- **pos2** (Raw) - Required - Starting position in s2.
- **sz** (Nat) - Required - Size in UTF-8 bytes.

### Response
#### Success Response (200)
- **result** (Bool) - True if substrings are equal, false otherwise.
```

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

### Lean.KeyedDeclsAttribute.init

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/KeyedDeclsAttribute.html

Initializes a new KeyedDeclsAttribute.

```APIDOC
## Lean.KeyedDeclsAttribute.init

### Description
Initializes a new KeyedDeclsAttribute.

### Method
IO

### Endpoint
N/A (Function within Lean)

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

#### Query Parameters
N/A

#### Request Body
N/A

### Request Example
N/A

### Response
#### Success Response (IO)
- **KeyedDeclsAttribute γ** - The newly initialized KeyedDeclsAttribute.

#### Response Example
N/A
```

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

### Example with `sorry` for Undefined Proofs in Lean

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Shows an example where `sorry` is used as a placeholder for an unimplemented proof. This is common during development when the proof logic is not yet complete.

```Lean
def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0

example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
  intros
  /- Tactic state
     f✝ : Nat → Nat
     a✝ : AllEven f✝
     ⊢ AllEven fun k => f✝ (k + 1) -/
  sorry

```

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

### Algebraic Solver Examples

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Demonstrates using the ring solver within grind for polynomial equations and disequations over commutative rings and fields.

```Lean
open Lean Grind

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

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

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

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

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

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

### Get Offset of Sliced String Position

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Basic.html

Calculates the offset of a position within a sliced string relative to the start of the slice.

```Lean
@[simp]
theorem String.Pos.offset_slice {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} :
(pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset
```

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

### SolveByElimConfig.intros

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Tactic/SolveByElim.html

Creates or modifies a Config that calls `intro` on each goal before applying lemmas.

```APIDOC
## POST /api/config/intros

### Description
Creates or modifies a `Config` which calls `intro` on each goal before applying lemmas.

### Method
POST

### Endpoint
/api/config/intros

### Parameters
#### Request Body
- **cfg** (SolveByElimConfig) - Optional - The current configuration.

### Request Example
```json
{
  "cfg": {}
}
```

### Response
#### Success Response (200)
- **cfg** (SolveByElimConfig) - The modified configuration.

#### Response Example
```json
{
  "cfg": {
    "intros": true
  }
}
```
```

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

### mvcgen Extended Syntax Example

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Demonstrates the extended syntax for mvcgen, including handling invariants and using case labels for inaccessibles.

```Lean
mvcgen [...] invariants
· I1
· I2
with grind
```

```Lean
mvcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2
with grind
```

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

### Example of zify tactic

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Demonstrates the basic usage of the `zify` tactic to shift propositions from `Nat` to `Int`. It also shows how to apply `zify` to a specific hypothesis.

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

```

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

### Linear Integer Arithmetic Examples

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Demonstrates using grind to solve goals involving linear integer arithmetic, including equalities, inequalities, and divisibility.

```Lean
-- Even + even is never odd.
example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
  grind

-- Mixing equalities and inequalities.
example {x y : Int} :
    2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
  grind

-- Reasoning with divisibility.
example (a b : Int) :
    2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
  grind

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

-- Types that implement the `ToInt` type-class.
example (a b c : UInt64)
    : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
  grind
```

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

### Get Offset of Slice Position

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Basic.html

Calculates the offset of a position within a string slice relative to the original string's start.

```Lean
@[simp]
theorem String.Pos.offset_ofSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} :
(ofSlice pos).offset = pos.offset.offsetBy p₀.offset
```

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

### File Setup Result

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Server/FileWorker/SetupFile.html

Represents the result of running `lake setup-file`.

```APIDOC
## Lean.Server.FileWorker.FileSetupResult

### Description
Result of running `lake setup-file`.

### Fields
- **kind** (FileSetupResultKind): Kind of outcome.
- **setup** (ModuleSetup): Configuration from a successful setup, or else the default.
```

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

### nlinarith Preprocessing Example

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

This tactic extends `linarith` with preprocessing steps to handle some nonlinear arithmetic problems. It adds assumptions for squared terms and products of linear terms to the context.

```Lean
nlinarith!
```

```Lean
nlinarith only [h1, h2]
```

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

### Configuring transparency for `convert`

Source: https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Tactic/Convert.html

Illustrates how to configure transparency options for the `convert` tactic, passing them to `congr!`.

```Lean
convert (config := {transparency := .default}) h
```

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

### Get Offset from Slice Position

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/String/Basic.html

Retrieves the offset of a slice position, which is the original string position offset by the slice's start.

```Lean
@[simp] theorem String.Slice.Pos.offset_ofStr {
  s : Slice
  pos : s.str.Pos
  h₁ : s.startInclusive ≤ pos
  h₂ : pos ≤ s.endExclusive
} :
(ofStr pos h₁ h₂).offset = pos.offset.unoffsetBy s.startInclusive.offset
```

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

### Rewrite expressions with push

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Examples of using the push tactic to rewrite expressions by pushing constants or operators deeper.

```lean
push _ ∈ _
```

```lean
push (disch := positivity) Real.log
```

```lean
push ¬ _
```

```lean
push fun _ ↦ _
```

```lean
push ∀ _, _
```

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

### dfoldRev example usage

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Nat/Fold.html

Illustrates the evaluation order of Nat.dfoldRev. It shows how f is applied in reverse order, starting from n-1 down to 0.

```Lean
`Nat.dfoldRev f 3 init = f 0 <| f 1 <| f 2 <| init` The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α (i + 1) → α i`.
```

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

### Use simp_intro to simplify and introduce variables

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

The `simp_intro` tactic simplifies the types of introduced variables and uses them to simplify subsequent arguments and the goal. It accepts the same options as `simp`.

```lean
example : x + 0 = y → x = z := by
  simp_intro h
  -- h: x = y ⊢ y = z
  sorry

```

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

### Lean.Meta.Sym.mkProofInstArgInfo?

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Sym/ProofInstInfo.html

Analyzes a collection of free variables to determine if any are proofs or instances.

```APIDOC
## mkProofInstArgInfo?

### Description
Analyzes whether the given free variables (arguments) are proofs or instances.

### Parameters
- **xs** (Array Expr) - Required - The array of free variables to analyze.

### Response
- **Option ProofInstInfo** - Returns `none` if no arguments are proofs or instances.
```

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

### Get binary search path

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Config/Env.html

Constructs the binary search path by combining the environment's initial path with Lean and Lake installation directories.

```Lean
env.path = if env.lake.binDir = env.lean.binDir then env.lean.binDir :: env.initPath else env.lake.binDir :: env.lean.binDir :: env.initPath
```

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

### contradiction tactic example with constructor injectivity

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

The contradiction tactic can close goals based on the injectivity of constructors. This example uses it to show a contradiction with none = some true.

```Lean
example (h : none = some true) : p := by contradiction  -- 
```

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

### Example with Assumption Tactic in Lean

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Illustrates the use of the `assumption` tactic in Lean to prove a simple implication. It automatically selects a hypothesis that matches the goal.

```Lean
example (p q : Prop) : p → q → p := by
  intros
  /- Tactic state
     a✝¹ : p
     a✝ : q
     ⊢ p      -/
  assumption

```

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

### Eta expand example

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Eta expands sub-expressions at a location and beta reduces applications of eta-expanded terms. Useful for transforming raw constructors into lambda expressions.

```Lean
example (x : α × β) : (x.1, x.2) = x :=
by
  eta_struct at x
  rfl
```

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

### Get Aligned Week of Month from ZonedDateTime

Source: https://imperialcollegelondon.github.io/FLT/docs/Std/Time/Zoned/ZonedDateTime.html

Determines the aligned week of the month for a ZonedDateTime. Calculation is based on the day of the month and weekday, with weeks starting on Monday.

```source
@[inline]
def Std.Time.ZonedDateTime.alignedWeekOfMonth (date : ZonedDateTime) :
Week.Ordinal.OfMonth
Determines the week of the month for the given `ZonedDateTime`. The week of the month is calculated based on the day of the month and the weekday. Each week starts on Monday because the entire library is based on the Gregorian Calendar.
Equations
  * date.alignedWeekOfMonth = date.date.get.alignedWeekOfMonth
```

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

### FacetOut for module.setup

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Build/Facets.html

Declares that the `FacetOut` for `module.setup` is of type `Lean.ModuleSetup`.

```Lean
@[simp]
axiom Lake.FacetOut.module.setup :
FacetOut `module.setup = Lean.ModuleSetup
```

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

### Get Goals to Copy

Source: https://imperialcollegelondon.github.io/FLT/docs/Aesop/Tree/AddRapp.html

Retrieves the goals that need to be copied for assigned metavariables, starting from a given goal reference. This is used when propagating state in the Aesop search.

```Lean
def Aesop.getGoalsToCopy (assignedMVars : UnorderedArraySet Lean.MVarId) (start : GoalRef) :
TreeM (Array GoalRef)
Equations
  * One or more equations did not get rendered due to their size.
```

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

### Configure SolveByElim to Intro Goals After

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/Tactic/SolveByElim.html

Calls `intro` on any goal for which no lemma applies. This is configured using `withDischarge`.

```Lean
def Lean.Meta.SolveByElim.SolveByElimConfig.introsAfter (cfg : SolveByElimConfig := { }) :
SolveByElimConfig
Create or modify a `SolveByElimConfig` which calls `intro` on any goal for which no lemma applies.
Equations
  * cfg.introsAfter = cfg.withDischarge fun (g : Lean.MVarId) => do let __do_lift ← g.intro1P pure (some [__do_lift.snd])
```

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

### mpure_intro Tactic

Source: https://imperialcollegelondon.github.io/FLT/docs/Std/Tactic/Do/Syntax.html

Transitions from stateful proof mode to regular goal mode.

```APIDOC
## mpure_intro

### Description
'mpure_intro' operates on a stateful 'Std.Do.SPred' goal of the form 'P ⊢ₛ ⌜φ⌝'. It leaves the stateful proof mode (discarding 'P') and leaves the regular goal 'φ'.

### Usage
```lean
theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
  mpure_intro
  exact True.intro
```
```

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

### Get Syntax Range (Canonical) - Lean

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Syntax.html

Retrieves the source code range (start and stop positions) of a syntax node. If `canonicalOnly` is true, it only considers canonical positions.

```Lean
def Lean.Syntax.getRange? (stx : Syntax) (canonicalOnly : Bool := false) :
Option Syntax.Range
Equations
  * stx.getRange? canonicalOnly = match stx.getPos? canonicalOnly, stx.getTailPos? canonicalOnly with | some start, some stop => some { start := start, stop := stop } | x, x_1 => none
```

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

### Example of Simps Projection Initialization

Source: https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Tactic/Simps/Basic.html

Demonstrates how to initialize custom simps projections for a structure.

```lean
structure gradedFun (A : ℕ → Type*) where
  toFun := ∀ i j, A i →+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
```

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

### Lean.Meta.constructorApp'?

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Meta/CtorRecognizer.html

Similar to constructorApp?, but uses whnf on failure and handles Nat offsets.

```APIDOC
## Lean.Meta.constructorApp'?

### Description
Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again. It also uses `isOffset?` for `Nat`.

### Parameters
#### Request Body
- **e** (Expr) - Required - The expression to check.
```

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

### GET /Lean/Parser/checkColEq

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Parser/Basic.html

The checkColEq parser ensures that the next token starts at exactly the column of the saved position. This is used for whitespace-sensitive syntax like 'by' or 'do' blocks.

```APIDOC
## GET /Lean/Parser/checkColEq

### Description
The `checkColEq` parser ensures that the next token starts at exactly the column of the saved position (see `withPosition`). This can be used to do whitespace sensitive syntax like a `by` block or `do` block, where all the lines have to line up.

### Method
GET

### Endpoint
/Lean/Parser/checkColEq

### Parameters
#### Query Parameters
- **errorMsg** (String) - Optional - Custom error message to return if the column check fails. Defaults to "checkColEq".
```

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

### Positivity Tactic Examples

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Examples demonstrating the use of the positivity tactic to solve goals involving inequalities.

```lean
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity

example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity

example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity

example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
    0 < a ^ c + 1 / (d - c) := by
  positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]
```

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

### Prove false propositions with decide

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Use the decide tactic to demonstrate that a proposition is false. If the Decidable instance reduces to 'isFalse', the goal is closed. This example shows proving '1 ≠ 1'.

```lean
example : 1 ≠ 1 := by decide
```

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

### Lean.FileMap Get Line

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Data/Position.html

Retrieves the starting position of a given line number. It maps line numbers to the corresponding entry in the positions array, capping at the last line.

```lean
def Lean.FileMap.getLine (fmap : FileMap) (x : Nat) : Nat
The line numbers associated with the `positions` of the `FileMap`. `fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]` where `n` is the `size` of `positions`.
Equations
  * fmap.getLine x = min (x + 1) fmap.getLastLine
```

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

### Lean.MVarId.intros!

Source: https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Lean/Meta.html

Repeatedly applies intro until failure, including unfolding.

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

### Description
Applies `intro` repeatedly until it fails. Unlike standard `intros`, this allows unfolding (e.g., `¬p` to `p → False`).

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

### Response
- **(Array FVarId × MVarId)** - The array of introduced FVarIds and the updated MVarId.
```

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

### contradiction tactic example with decidable false proposition

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

This example demonstrates the contradiction tactic's ability to close goals involving decidable false propositions.

```Lean
example (h : 2 + 2 = 3) : p := by contradiction
```

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

### Array.foldrM Example (Full Array)

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Array/Basic.html

Demonstrates folding a monadic function over the entire array from right to left. The optional `start` and `stop` parameters control the folding region.

```Lean
example [Monad m] (f : α → β → m β) :
  Array.foldrM (m := m) f x₀ #[a, b, c] = (do
    let x₁ ← f c x₀
    let x₂ ← f b x₁
    let x₃ ← f a x₂
    pure x₃)
  := by rfl
```

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

### Initialize Empty BuildStore

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Build/Store.html

Creates an empty instance of the BuildStore.

```Lean
@[inline]
def Lake.BuildStore.empty :
BuildStore
```

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

### congrm tactic example

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

Use congrm to prove goals of the form lhs = rhs, lhs ↔ rhs, lhs ≍ rhs, or R lhs rhs. The expression e is a pattern containing placeholders ?_, which are matched against lhs and rhs simultaneously.

```Lean
example {
  a b c d : ℕ
} :
    Nat.pred a.succ * (d + (c + a.pred)) = Nat.pred b.succ * (b + (c + d.pred)) := by
  congrm Nat.pred (Nat.succ ?h1) * (?h2 + ?h3)
  /-  Goals left:
  case h1 ⊢ a = b
  case h2 ⊢ d = b
  case h3 ⊢ c + a.pred = c + d.pred
  -/  sorry
  sorry
  sorry
```

```Lean
example {
  a b : ℕ
} (h : a = b) : (fun y : ℕ => ∀ z, a + a = z) = (fun x => ∀ z, b + a = z) := by
  congrm fun x => ∀ w, ?_ + a = w
  -- ⊢ a = b
  exact h
```

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

### Array.foldlM Example (Full Array)

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Data/Array/Basic.html

Demonstrates folding a monadic function over the entire array from left to right. The optional `start` and `stop` parameters control the folding region.

```Lean
example [Monad m] (f : α → β → m α) :
    Array.foldlM (m := m) f x₀ #[a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure x₃)
  := by rfl
```

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

### Lean.Elab.Tactic.Do.ProofMode.elabMStart

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Elab/Tactic/Do/ProofMode/Basic.html

Elaborator for starting the proof mode.

```APIDOC
## FUNCTION Lean.Elab.Tactic.Do.ProofMode.elabMStart

### Description
Elaborator function that triggers the start of the proof mode by calling mStartMainGoal.
```

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

### Handle undecidable propositions with decide

Source: https://imperialcollegelondon.github.io/FLT/docs/tactics.html

When a Decidable instance fails to reduce to 'isTrue' or 'isFalse', the decide tactic will report failure. This example illustrates this with an opaque proposition 'unknownProp'.

```lean
opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
```

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

### Get Bounded Application Arguments - Lean Expr

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Expr.html

Extracts a limited number of arguments from a Lean application expression. Returns an array containing at most `maxArgs` arguments, starting from the last ones.

```Lean
@[inline]
def Lean.Expr.getBoundedAppArgs (maxArgs : Nat) (e : Expr) :
Array Expr
Like `Lean.Expr.getAppArgs` but returns up to `maxArgs` arguments.
In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]` where `k` is minimal such that the size of this array is at most `maxArgs`.
Equations
  * Lean.Expr.getBoundedAppArgs maxArgs e = Lean.Expr.getBoundedAppArgsAux✝ e (Array.replicate (min maxArgs e.getAppNumArgs) (Lean.mkSort Lean.levelZero)) (min maxArgs e.getAppNumArgs)
```

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

### Lean.Elab.Tactic.Do.ProofMode.mIntroForallN

Source: https://imperialcollegelondon.github.io/FLT/docs/Lean/Elab/Tactic/Do/ProofMode/Intro.html

Introduces N forall binders into the proof goal.

```APIDOC
## Lean.Elab.Tactic.Do.ProofMode.mIntroForallN

### Description
Introduces a specified number of forall binders into the proof goal.

### Parameters
- **goal** (MGoal) - Required - The current goal state.
- **n** (Nat) - Required - The number of binders to introduce.
- **k** (MGoal → m Expr) - Required - The continuation function.
```

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

### Example of simp? usage

Source: https://imperialcollegelondon.github.io/FLT/docs/Init/Tactics.html

Use `simp?` to get a suggestion for a `simp only` command that would close the goal. This helps in reducing the size of the simp set for faster processing. It can be used with `simp_all` and `dsimp` as well.

```lean
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

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

### Create Lake Installation from Lean Installation

Source: https://imperialcollegelondon.github.io/FLT/docs/Lake/Config/InstallPath.html

Constructs a Lake installation that is co-located with a given Lean installation.

```APIDOC
## def Lake.LakeInstall.ofLean (lean : LeanInstall) : LakeInstall

### Description
Construct a Lake installation co-located with the specified Lean installation.

### Equations
- One or more equations did not get rendered due to their size.
```
Tokens:
Raw