Lean Community

https://leanprover-community.github.io
Admin
Lean Community is a comprehensive documentation hub for Lean, a powerful theorem prover, and...
Tokens:40,065,153
Snippets:243,581
Trust Score:9.7
Update:1 month ago
Show doc for...
Tokens:
Raw
### 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
```

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

### Free module instances for products

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/StdBasis.html

Instances proving that the product of finitely many free modules is itself a free module.

```lean
instance Module.Free.pi {ι : Type u_1} (R : Type u_2) [Semiring R] (M : ι → Type u_4) [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Free R (M i)] :
Free R ((i : ι) → M i)
```

```lean
instance Module.Free.function (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [Free R M] :
Free R (ι → M)
```

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

### Algebra instance for free product

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/FreeProduct/Basic.html

Provides the Algebra instance for the free product.

```lean
@[instance_reducible]
instance LinearAlgebra.FreeProduct.instAlgebra {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :
Algebra R (FreeProduct R A)
```

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

### 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
```

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

### Lake.lakeBuildHome?

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

Gets the root of Lake's installation.

```APIDOC
## Lake.lakeBuildHome?(lake : System.FilePath)

### Description
Get the root of Lake's installation by assuming the executable is located at `<lake-home>/.lake/build/bin/lake`.
```

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

### Using intros for let-bindings

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

Introduces let-bound variables into the local context.

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

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

### Action and Module Instances

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/PiTensorProduct/Basic.html

Instances for DistribMulAction, SMulCommClass, IsScalarTower, and Module.

```lean
@[instance_reducible]
instance PiTensorProduct.distribMulAction' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] :
DistribMulAction R₁ (PiTensorProduct R fun (i : ι) => s i)
Equations
  * PiTensorProduct.distribMulAction' = { toSMul := PiTensorProduct.hasSMul', mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
```

```lean
instance PiTensorProduct.smulCommClass' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMulCommClass R₁ R₂ R] :
SMulCommClass R₁ R₂ (PiTensorProduct R fun (i : ι) => s i)
```

```lean
instance PiTensorProduct.isScalarTower' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMul R₁ R₂] [IsScalarTower R₁ R₂ R] :
IsScalarTower R₁ R₂ (PiTensorProduct R fun (i : ι) => s i)
```

```lean
@[instance_reducible]
instance PiTensorProduct.module' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Semiring R₁] [Module R₁ R] [SMulCommClass R₁ R R] :
Module R₁ (PiTensorProduct R fun (i : ι) => s i)
Equations
  * PiTensorProduct.module' = { toDistribMulAction := PiTensorProduct.distribMulAction', add_smul := ⋯, zero_smul := ⋯ }
```

```lean
@[instance_reducible]
instance PiTensorProduct.instModule {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
Module R (PiTensorProduct R fun (i : ι) => s i)
Equations
  * PiTensorProduct.instModule = PiTensorProduct.module'
```

```lean
instance PiTensorProduct.instSMulCommClass {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
SMulCommClass R R (PiTensorProduct R fun (i : ι) => s i)
```

```lean
instance PiTensorProduct.instIsScalarTower {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
IsScalarTower R R (PiTensorProduct R fun (i : ι) => s i)
```

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

### 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
```

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

### Get stop index of ByteSlice

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

Theorem stating the relationship between stop, start, and size.

```lean
theorem ByteSlice.stop_eq_start_add_size (s : ByteSlice) :
s.stop = s.start + s.size
```

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

### List ForIn.toList and instances

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Internal/ForIn/Lemmas.html

Lemmas and instances for List containers.

```lean
@[simp]
theorem Std.Internal.ForIn.toList_list {γ : Type u₁} (xs : List γ) :
ForIn.toList xs = xs
```

```lean
instance Std.Internal.instLawfulMemForInIdList {α : Type u₁} :
LawfulMemForInId (List α) α
```

```lean
instance Std.Internal.instPureForIn'List {m : Type u → Type v} [Monad m] {α : Type u₁} :
PureForIn' m (List α) α
```

```lean
instance Std.Internal.instPureForInList {m : Type u → Type v} [Monad m] {α : Type u₁} :
PureForIn m (List α) α
```

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

### Binary arithmetic instances for products

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Notation/Prod.html

Instances for Div and Sub on product types.

```lean
@[instance_reducible]
instance Prod.instDiv {G : Type u_7} {H : Type u_8} [Div G] [Div H] :
Div (G × H)
Equations
  * Prod.instDiv = { div := fun (p q : G × H) => (p.1 / q.1, p.2 / q.2) }
```

```lean
@[instance_reducible]
instance Prod.instSub {G : Type u_7} {H : Type u_8} [Sub G] [Sub H] :
Sub (G × H)
Equations
  * Prod.instSub = { sub := fun (p q : G × H) => (p.1 - q.1, p.2 - q.2) }
```

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

### String.foldl Examples

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

Demonstrates folding over a string from the start to count whitespace or reconstruct the string.

```lean
"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2
```

```lean
"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3
```

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

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

### Scalar and power instances for products

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Notation/Prod.html

Instances for Pow, VAdd, and SMul on product types.

```lean
@[instance_reducible]
instance Prod.instPow {E : Type u_7} {α : Type u_8} {β : Type u_9} [Pow α E] [Pow β E] :
Pow (α × β) E
Equations
  * Prod.instPow = { pow := fun (p : α × β) (c : E) => (p.1 ^ c, p.2 ^ c) }
```

```lean
@[instance_reducible]
instance Prod.instVAdd {E : Type u_7} {α : Type u_8} {β : Type u_9} [VAdd E α] [VAdd E β] :
VAdd E (α × β)
Equations
  * Prod.instVAdd = { vadd := fun (c : E) (p : α × β) => (c +ᵥ p.1, c +ᵥ p.2) }
```

```lean
@[instance_reducible]
instance Prod.instSMul {E : Type u_7} {α : Type u_8} {β : Type u_9} [SMul E α] [SMul E β] :
SMul E (α × β)
Equations
  * Prod.instSMul = { smul := fun (c : E) (p : α × β) => (c • p.1, c • p.2) }
```

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

### 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
```

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

### 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
```

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

### Order instances for Q

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Grind/Module/Envelope.html

Instances defining LE, LT, and preorder properties for Q.

```lean
@[instance_reducible]
instance Lean.Grind.IntModule.OfNatModule.instLEQOfOrderedAdd {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :
LE (Q α)
```

```lean
@[instance_reducible]
instance Lean.Grind.IntModule.OfNatModule.instLTQOfOrderedAdd {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :
LT (Q α)
Equations
  * Lean.Grind.IntModule.OfNatModule.instLTQOfOrderedAdd = { lt := fun (a b : Lean.Grind.IntModule.OfNatModule.Q α) => a ≤ b ∧ ¬b ≤ a }
```

```lean
theorem Lean.Grind.IntModule.OfNatModule.mk_le_mk {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} :
Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁
```

```lean
instance Lean.Grind.IntModule.OfNatModule.instIsPreorderQ {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :
Std.IsPreorder (Q α)
```

```lean
instance Lean.Grind.IntModule.OfNatModule.instIsPartialOrderQ {α : Type u} [NatModule α] [LE α] [Std.IsPartialOrder α] [OrderedAdd α] :
Std.IsPartialOrder (Q α)
```

```lean
instance Lean.Grind.IntModule.OfNatModule.instIsLinearPreorderQ {α : Type u} [NatModule α] [LE α] [Std.IsLinearPreorder α] [OrderedAdd α] :
Std.IsLinearPreorder (Q α)
```

```lean
instance Lean.Grind.IntModule.OfNatModule.instIsLinearOrderQ {α : Type u} [NatModule α] [LE α] [Std.IsLinearOrder α] [OrderedAdd α] :
Std.IsLinearOrder (Q α)
```

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

### Basic Topological Space Examples in Lean

Source: https://leanprover-community.github.io/theories/topology.html

Illustrates fundamental properties of topological spaces in Lean, such as the relationship between closed sets and unions, complements, and set differences. Requires importing `Mathlib.Topology.Basic`.

```lean
import Mathlib.Topology.Basic


open TopologicalSpace
variable {X : Type} [TopologicalSpace X] {U V C D Y Z : Set X}

example : IsClosed C → IsClosed D → IsClosed (C ∪ D) := IsClosed.union
```

```lean
example : IsOpen Cᶜ ↔ IsClosed C := isOpen_compl_iff
```

```lean
example : IsOpen U → IsClosed C → IsOpen (U \ C) := IsOpen.sdiff
```

```lean
example : interior Y = Y ↔ IsOpen Y := interior_eq_iff_isOpen
```

```lean
example : Y ⊆ Z → interior Y ⊆ interior Z := interior_mono
```

```lean
example : IsOpen Y ↔ ∀ x ∈ Y, ∃ U ⊆ Y, IsOpen U ∧ x ∈ U := isOpen_iff_forall_mem_open
```

```lean
example : closure Y = Y ↔ IsClosed Y := closure_eq_iff_isClosed
```

```lean
example : closure Y = (interior Yᶜ)ᶜ := closure_eq_compl_interior_compl
```

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

### 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.
```

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

### 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
```

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

### Countable and Uncountable instances for Products

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Countable/Basic.html

Instances and theorems for product types.

```lean
instance instCountableProd {α : Type u} {β : Type v} [Countable α] [Countable β] :
Countable (α × β)
```

```lean
instance instUncountableProdOfNonempty {α : Type u} {β : Type v} [Uncountable α] [Nonempty β] :
Uncountable (α × β)
```

```lean
instance instUncountableProdOfNonempty_1 {α : Type u} {β : Type v} [Nonempty α] [Uncountable β] :
Uncountable (α × β)
```

```lean
theorem countable_left_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty β] (h : Countable (α × β)) :
Countable α
```

```lean
theorem countable_right_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty α] (h : Countable (α × β)) :
Countable β
```

```lean
theorem countable_prod_swap {α : Type u} {β : Type v} [Countable (α × β)] :
Countable (β × α)
```

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

### 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
```

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

### Legacy.Range ForIn.toList and instances

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Internal/ForIn/Lemmas.html

Lemmas and instances for Legacy.Range containers.

```lean
@[simp]
theorem Std.Internal.ForIn.toList_range (r : Legacy.Range) :
ForIn.toList r = List.range' r.start r.size r.step
```

```lean
instance Std.Internal.instLawfulMemForInIdRangeNat :
LawfulMemForInId Legacy.Range Nat
```

```lean
instance Std.Internal.instPureForIn'RangeNat {m : Type u → Type v} [Monad m] :
PureForIn' m Legacy.Range Nat
```

```lean
instance Std.Internal.instPureForInRangeNat {m : Type u → Type v} [Monad m] :
PureForIn m Legacy.Range Nat
```

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

### Get Lake build home

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

Calculates the root of a Lake installation based on the expected path of the executable.

```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
```

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

### Product and Pi Instances for Convergence Classes

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Order/MonotoneConvergence.html

Instances for SupConvergenceClass and InfConvergenceClass on product and pi types.

```lean
instance Prod.supConvergenceClass {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [SupConvergenceClass α] [SupConvergenceClass β] :
SupConvergenceClass (α × β)
```

```lean
instance instInfConvergenceClassProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [InfConvergenceClass α] [InfConvergenceClass β] :
InfConvergenceClass (α × β)
```

```lean
instance Pi.supConvergenceClass {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SupConvergenceClass (α i)] :
SupConvergenceClass ((i : ι) → α i)
```

```lean
instance Pi.infConvergenceClass {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), InfConvergenceClass (α i)] :
InfConvergenceClass ((i : ι) → α i)
```

```lean
instance Pi.supConvergenceClass' {α : Type u_1} {ι : Type u_3} [Preorder α] [TopologicalSpace α] [SupConvergenceClass α] :
SupConvergenceClass (ι → α)
```

```lean
instance Pi.infConvergenceClass' {α : Type u_1} {ι : Type u_3} [Preorder α] [TopologicalSpace α] [InfConvergenceClass α] :
InfConvergenceClass (ι → α)
```

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

### Densely Ordered Instances for Products and Functions

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Basic.html

Instances for product types and function spaces.

```lean
instance instDenselyOrderedProd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
DenselyOrdered (α × β)
```

```lean
instance instDenselyOrderedForall {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → Preorder (π i)] [∀ (i : ι), DenselyOrdered (π i)] :
DenselyOrdered ((i : ι) → π i)
```

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

### 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)
```

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

### Instances for WithTop

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.html

Instances for ZeroLEOneClass, IsBotOneClass, and IsBotZeroClass.

```lean
instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
ZeroLEOneClass (WithTop α)
```

```lean
instance WithTop.instIsBotOneClass {α : Type u} [One α] [LE α] [IsBotOneClass α] :
IsBotOneClass (WithTop α)
```

```lean
instance WithTop.instIsBotZeroClass {α : Type u} [Zero α] [LE α] [IsBotZeroClass α] :
IsBotZeroClass (WithTop α)
```

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

### 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
```

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

### Example of mvcgen invariant suggestion

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

Demonstrates using invariants? to generate a starting point for loop invariants in a function.

```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
```

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

### Free module product instance

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Basis/Prod.html

Instance showing that the product of two free modules is free.

```lean
instance Module.Free.prod (R : Type u_6) (M : Type u_7) (N : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Free R M] [Free R N] :
Free R (M × N)
```

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

### Semiring instance for free product

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/FreeProduct/Basic.html

Provides the Semiring instance for the free product.

```lean
@[instance_reducible]
instance LinearAlgebra.FreeProduct.instSemiring {I : Type u} [DecidableEq I] (R : Type v) [CommSemiring R] (A : I → Type w) [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] :
Semiring (FreeProduct R A)
```

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

### 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

```

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

### Finite Presentation Instances

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/FinitePresentation.html

Instances for subsingletons, products, and pi types.

```lean
@[instance 900]
instance Module.FinitePresentation.of_subsingleton {R : Type u_2} (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Subsingleton M] :
FinitePresentation R M
```

```lean
instance Module.FinitePresentation.prod {R : Type u_1} (M : Type u_2) (N : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [FinitePresentation R M] [FinitePresentation R N] :
FinitePresentation R (M × N)
```

```lean
instance Module.FinitePresentation.pi {R : Type u_3} [Ring R] {ι : Type u_1} (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), FinitePresentation R (M i)] [Finite ι] :
FinitePresentation R ((i : ι) → M i)
```

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

### Get String Length

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

Returns the length of a string in Unicode code points. Examples show its usage with empty, simple, and Unicode strings.

```Lean
@[extern lean_string_length]
def String.length (b : String) :
Nat
-- Returns the length of a string in Unicode code points.
-- Examples:
--   * `".length = 0`
--   * `"abc".length = 3`
--   * `"L∃∀N".length = 4`
```

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

### Get Previous Valid Position in String (Unsafe)

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

Returns the previous valid position before the given position in a string, or panics if the position is the start position.

```Lean
@[inline]
def String.Pos.prev! {s : String} (pos : s.Pos) :
  s.Pos
Equations
  * pos.prev! = String.Pos.ofToSlice pos.toSlice.prev!
```

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

### Action instances for Lp spaces

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.html

Instances for MulAction, AddAction, and DistribMulAction on Lp spaces.

```lean
@[instance_reducible]
instance DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [Monoid M] [MulAction M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] :
MulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
Equations
  * DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp = Function.Injective.mulAction Subtype.val ⋯ ⋯
```

```lean
@[instance_reducible]
instance DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [AddMonoid M] [AddAction M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] :
AddAction Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
Equations
  * DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp = Function.Injective.addAction Subtype.val ⋯ ⋯
```

```lean
@[instance_reducible]
instance DomMulAct.instDistribMulActionSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [Monoid M] [MulAction M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] :
DistribMulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
Equations
  * One or more equations did not get rendered due to their size.
```

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

### Get Previous Valid Position in String (Optional)

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

Returns the previous valid position before the given position in a string, or `none` if the position is the start position.

```Lean
@[inline]
def String.Pos.prev? {s : String} (pos : s.Pos) :
  Option s.Pos
Equations
  * pos.prev? = Option.map String.Pos.ofToSlice pos.toSlice.prev?
```

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

### Using simp_intro to simplify and introduce variables

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

Simplifies types of variables while introducing them into the context.

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

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

### Array ForIn.toList and instances

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Internal/ForIn/Lemmas.html

Lemmas and instances for Array containers.

```lean
@[simp]
theorem Std.Internal.ForIn.toList_array {γ : Type u₁} (xs : Array γ) :
ForIn.toList xs = xs.toList
```

```lean
instance Std.Internal.instLawfulMemForInIdArray {α : Type u₁} :
LawfulMemForInId (Array α) α
```

```lean
instance Std.Internal.instPureForIn'Array {m : Type u → Type v} [Monad m] {α : Type u₁} :
PureForIn' m (Array α) α
```

```lean
instance Std.Internal.instPureForInArray {m : Type u → Type v} [Monad m] {α : Type u₁} :
PureForIn m (Array α) α
```

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

### Get Previous Valid Position in String

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

Returns the previous valid position before the given position in a string. Requires a proof that the position is not the start position.

```Lean
@[inline]
def String.Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) :
  s.Pos
Equations
  * pos.prev h = String.Pos.ofToSlice (pos.toSlice.prev ⋯)
```

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

### Instance for free products

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/FinitelyPresentedGroup.html

Instance showing that the free product of two finitely presented groups is finitely presented.

```lean
instance Group.IsFinitelyPresented.instCoprod {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsFinitelyPresented G] [IsFinitelyPresented H] :
IsFinitelyPresented (Monoid.Coprod G H)
```

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

### Get Previous Valid Position in Slice (Unsafe)

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

Returns the previous valid position before the given position in a slice, or panics if the position is the start position.

```Lean
def String.Slice.Pos.prev! {s : Slice} (pos : s.Pos) :
  s.Pos
Equations
  * pos.prev! = if h : pos = s.startPos then panicWithPosWithDecl "Init.Data.String.FindPos" "String.Slice.Pos.prev!" 115 31 "The start position has no previous position" else pos.prev h
```

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

### Instances for TietzeExtension

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/TietzeExtension.html

Instances for product, pi, and unique types.

```lean
instance Pi.instTietzeExtension {ι : Type u_1} {Y : ι → Type v} [(i : ι) → TopologicalSpace (Y i)] [∀ (i : ι), TietzeExtension (Y i)] :
TietzeExtension ((i : ι) → Y i)
```

```lean
instance Prod.instTietzeExtension {Y : Type v} {Z : Type w} [TopologicalSpace Y] [TietzeExtension Y] [TopologicalSpace Z] [TietzeExtension Z] :
TietzeExtension (Y × Z)
```

```lean
instance Unique.instTietzeExtension {Y : Type v} [TopologicalSpace Y] [Nonempty Y] [Subsingleton Y] :
TietzeExtension Y
```

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

### Get Previous Valid Position in Slice (Optional)

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

Returns the previous valid position before the given position in a slice, or `none` if the position is the start position.

```Lean
def String.Slice.Pos.prev? {s : Slice} (pos : s.Pos) :
  Option s.Pos
Equations
  * pos.prev? = if h : pos = s.startPos then none else some (pos.prev h)
```

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

### Get Previous Valid Position in Slice

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

Returns the previous valid position before the given position in a slice. Requires a proof that the position is not the start position.

```Lean
@[inline]
def String.Slice.Pos.prev {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) :
  s.Pos
Equations
  * pos.prev h = s.posLT pos.offset ⋯
```

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

### Product and Pi Instances

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Max.html

Instances for product types and Pi types.

```lean
instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :
NoMinOrder (α × β)
```

```lean
instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :
NoMaxOrder (α × β)
```

```lean
instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :
NoMinOrder (α × β)
```

```lean
instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :
NoMaxOrder (α × β)
```

```lean
instance instNoMinOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :
NoMinOrder ((i : ι) → π i)
```

```lean
instance instNoMaxOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :
NoMaxOrder ((i : ι) → π i)
```

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

### Cardinal Presentability Instances and Theorems

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Presentable/Basic.html

Basic instances and equivalence theorems for cardinal presentable objects.

```lean
instance CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : (isCardinalPresentable C κ).FullSubcategory) :
IsCardinalPresentable ((isCardinalPresentable C κ).ι.obj X) κ
```

```lean
theorem CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
IsCardinalPresentable X κ ↔ (coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ
```

```lean
theorem CategoryTheory.isCardinalPresentable_iff {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) :
isCardinalPresentable C κ X ↔ IsCardinalPresentable X κ
```

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

### Array Get Element Extract

Source: https://leanprover-community.github.io/mathlib4_docs/Init/Data/Array/Extract.html

Safely accessing an element within an extracted sub-array using `getElem?`. The index `k` is relative to the start of the extracted sub-array.

```lean
@[simp]
theorem Array.getElem?_extract_of_lt {α : Type u_1} {as : Array α} {i j k : Nat} (h : k < min j as.size - i) :
(as.extract i j)[k]? = some as[i + k]
```

```lean
theorem Array.getElem?_extract_of_succ {α : Type u_1} {as : Array α} {j : Nat} :
(as.extract 0 (j + 1))[j]? = as[j]?
```

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

### Get the list of vertices in a path

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Quiver/Path/Vertices.html

Returns the list of vertices in a path, including the start and end vertices. For `nil` path, it's `[a]`. For `p.cons e`, it's `p.vertices` appended with the end vertex.

```Lean
def Quiver.Path.vertices {
  V : Type u_1
}
[Quiver V] {a b : V} : Path a b → List V
-- The list of vertices in a path, including the start and end vertices.
Equations
  * Quiver.Path.nil.vertices = [a]
  * (p.cons e).vertices = p.vertices.concat (p.cons e).end
```

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

### Add instance and theorems for WithTop

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.html

Add instance and related theorems for WithTop.

```lean
@[instance_reducible]
instance WithTop.add {α : Type u} [Add α] :
Add (WithTop α)
Equations
  * WithTop.add = { add := WithTop.map₂ fun (x1 x2 : α) => x1 + x2 }
```

```lean
@[simp]
theorem WithTop.coe_add {α : Type u} [Add α] (a b : α) :
↑(a + b) = ↑a + ↑b
```

```lean
@[simp]
theorem WithTop.top_add {α : Type u} [Add α] (x : WithTop α) :
⊤ + x = ⊤
```

```lean
@[simp]
theorem WithTop.add_top {α : Type u} [Add α] (x : WithTop α) :
x + ⊤ = ⊤
```

```lean
@[simp]
theorem WithTop.add_eq_top {α : Type u} [Add α] {x y : WithTop α} :
x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
```

```lean
theorem WithTop.add_ne_top {α : Type u} [Add α] {x y : WithTop α} :
x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
```

```lean
@[simp]
theorem WithTop.add_lt_top {α : Type u} [Add α] {x y : WithTop α} [LT α] :
x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
```

```lean
theorem WithTop.add_eq_coe {α : Type u} [Add α] {a b : WithTop α} {c : α} :
a + b = ↑c ↔ ∃ (a' : α), ∃ (b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
```

```lean
theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {b : α} :
x + ↑b = ⊤ ↔ x = ⊤
```

```lean
theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {y : WithTop α} {a : α} :
↑a + y = ⊤ ↔ y = ⊤
```

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

### Product Topology Instances

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Order/LowerUpperTopology.html

Instances for lower and upper topologies on product spaces.

```lean
instance Topology.instIsLowerProd {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [IsLower α] [OrderBot α] [Preorder β] [TopologicalSpace β] [IsLower β] [OrderBot β] :
IsLower (α × β)
```

```lean
instance Topology.instIsUpperProd {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [IsUpper α] [OrderTop α] [Preorder β] [TopologicalSpace β] [IsUpper β] [OrderTop β] :
IsUpper (α × β)
```

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

### Get! Equality with Get! and Get?

Source: https://leanprover-community.github.io/mathlib4_docs/Std/Data/DHashMap/Internal/RawLemmas.html

Asserts that `get!` is equivalent to calling `get!` on the result of `get?`.

```Lean
theorem Std.DHashMap.Internal.Raw₀.get!_eq_get!_get? {
  α : Type u
}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α] [Hashable α] [LawfulBEq α]
(h : m.val.WF)
{a : α}
[Inhabited (β a)] :
m.get! a = (m.get? a).get!
```

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

### WithConv Module and Action Instances

Source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/WithConv.html

Instances for DistribMulAction and Module on WithConv.

```lean
@[instance_reducible]
instance WithConv.instDistribMulAction {R : Type u_1} {A : Type u_2} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] :
DistribMulAction R (WithConv A)
Equations
  * WithConv.instDistribMulAction = { toMulAction := WithConv.instMulAction, smul_zero := ⋯, smul_add := ⋯ }
```

```lean
@[instance_reducible]
instance WithConv.instModule {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Module R A] :
Module R (WithConv A)
Equations
  * WithConv.instModule = { toDistribMulAction := WithConv.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }
```
Tokens:
Raw