Glossary

Every word this site uses, in one place: what this project defines, the words its explanations and readings use, and Lean's own words. Type in the box to filter.

Defined in this project

Every definition in this project, under its own name: the first paragraph of its description, or how it is declared when it has none. Theorems are not listed here: they are results, not words.

A · B · C · D · E · F · G · H · I · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

A

ack def: def ack : Nat → Nat → Nat · ack
Add structure: ---- · Ex.Add
Add structure: structure Add (α : Type) · Ex.Add
Add class: class Add (α : Type) · Ex.Add
Add structure: structure Add (α : Type) · Ex.Ex.Add
Add class: ---- · Ex.Ex.Add
Add class: class Add (α : Type) · Ex.Ex.Add
Add class: class Add (α : Type) · Ex.Ex.Ex.Add
add def: def add (x y : Nat) · add
add def: --- · add
add def: def add : Nat → Nat → Nat · add
add def: def add (m : Nat) : Nat → Nat · add
add def: def add (m n : Nat) : Nat · add
add def: def add (α β : Type) : Type · add
add def: def Bool.add (a b : Bool) : Bool · Bool.add
add def: def String.add (a b : String) : String · String.add
add def: def Kept.add (kept : Kept α) (val : α) : Kept α · TPiL.Kept.add
add def: def Vect.add [Add α] : {n : Nat} → Vect α n → Vect α n → Vect α n · Vect.add
add def: ---- · Vect.add
add def: def add (m n : Nat) : Nat · Weekday.Weekday.add
add def: def add (m n : Nat) : Nat · Weekday.Weekday.Hidden.add
add def: def add (m n : Nat) : Nat · Weekday.Weekday.Hidden.Nat.add
add def: def Point.add (p q : Point Nat) · with.Point.add
allInfo def: Extracts all messages from the given code. · TPiL.allInfo
allProofInfo def: def allProofInfo (hl : Highlighted) : Array Highlighted · TPiL.allProofInfo
alphabet def: def alphabet · TPiL.alphabet
And inductive: inductive And (a b : Prop) : Prop · Weekday.Weekday.Hidden.And
and def: ---- · Hidden.and
and def: ---- · Weekday.Weekday.Hidden.and
append def: def append : List α → List α → List α · append
append def: def Lst.append (α : Type u) (as bs : Lst α) : Lst α · Lst.append
append def: def Lst.append {α : Type u} (as bs : Lst α) : Lst α · Lst.append
append def: def append : {α : Type u} → List α → List α → List α · Weekday.Weekday.append
append def: def append (as bs : List α) : List α · Weekday.Weekday.Hidden.List.append
as def: def as : Lst Nat · as
attr def: def attr : RoleExpander · TPiL.attr

B

b def: def b : γ · b
b1 def: def b1 : Bool · b1
b2 def: def b2 : Bool · b2
Bar inductive: inductive Bar · Bar
bar def: def bar : Option Nat → Nat · bar
bar def: ------ · bar
bar def: def bar : Nat → List Nat → Bool → Nat · bar
bar def: def bar : Inhabited (Nat → Nat) · Ex.Ex.bar
bar def: def bar : Nat · Foo.bar
bar def: def Foo.bar : Nat · Foo.bar
bar def: def Foo.bar (x : Foo) : Bar · Foo.bar
bar₁ def: def bar₁ : Nat × Nat → Nat · bar₁
bar₂ def: def bar₂ (p : Nat × Nat) : Nat · bar₂
bar₃ def: def bar₃ : Nat × Nat → Nat · bar₃
bar₄ def: def bar₄ (p : Nat × Nat) : Nat · bar₄
BinaryTree inductive: inductive BinaryTree · Weekday.Weekday.BinaryTree
Bool inductive: ---- · Weekday.Weekday.Hidden.Bool
bs def: def bs : Lst Nat · bs

C

CBTree inductive: inductive CBTree · Weekday.Weekday.CBTree
checkSeverity def: Reports a comment that names a severity other than the one its command produced. · TPiL.checkSeverity
choose def: def choose (h : ∃ x, p x) : α · Hidden.Hidden.choose
codeStrs def: def codeStrs [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m (Array StrLit) · TPiL.codeStrs
Color structure: structure Color · Weekday.Weekday.Color
Color inductive: inductive Color · with.Color
ColorPoint structure: structure ColorPoint (α : Type u) extends Point α · with.ColorPoint
comment def: def comment : DirectiveExpander · TPiL.comment
commentColumn def: The column at which the comment on a line begins, if it has one. · TPiL.commentColumn
commentContents def: Extracts the text of a comment, which may span several lines. · TPiL.commentContents
compose def: def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ · compose
compose def: def compose (g : β → γ) (f : α → β) (x : α) : γ · compose
compose def: def compose · compose
compose def: def compose {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (x : α) : γ · {lit}`Nat`.compose
compose def: def compose.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (x : α) : γ · {lit}`Nat`.compose
compose def: def compose (g : β → γ) (f : α → β) (x : α) : γ · {lit}`Nat`.compose
cond def: def cond : Bool → α → α → α · Hidden.cond
cons def: def cons (α : Type) (a : α) (as : List α) : List α · cons
cons def: def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α · Lst.cons
cons def: def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α · Lst.cons
copyButtonCss def: def copyButtonCss : String · TPiL.copyButtonCss
copyButtonJs def: def copyButtonJs : String · TPiL.copyButtonJs
currentHelper def: def currentHelper : DocElabM Helper · TPiL.currentHelper

D

data inductive: inductive data types can depend on parameters. The following example defines the {name}`tail` function using pattern matching. The argument {leanRef}`α : Type u` is a parameter and occurs before the … · data
data inductive: inductive data types. Every {kw}`structure` declaration introduces a namespace with the same name. The general form is as follows: ``` structure <name> <parameters> <parent-structures> · data
Decidable class inductive: ---- · Ex.Ex.Hidden.Decidable
Decidable class inductive: ---- · Hidden.Hidden.Decidable
default opaque: opaque default [Inhabited α] : α · Ex.Ex.Ex.default
definitions inductive: inductive definitions. First, Lean supports _mutually defined_ inductive types. The idea is that we can define two (or more) inductive types at the same time, · Weekday.Weekday.definitions
definitions, inductive: inductive definitions, for example, the principles of _induction-recursion_ and _induction-induction_. These are not supported by Lean. # Axiomatic Details %%% tag · Weekday.Weekday.definitions,
detachPrefix def: def detachPrefix (code : Array ModuleItem) : Option (Array ModuleItem) × Array ModuleItem · TPiL.detachPrefix
detachSuffix def: def detachSuffix (code : Array ModuleItem) : Array ModuleItem × Option (Array ModuleItem) · TPiL.detachSuffix
dite def: ---- · Ex.Ex.Hidden.dite
div def: def div · div
div def: def div (x y : Nat) : Nat · div
divides def: def divides (x y : Nat) : Prop · divides
divides_mul def: def divides_mul (x : Nat) (k : Nat) : divides x (k*x) · divides_mul
divides_trans def: Compose the two witnesses by multiplying them, which is the witness for the combined divisibility. · divides_trans
doThrice def: def doThrice (α : Type) (h : α → α) (x : α) : α · doThrice
doThrice def: def doThrice (h : α → α) (x : α) : α · doThrice
doThrice def: def doThrice · doThrice
doTwice def: --- · doTwice
doTwice def: def doTwice (α : Type) (h : α → α) (x : α) : α · doTwice
doTwice def: def doTwice (h : α → α) (x : α) : α · doTwice
doTwice def: def doTwice · doTwice
double def: def double (x : Nat) : Nat · double
double def: def double : Nat → Nat · double
double def: def double · double
double def: def double (s : Add α) (x : α) : α · Ex.double
double def: ---- · Ex.Ex.double
double def: def double (p : Point) · Ex.Ex.double
double def: ---- · Ex.Ex.Ex.double
double def: def double (p : Point) · Ex.Ex.Point.double

E

empty def: def Set.empty {α : Type u} : Set α · Ex.Ex.Set.empty
empty def: ---- · Set.empty
empty def: def empty : RoleExpander · TPiL.empty
Eq inductive: ---- · Weekday.Weekday.Hidden.Eq
eqv def: def eqv (p₁ p₂ : α × α) : Prop · Hidden.eqv
Euclidean def: def Euclidean {α : Type u} (r : α → α → Prop) : Prop · Euclidean
Even inductive: inductive Even : Nat → Prop · Even
ExampleItem structure: structure ExampleItem · TPiL.ExampleItem
examplesCss def: def examplesCss · TPiL.examplesCss
exampleSubversoRev def: The SubVerso revision recorded in the example project's Lake manifest. · TPiL.exampleSubversoRev
Exists inductive: ---- · Weekday.Weekday.Hidden.Exists
expectedComment def: The comment that describes a message. · TPiL.expectedComment
ExpectedMessage structure: A comment that describes the message a command produces. · TPiL.ExpectedMessage
extfun def: def extfun (α : Sort u) (β : α → Sort v) · Hidden.extfun
extfun_app def: def extfun_app {α β} : extfun α β → (x : α) → β x · Hidden.extfun_app
extfun_app def: def extfun_app {α β} (f : extfun α β) (x : α) : β x · Hidden.extfun_app
extractFile def: Extracts the highlighted contents of an example. · TPiL.extractFile

F

F def: def div.F (x : Nat) (f : (x₁ : Nat) → x₁ < x → Nat → Nat) (y : Nat) : Nat · div.F
F def: def F : Type → Type · F
F def: def F (α : Type u) : Type u · F
F def: def F.{u} (α : Type u) : Type u · F
f def: def f (x : Nat) · f
f def: def f (x : Nat) : Bool · f
f def: def f (n : Nat) : String · f
f def: def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a · f
f def: def f {α : Sort u} (r : α → α → Prop) (h : WellFounded r) (C : α → Sort v) (F : (x : α) → ((y : α) → r y x → C y) → C x) : (x : α) → C x · f
f def: def f : Bool → Bool → Bool → Bool → Bool → Bool · f
f def: def f (x : Nat) {y : Nat} (z : Nat) : Nat · f
f def: def f (x : Nat) {{y : Nat}} (z : Nat) : Nat · f
f def: def f (m n : Nat) : Nat · f
f def: def f (x y z : Nat) : Nat · f
f def: def f (n : Nat) : Nat · Weekday.Weekday.f
f def: def f {n : Nat} (t : Tuple α n) : Nat · Weekday.Weekday.f
f def: def f : Nat → Nat · with.f
f def: def f (x y z : Nat) · {lit}`Nat`.Ex3.f
f def: def f (x : Nat) (y : Nat · {lit}`Nat`.f
f' def: Alternative syntax: · f'
f1 def: def f1 : Nat → Nat → Nat · f1
f2 def: def f2 : Nat → Nat → Option Nat · f2
False inductive: ---- · Weekday.Weekday.Hidden.False
families inductive: inductive families such as {leanRef}`Vect α n`, since case splits impose constraints on the values of the indices. Without the equation compiler, we would need a lot of boilerplate code to define … · families
fib def: def fib : Nat → Nat · fib
fibFast def: def fibFast (n : Nat) : Nat · fibFast
filter def: def filter (p : α → Bool) : List α → List α · filter
five def: ---- · five
fixupAnchorComments def: Leading anchor comments are always incorrect. They probably result from Lean placing them with the next command, so we should move them back up before processing them. · TPiL.fixupAnchorComments
Foo class: class Foo · Ex.Ex.Foo
Foo inductive: inductive Foo · Foo
Foo inductive: inductive Foo · Weekday.Weekday.Foo
foo def: def foo : Inhabited (Nat × Nat) · Ex.Ex.foo
foo def: def foo : Add Nat · Ex.Ex.foo
foo def: def foo · foo
foo def: def foo : Nat × Nat → Nat · foo
foo def: ------ · foo
foo def: def foo : Nat → Nat → Nat · foo
foo def: ----- · foo
foo def: def foo (a : α) : (b : β) → γ · foo
foo def: def foo (n : Nat) (b c : Bool) · foo
foo def: a user-defined function · foo
foo inductive: inductive foo : ... → Sort u · Weekday.Weekday.foo
fromModule def: def Helper.fromModule (setup : String) : IO Helper · TPiL.Helper.fromModule
fst def: ---- · Weekday.Weekday.Hidden.fst

G

G def: def G : Type → Type → Type · G
g def: def g (x : Nat) · g
g def: def g (s : String) : Bool · g
g def: def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a · g
g def: def g (xs ys : List Nat) : Nat · g
g def: def g {α} [Add α] (a : α) (b? : Option α · {lit}`Nat`.g
getBinderName def: def getBinderName : Term → Option String · {lit}`Nat`.getBinderName
getBinderType def: def getBinderType : Term → Option Term · {lit}`Nat`.getBinderType
getUnit def: def getUnit [Monoid α] : α · Ex.Ex.getUnit
goal def: def goal : RoleExpander · TPiL.goal
GoalConfig structure: structure GoalConfig · TPiL.GoalConfig
greater def: def greater (x y : Nat) · greater

H

h1 def: def h1 (x : Nat) : Nat · h1
h2 def: def h2 (x : Nat) : Nat · h2
hasAtLeast def: def hasAtLeast [Iterator α Id β] [Productive α Id] (it : Iter (α · TPiL.hasAtLeast
hasAtLeastM def: def hasAtLeastM [Monad m] [Iterator α m β] [Productive α m] (it : IterM (α · TPiL.hasAtLeastM
hashString def: def hashString (n : UInt64) : String · TPiL.hashString
head def: def head [Inhabited α] (xs : List α) : α · Ex.Ex.head
head def: def head [Inhabited α] (xs : List α) : α · head
head def: ---- · Vect.head
hello def: def hello · hello
Helper structure: structure Helper · TPiL.Helper
highlightCommand def: def highlightCommand (code : String) : DocElabM Highlighted · TPiL.highlightCommand
highlightInline def: def highlightInline (code : String) (type? : Option String · TPiL.highlightInline
highlightName def: def highlightName (code : String) : DocElabM Highlighted · TPiL.highlightName
highlightSignature def: def highlightSignature (code : String) : DocElabM Highlighted · TPiL.highlightSignature
hlIsWs def: def hlIsWs (hl : Highlighted) : Bool · TPiL.hlIsWs
HMul class: ---- · Ex.Ex.Ex.HMul
HMul class: class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) · Ex.Ex.Ex.HMul

I

id1 def: ---- · {lit}`Nat`.Ex2.id1
id2 def: In this example, implicit lambda introduction has been disabled because we use `@` before {kw}`fun` · {lit}`Nat`.Ex2.id2
id3 def: def id3 : {α : Type} → α → α · {lit}`Nat`.Ex2.id3
id4 def: def id4 : {α : Type} → α → α · {lit}`Nat`.Ex2.id4
id5 def: In this example, implicit lambda introduction has been disabled because we used the binder annotation `{...}` · {lit}`Nat`.Ex2.id5
ident def: def ident {α : Type u} (x : α) · ident
ImageOf inductive: inductive ImageOf {α β : Type u} (f : α → β) : β → Type u · ImageOf
Implies def: def Implies (p q : Prop) : Prop · Implies
in structure: structure in a namespace with the same name. For example, we can put the {leanRef}`numberOfDay` function in the {lit}`Weekday` namespace. We are then allowed to use the shorter name when we open the … · in
indefiniteDescription def: ---- · Hidden.Hidden.indefiniteDescription
Inhabited class: ---- · Ex.Ex.Ex.Inhabited
Inhabited class: class Inhabited (a : Type _) · Ex.Ex.Ex.Inhabited
Inhabited class: class Inhabited (α : Type u) · Ex.Ex.Ex.Inhabited
Inhabited inductive: inductive Inhabited (α : Type u) · Weekday.Weekday.Hidden.Inhabited
inhabited_of_nonempty def: ---- · Hidden.inhabited_of_nonempty
instLe abbrev: ---- · instLe
inter def: def inter (a b : Set α) : Set α · Set.inter
inverse def: def inverse {f : α → β} : (b : β) → ImageOf f b → α · inverse
inverse' def: def inverse' {f : α → β} : (b : β) → ImageOf f b → α · inverse'
isCommentLine def: Whether a line consists of a comment, along with any surrounding whitespace. · TPiL.isCommentLine
IsEven def: def IsEven (a : Nat) · IsEven
isLeanBlock def: def isLeanBlock : TSyntax `block → CoreM Bool · TPiL.isLeanBlock
isMessageCommentLine def: Whether a line is a comment that introduces a message. · TPiL.isMessageCommentLine
isNewline def: def isNewline (hl : Highlighted) : Bool · TPiL.isNewline
isNotZero def: ---- · isNotZero
isNotZero def: ----- · isNotZero
isPrefix def: def isPrefix (l₁ : List α) (l₂ : List α) : Prop · isPrefix
isZero def: def isZero : Nat → Bool · isZero
ite def: ---- · Ex.Ex.Hidden.ite

K

kbd def: def kbd : RoleExpander · TPiL.kbd
kbdCSS def: def kbdCSS · TPiL.kbdCSS
Kept structure: structure Kept (α : Type u) · TPiL.Kept
keywords def: def keywords · TPiL.keywords
kw def: def kw : RoleExpander · TPiL.kw

L

lastLineIndent def: The indentation of the last line of some code. · TPiL.lastLineIndent
lean def: def lean : CodeBlockExpander · TPiL.lean
leanCommand def: def leanCommand : RoleExpander · TPiL.leanCommand
leanCommandBlock def: def leanCommandBlock : CodeBlockExpander · TPiL.leanCommandBlock
LeanConfig structure: structure LeanConfig · TPiL.LeanConfig
leanFirst def: Elaborates Lean blocks first, maintaining the order of blocks. This makes their code available for leanRef. · TPiL.leanFirst
leanInline def: def leanInline : RoleExpander · TPiL.leanInline
leanLits def: def leanLits · TPiL.leanLits
leanRef def: def leanRef : RoleExpander · TPiL.leanRef
length def: def length : List α → Nat · Weekday.length
length def: def length : {α : Type u} → List α → Nat · Weekday.Weekday.length
LineType inductive: inductive LineType · TPiL.LineType
lineType def: def lineType (line : Highlighted) : LineType · TPiL.lineType
linv def: def linv [Inhabited α] (f : α → β) : β → α · Hidden.linv
List inductive: ---- · Weekday.Weekday.Hidden.List
List inductive: inductive List (α : Type u) · Weekday.Weekday.Hidden.List
listAdd def: def listAdd [Add α] : List α → List α → List α · listAdd
listId def: def listId : List ({α : Type} → α → α) · {lit}`Nat`.Ex2.listId
logCommentMismatch def: Reports a comment that doesn't describe the message its command produced. · TPiL.logCommentMismatch
long structure: structure long proofs, namely, the {kw}`have` construct, which introduces an auxiliary subgoal in a proof. Here is a small example, adapted from the last section: ```lean variable (p q : Prop) · long
Lst def: def Lst (α : Type u) : Type u · Lst

M

m def: def m : Nat · m
map def: def map (f : α → β) : Vect α n → Vect β n · map
map def: def map (f : α → β → γ) : {n : Nat} → Vect α n → Vect β n → Vect γ n · Vect.map
map def: def map (f : α → β → γ) : Vect α n → Vect β n → Vect γ n · Vect.map
mem def: def Set.mem (a : α) (s : Set α) : Prop · Ex.Ex.Set.mem
mem def: def mem (a : α) (u : UProd α) : Prop · Hidden.UProd.mem
mem def: def mem (x : α) (a : Set α) · Set.mem
mem_fn def: ---- · Hidden.UProd.mem_fn
messageComment? def: Splits the marker that introduces a message off a comment's text, along with the severity it names, if any. · TPiL.messageComment?
messageSeverityName def: The name of a message's severity. · TPiL.messageSeverityName
mk def: def mk {α : Type} (a₁ a₂ : α) : UProd α · Hidden.UProd.mk
mk_symm def: def mk_symm (xs : List α) · mk_symm
mod7Rel def: def mod7Rel (x y : Nat) : Prop · mod7Rel
Monoid class: class Monoid (α : Type u) · Ex.Ex.Monoid
Morphism structure: ---- · Ex.Ex.Morphism
Morphism structure: structure Morphism (S1 S2 : Semigroup) · Ex.Ex.Morphism
Mul class: class Mul (α : Type u) · Ex.Ex.Ex.Mul
mul def: def mul : Nat → Nat → Nat · mul
multiVar? def: def multiVar? (str : String) : Option (Array String × String) · TPiL.multiVar?
MyStruct structure: structure MyStruct · with.MyStruct
myTuple def: def myTuple : Tuple Nat 3 · Weekday.Weekday.myTuple

N

n def: def n : Nat · n
name def: def name : RoleExpander · TPiL.name
Nat inductive: ---- · Weekday.Weekday.Hidden.Nat
Nat inductive: inductive Nat · Weekday.Weekday.Hidden.Nat
natToBin def: def natToBin : Nat → List Nat · natToBin
Natural def: def Natural · Natural
next def: def next (d : Weekday) : Weekday · Weekday.next
next def: def next (d : Weekday) : Weekday · Weekday.Weekday.next
nil def: def Lst.nil (α : Type u) : Lst α · Lst.nil
nil def: def Lst.nil {α : Type u} : Lst α · Lst.nil
Nonempty class inductive: ---- · Hidden.Hidden.Nonempty
not def: ---- · Hidden.not
numberOfDay def: def numberOfDay (d : Weekday) : Nat · numberOfDay
numConsts def: def numConsts : Term → Nat · Term.numConsts

O

object structure: structure object {lit}`s` by adding the annotation {lit}`s `{kw}`with` before the field assignments. If more than one record object is provided, then they are visited in order until Lean finds one … · with.object
Odd inductive: inductive Odd : Nat → Prop · Odd
OfNat class: ---- · Ex.Ex.Ex.OfNat
ofNat def: def Nat.ofNat : _root_.Nat → Nat · Weekday.Weekday.Hidden.Nat.ofNat
omega def: def omega : CBTree · Weekday.Weekday.CBTree.omega
oneCodeStr def: def oneCodeStr [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m StrLit · TPiL.oneCodeStr
Option inductive: ---- · Weekday.Weekday.Hidden.Option
option def: def option : RoleExpander · TPiL.option
Or inductive: inductive Or (a b : Prop) : Prop · Weekday.Weekday.Hidden.Or
or def: def or : Bool → Bool → Bool · Hidden.or

P

p def: ---- · with.p
p def: def p : Point Nat · with.p
Person structure: structure Person · Ex.Ex.Person
pi def: def pi · pi
Point structure: structure Point · Ex.Ex.Point
Point structure: structure Point (α : Type u) · with.Point
Point3 structure: structure Point3 (α : Type u) · with.Point3
previous def: def previous (d : Weekday) : Weekday · Weekday.previous
previous def: def previous (d : Weekday) : Weekday · Weekday.Weekday.previous
prioritizedElab def: def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β) (xs : Array α) : m (Array β) · TPiL.prioritizedElab
Prod inductive: ---- · Weekday.Weekday.Hidden.Prod
Prod inductive: inductive Prod (α : Type u) (β : Type v) · Weekday.Weekday.Hidden.Prod
Prod structure: ---- · Weekday.Weekday.Hidden.Prod
prod_example def: def prod_example (p : Bool × Nat) : Nat · Weekday.Weekday.prod_example
projectDir def: def projectDir : System.FilePath · TPiL.projectDir
Proof structure: structure Proof (p : Prop) : Type · Proof
ProofState structure: structure ProofState · TPiL.ProofState
proofState def: def proofState : CodeBlockExpander · TPiL.proofState
ProofStateConfig structure: structure ProofStateConfig · TPiL.ProofStateConfig
proofStateStyle def: def proofStateStyle · TPiL.proofStateStyle

Q

q def: def q : Point Nat · with.q
q def: def q : Point3 Nat · with.q
Quotient def: ---- · Hidden.Hidden.Quotient

R

r def: def r : Point3 Nat · with.r
r' def: def r' : α → α → Prop · r'
Rational structure: structure Rational · Ex.Ex.Rational
Rational structure: structure Rational · Rational
RedGreenPoint structure: structure RedGreenPoint (α : Type u) extends Point α, RGBValue · with.RedGreenPoint
reflexive def: def reflexive {α : Type u} (r : α → α → Prop) : Prop · reflexive
replicate def: def replicate (n : Nat) (a : α) : List α · replicate
reverse def: def reverse : List α → List α · Weekday.reverse
RGBValue structure: structure RGBValue · with.RGBValue
rgp def: def rgp : RedGreenPoint Nat · with.rgp

S

s def: def s : Set Nat · Ex.Ex.s
s def: ---- · Ex.Ex.s
sample def: def sample · sample
save def: def save : CodeBlockExpander · TPiL.save
saveBackref def: def saveBackref (hl : Highlighted) : DocElabM Unit · TPiL.saveBackref
savedAnchor def: def savedAnchor : CodeBlockExpander · TPiL.savedAnchor
SavedLeanConfig structure: structure SavedLeanConfig · TPiL.SavedLeanConfig
Semigroup structure: structure Semigroup · Ex.Ex.Semigroup
Semigroup structure: structure Semigroup · Semigroup
Semigroup structure: structure Semigroup · Weekday.Weekday.Semigroup
Set def: def Set (α : Type u) · Ex.Ex.Set
Set def: def Set (α : Type u) · Set
Setoid class: ---- · Hidden.Hidden.Setoid
setup def: def setup : DirectiveExpander · TPiL.setup
setupCode def: def setupCode : CodeBlockExpander · TPiL.setupCode
showGoals def: def showGoals (goals : Array (Highlighted.Goal Highlighted)) : MessageData · TPiL.showGoals
ShowProofStates inductive: inductive ShowProofStates · TPiL.ShowProofStates
Sigma inductive: ---- · Weekday.Weekday.Hidden.Sigma
signature def: def signature : CodeBlockExpander · TPiL.signature
silly def: def silly (x : Foo) : Nat · Weekday.Weekday.silly
silly def: ---- · Weekday.Weekday.silly
singleton def: def Set.singleton (a : α) : Set α · Ex.Ex.Set.singleton
smul def: ---- · with.Point.smul
snd def: def snd {α : Type u} {β : Type v} (p : Prod α β) : β · Weekday.Weekday.Hidden.snd
splitExample def: def splitExample (code : Highlighted) : Option Highlighted × Highlighted · TPiL.splitExample
splitExample' def: def splitExample' (code : Array ModuleItem) : Option (Array ModuleItem) × Array ModuleItem × Option (Array ModuleItem) · TPiL.splitExample'
square def: --- · square
step def: def step (a b x : Nat) : Nat · Ex.Ex.step
strOrName def: def strOrName : ValDesc m StrLit · TPiL.strOrName
sub1 def: def sub1 : Nat → Nat · sub1
sub1 def: ------ · sub1
sub2 def: def sub2 : Nat → Nat · sub2
Subtype inductive: ---- · Weekday.Weekday.Hidden.Subtype
Subtype structure: ---- · Weekday.Weekday.Hidden.Subtype
succ def: def succ (t : CBTree) : CBTree · Weekday.Weekday.CBTree.succ
suggest def: Internal detail of suggestion mechanism. · TPiL.suggest
Sum inductive: inductive Sum (α : Type u) (β : Type v) · Weekday.Weekday.Hidden.Sum
sum def: def sum (xs : List Nat) · {lit}`Nat`.sum
sum_example def: def sum_example (s : Sum Nat Nat) : Nat · Weekday.Weekday.sum_example
swap def: def swap : α × β → β × α · swap
swap_pair def: The same tactic script that proves p and q implies q and p also builds a function that swaps the two components of a pair. · swap_pair
swap_sum def: cases splits on which side of the sum we are in, and each branch rebuilds the value on the opposite side. · swap_sum
symmetric def: def symmetric {α : Type u} (r : α → α → Prop) : Prop · symmetric

T

t def: def t (x : Nat) : Nat · t
tactic def: def tactic : RoleExpander · TPiL.tactic
tactics def: def tactics · TPiL.tactics
tail def: ------ · tail
tail def: def tail : Vect α (n + 1) → Vect α n · tail
tail def: def tail (v : Vect α (n+1)) : Vect α n · Vect.tail
tail def: def tail : {n : Nat} → Vect α (n+1) → Vect α n · Vect.tail
tail def: def tail : Vect α (n+1) → Vect α n · Vect.tail
tail1 def: ------ · tail1
tail2 def: def tail2 : {α : Type u} → List α → List α · tail2
tailAux def: ---- · Vect.tailAux
takeWhile def: def takeWhile (p : α → Bool) (as : Array α) : Array α · takeWhile
Term inductive: inductive Term · Term
Term inductive: inductive Term · Weekday.Term
Term inductive: inductive Term · {lit}`Nat`.Term
to opaque: opaque to Lean. In contrast, the ``#reduce`` command relies on a reduction engine similar to the one used in Lean's trusted kernel, the part of Lean that is responsible for checking and verifying the … · to
to structure: structure to a tactic-style proof, making such proofs more readable and robust. :::leanFirst One thing that is nice about Lean's proof-writing syntax is that it is possible to mix term-style and … · to
toCBTree def: def toCBTree : Nat → CBTree · Weekday.Weekday.CBTree.toCBTree
TODO def: def TODO : DirectiveExpander · TPiL.TODO
TODOinline def: def TODOinline : RoleExpander · TPiL.TODOinline
toNat def: def Nat.toNat : Nat → _root_.Nat · Weekday.Weekday.Hidden.Nat.toNat
toSet def: ---- · Ex.Ex.List.toSet
toSet def: def List.toSet : List α → Set α · Ex.Ex.List.toSet
tpilBlock def: def tpilBlock (block : BlockDescr) : BlockDescr · TPiL.tpilBlock
tpilInline def: def tpilInline (inline : InlineDescr) : InlineDescr · TPiL.tpilInline
trailingComment def: Extracts a trailing comment from code, if present. · TPiL.trailingComment
trailingText def: Splits the trailing text off some code. · TPiL.trailingText
transitive def: def transitive {α : Type u} (r : α → α → Prop) : Prop · transitive
Tree inductive: inductive Tree (α : Type u) · Weekday.Tree
triple def: def triple (p : Point) · Ex.Ex.triple
True inductive: inductive True : Prop · Weekday.Weekday.Hidden.True
Tuple def: def Tuple (α : Type) (n : Nat) · Tuple
Tuple def: def Tuple (α : Type) (n : Nat) · Weekday.Weekday.Tuple
twice_double def: def twice_double (x : Nat) : Nat · twice_double
type inductive: inductive type and can be inferred from the context. In particular, we can often write {lean (type · type
type inductive: inductive type under definition occurs only as the resulting type, · Weekday.Weekday.type
types inductive: inductive types is of the form ``` c : (a : α) → (b : β[a]) → C a p[a,b] ``` · Weekday.Weekday.types
types, inductive: inductive types, and a hierarchy of universes that starts with an {tech}[impredicative], {tech (key · types,

U

union def: def Set.union (a b : Set α) : Set α · Ex.Ex.Set.union
unsound def: def unsound (x : Nat) : False · unsound
unzip def: def unzip : Vect (α × β) n → (Vect α n × Vect β n) · unzip
UProd def: def UProd (α : Type u) : Type u · Hidden.UProd

V

val def: def val : Nat · val
Vect inductive: inductive Vect (α : Type u) : Nat → Type u · Vect
Vect inductive: inductive Vect (α : Type u) : Nat → Type u · Weekday.Weekday.Vect
verbatimBlock def: def verbatimBlock (cmd : Highlighted) : TeX · TPiL.verbatimBlock
versionString def: def versionString : RoleExpander · versionString

W

Weekday inductive: inductive Weekday · Weekday
Weekday inductive: inductive Weekday · Weekday.Weekday
wobble def: def wobble : α → β → γ · wobble

X

x def: def x : Nat · x
xs def: def xs : List Int · Ex.Ex.Ex.xs
xs def: def xs : List Nat · with.xs

Y

yellow def: def yellow · Weekday.Weekday.yellow

Z

zip def: def zip : {n : Nat} → Vect α n → Vect β n → Vect (α × β) n · Vect.zip
zip def: def zip : Vect α n → Vect β n → Vect (α × β) n · Vect.zip
zip def: def zip : Vect α n → Vect β n → Vect (α × β) n · zip
zipWith def: ----- · Vect.zipWith

Other

α def: def α : Type · α
β def: def β : Type · β

Terms from the explanations

Words defined in the explanations on this site (Lean4 Domain Explanation Language term lines). Where they appear, they link here.

axiom: a declaration whose type is asserted without any proof term; Lean takes it on trust. · and_commut
cases: the tactic that splits a value or hypothesis by its constructors and gives one goal for each. · swap_sum
induction hypothesis: in the inductive step, the assumption that the property holds for n, used to prove it for succ n. · Weekday.Weekday.add_comm
inductive type: a type generated freely by a list of constructors, such as the seven weekdays. · Weekday.next_previous
modus ponens: the inference rule that from p implies q and p concludes q. · modus_ponens

Types

What kind of object something is. The Reading says these in words wherever they appear.

Bool: true or false
Equiv.Perm: Equiv.Perm α — a permutation (reordering) of α
EReal: a real number or ±∞
EuclideanSpace: EuclideanSpace ℝ (Fin n) — a point in n-dimensional space
Fin: Fin n — a number from 0 up to n − 1
Finset: Finset α — a finite set of elements of α
Ideal: Ideal R — a ideal (Ideal R)
IntermediateField: IntermediateField K L — a intermediate field (IntermediateField K L)
List: List α — a list of elements of α
Matrix: Matrix m n R — a matrix with rows m, columns n and entries in R
Measure: Measure α — a measure on α (a way to give sets a size)
Multiset: Multiset α — a finite collection of elements of α, repeats allowed
Option: Option α — either nothing or an element of α
Polynomial, R[X]: Polynomial R — a polynomial with coefficients in R
Prop: a statement (something true or false)
Set: Set α — a set of elements of α
SimpleGraph: SimpleGraph V — a graph whose vertices are the elements of V
String: a piece of text
Subfield: Subfield K — a subfield (Subfield K)
Subgroup: Subgroup G — a subgroup (Subgroup G)
Submodule: Submodule R M — a submodule (Submodule R M)
Subring: Subring R — a subring (Subring R)
Type, Type*, Type _, Type u, Type v, Sort*: a type (a collection of objects)
ZMod: ZMod n — an integer modulo n
× (pair type): α × β — a pair (α, β)
ℂ, Complex: a complex number
ℕ+: a positive whole number
ℕ, Nat: a natural number (0, 1, 2, …)
ℚ, Rat: a rational number (a fraction)
ℝ, Real: a real number
ℝ≥0, NNReal: a real number that is at least 0
ℝ≥0∞, ENNReal: a number from 0 to ∞, ∞ included
ℤ, Int: an integer
→ (function type): α → β — a function that takes α and gives β

Structures a type can have

Written in square brackets, such as [Field K]. Lean finds them by itself (they are type classes).

AddCommGroup: [AddCommGroup G] — G is a commutative group under addition
AddGroup: [AddGroup G] — G is a group under addition
CharZero: [CharZero α] — in α, 1 + 1 + … + 1 is never 0
CommGroup: [CommGroup G] — G is a commutative group
CommRing: [CommRing R] — R is a commutative ring: you can add, subtract and multiply, and order of multiplication does not matter
CommSemiring: [CommSemiring R] — R has addition and commutative multiplication
Countable: [Countable α] — α is countable
DecidableEq: [DecidableEq α] — equality between elements of α can be checked
DecidablePred: [DecidablePred p] — whether p holds can be checked
Fact: [Fact (Nat.Prime p)] — it is known that Nat.Prime p
Field: [Field K] — K is a field: you can add, subtract, multiply and divide (except by 0)
Finite: [Finite α] — α has finitely many elements
Fintype: [Fintype α] — α has finitely many elements
Group: [Group G] — G is a group: you can multiply and undo multiplication
Inhabited: [Inhabited α] — α has a chosen default element
InnerProductSpace: [InnerProductSpace ℝ E] — E has angles and lengths (an inner product)
LinearOrder: [LinearOrder α] — any two elements of α can be compared
MeasurableSpace: [MeasurableSpace X] — X has measurable sets
MetricSpace: [MetricSpace X] — X has a distance between any two points
Module: [Module R M] — M is a module (a vector space when the scalars form a field)
Monoid: [Monoid M] — M has a multiplication with a 1
NeZero: [NeZero n] — n is not 0
Nonempty: [Nonempty α] — α has at least one element
Nontrivial: [Nontrivial α] — α has at least two different elements
NormedAddCommGroup: [NormedAddCommGroup E] — E has a length (norm) for its elements
NormedSpace: [NormedSpace ℝ E] — E is a vector space with lengths
PartialOrder: [PartialOrder α] — α has an order (some pairs may be incomparable)
Ring: [Ring R] — R is a ring: you can add, subtract and multiply
Semiring: [Semiring R] — R has addition and multiplication
TopologicalSpace: [TopologicalSpace X] — X has a notion of nearness (open sets)

Properties

Statements about functions, numbers and sets that the Reading puts in words, each shown on a sample use.

AEMeasurable: AEMeasurable f — f is measurable, apart from a set of measure zero
AEStronglyMeasurable: AEStronglyMeasurable f — f is (strongly) measurable, apart from a set of measure zero
Antitone: Antitone f — f never increases
BddAbove: BddAbove S — S is bounded above
BddBelow: BddBelow S — S is bounded below
Bijective: Bijective f — f is a bijection: a perfect one-to-one pairing
BijOn: BijOn f s t — f pairs s one-to-one with t
Collinear: Collinear ℝ S — the points S lie on one line
Colorable: Colorable G n — the graph can be colored with n colors so that neighbors get different colors
Commute: Commute a b — a and b commute: their product is the same in either order
Computable: Computable f — f is computable
ConcaveOn: ConcaveOn ℝ s f — f is concave on s: its graph bends downward
ContDiff: ContDiff ℝ n f — f is smooth: it can be differentiated n times, continuously
ContDiffAt: ContDiffAt ℝ n f x — f is smooth at x
Continuous: Continuous f — f is continuous: no jumps or breaks
ContinuousAt: ContinuousAt f x — f is continuous at x
ContinuousOn: ContinuousOn f s — f is continuous on s
ContinuousWithinAt: ContinuousWithinAt f s x — f is continuous at x within s
Convex: Convex ℝ s — s is convex: it contains the segment between any two of its points
ConvexOn: ConvexOn ℝ s f — f is convex on s: its graph bends upward
Coprime: Coprime a b — a and b are coprime: no common factor bigger than 1
Countable: Countable S — S is countable
Dense: Dense S — S is dense: it comes arbitrarily close to every point
Differentiable: Differentiable ℝ f — f is differentiable: it has a derivative everywhere
DifferentiableAt: DifferentiableAt ℝ f x — f has a derivative at x
DifferentiableOn: DifferentiableOn ℝ f s — f has a derivative at every point of s
Disjoint: Disjoint s t — s and t have nothing in common
Even: Even n — n is even
Finite: Finite S — S is finite
HasDerivAt: HasDerivAt f f' x — f has derivative f' at x
HasSum: HasSum a s — the terms a add up to s
IdentDistrib: IdentDistrib X Y — X and Y have the same distribution
iIndepFun: iIndepFun m X μ — the random variables X are independent
IndepFun: IndepFun X Y — the random variables X and Y are independent
Infinite: Infinite S — S is infinite
Injective: Injective f — f is injective: different inputs always give different outputs
InjOn: InjOn f s — f is injective on s: different inputs there give different outputs
Integrable: Integrable f — f is integrable (its integral is finite)
IntegrableOn: IntegrableOn f s — f is integrable on s
IntervalIntegrable: IntervalIntegrable f volume a b — f can be integrated from a to b
Involutive: Involutive f — applying f twice gives back the input
Irrational: Irrational x — x is irrational: not a fraction of two integers
Irreducible: Irreducible p — p is irreducible: it cannot be factored into smaller non-units
IsAlgebraic: IsAlgebraic ℤ x — x is algebraic: a root of a nonzero polynomial
IsBigO: IsBigO l f g — f is at most a constant times g (big O)
IsClosed: IsClosed F — F is a closed set
IsCompact: IsCompact K — K is compact (closed and bounded, in ℝⁿ)
IsConnected: IsConnected S — S is connected: it is all in one piece
IsCoprime: IsCoprime a b — a and b are coprime
IsGLB: IsGLB S m — m is the greatest lower bound of S
IsGreatest: IsGreatest S m — m is the greatest element of S
IsLeast: IsLeast S m — m is the least element of S
IsLittleO: IsLittleO l f g — f is negligible compared with g (little o)
IsLUB: IsLUB S m — m is the least upper bound of S
IsOpen: IsOpen U — U is an open set
IsProbabilityMeasure: IsProbabilityMeasure μ — μ is a probability measure: the whole space has size 1
IsSquare: IsSquare n — n is a perfect square
IsUnit: IsUnit a — a has a multiplicative inverse
LeftInverse: LeftInverse g f — g undoes f: applying f then g gives back the input
LinearIndependent: LinearIndependent K v — the vectors v are linearly independent
LipschitzWith: LipschitzWith K f — f never stretches distances by more than a factor K
MapsTo: MapsTo f s t — f sends every element of s into t
Measurable: Measurable f — f is measurable
MeasurableSet: MeasurableSet S — S is a measurable set (one that has a size)
MeasurePreserving: MeasurePreserving f — f preserves the measure: sets keep their size
MemLp: MemLp f p — f is in Lᵖ for p = p (the p-th power of |f| has a finite integral)
Monotone: Monotone f — f never decreases: a bigger input gives an output at least as big
MonotoneOn: MonotoneOn f s — f never decreases on s
Nonempty: Nonempty S — S is not empty
Odd: Odd n — n is odd
Pairwise: Pairwise r — every two different elements are related by r
Periodic: Periodic f c — f repeats every c
Perm: Perm l₁ l₂ — l₁ is a rearrangement of l₂
Prime: Prime p — p is a prime number
Primrec: Primrec f — f is primitive recursive (computable by a simple kind of program)
Reachable: Reachable u v — there is a path from u to v
RightInverse: RightInverse g f — g is a right inverse of f
Sbtw: Sbtw ℝ x y z — y lies strictly between x and z
Squarefree: Squarefree n — n is squarefree: no square bigger than 1 divides it
StrictAnti: StrictAnti f — f is strictly decreasing
StrictMono: StrictMono f — f is strictly increasing: a bigger input gives a bigger output
StronglyMeasurable: StronglyMeasurable f — f is strongly measurable
Summable: Summable a — the series of the terms a adds up to a finite value
Surjective: Surjective f — f is surjective: every possible output is reached
SurjOn: SurjOn f s t — f maps s onto all of t
Tendsto: Tendsto f atTop (𝓝 0) — f tends to 0 as the input grows without bound
Transcendental: Transcendental ℤ x — x is transcendental: not a root of any nonzero polynomial with integer coefficients
UniformContinuous: UniformContinuous f — f is uniformly continuous
Wbtw: Wbtw ℝ x y z — y lies between x and z

Symbols

Notation a newcomer may not know. A Reading lists the ones its statement uses.

#s, card: the number of elements
%: remainder after division
.Finite: the set has finitely many elements
.Infinite: the set has infinitely many elements
/: division; on ℕ and ℤ it rounds down
^: a power
A × B: pairs (a, b) with a from A and b from B
answer(…): marks the answer the problem asks for; answer(sorry) means the answer is not filled in
atTop: “as the input goes to infinity”
choose: binomial coefficient: the number of ways to pick k things from n
deriv: the derivative
exp: the exponential function eˣ
f '' s: the image: all outputs f gives on s
f =O[l] g: big O: f is at most a constant times g, along l
f =o[l] g: little o: f is negligible compared with g, along l
f ⁻¹' s: the preimage: all inputs that f sends into s
f ∘ g: composition: first g, then f
f ≪ g: f is at most a constant times g (for large inputs)
Finset.range n: the numbers 0, 1, …, n − 1
fun x ↦ …: a function: send x to …
gcd: greatest common divisor
lcm: least common multiple
log: the natural logarithm
n !: factorial: 1 · 2 · … · n
Set.Icc a b: the closed interval [a, b]
Set.Ioo a b: the open interval (a, b)
sᶜ: the complement: everything not in s
x⁻¹: the inverse, 1 / x for numbers
{x | p x}: the set of all x with property p
|x|: absolute value
¬: “not”
π: pi
‖x‖: the norm (length) of x
ℂ: the complex numbers
ℕ: the natural numbers 0, 1, 2, … (in Lean ℕ starts at 0)
ℚ: the rational numbers (fractions)
ℝ: the real numbers
ℤ: the integers …, −2, −1, 0, 1, 2, …
↑x: x viewed in a bigger number system, such as a natural number as a real number
→: “implies”, or for functions “to”
↔: “if and only if”: both directions hold
∀: “for every”
∃: “there exists”
∃!: “there is exactly one”
∏: a product over a range or a finite set
∑: a sum over a range or a finite set
√: square root
∣: “divides”: a ∣ b means b is a multiple of a
∧: “and”
∨: “or”
∩: intersection: what both sets have in common
∪: union: everything in either set
∫: an integral
≡ [MOD n]: same remainder when divided by n
⌈x⌉: ceiling: the smallest integer at least x
⌊x⌋: floor: the largest integer at most x
𝓝 x: “near x”: used for limits

Tactics

Steps inside a proof that starts with by. Each says what the tactic does in general; the goal it leaves depends on the proof.

abel: Both sides are equal by rearranging sums (abel: algebra in commutative groups).
absurd: absurd h h' — Two facts contradict each other: h h'.
admit: Not proved yet: admit is a placeholder, so this proof is unfinished.
aesop: Search automatically for a proof using many small rules (aesop).
all_goals: all_goals simp — On every remaining goal: Simplify with Lean's standard simplification rules.
and_intros: Split the “and” goal into its parts.
any_goals: any_goals simp — On every goal where it works: Simplify with Lean's standard simplification rules.
apply: apply h — Work backwards with h: it gives the goal once its own conditions hold, so those conditions become the new goals.
apply_fun: apply_fun f at h — Apply f to both sides in h.
assumption: The goal is exactly one of the assumptions.
bound: Prove the bound by combining standard inequalities.
by_cases: by_cases h : x = 0 — Split into two cases: x = 0 is true, or it is false.
by_contra: Proof by contradiction: assume the opposite and reach something false.
by_contra!: Proof by contradiction, with the assumed opposite already simplified.
calc: A chain of steps, each one justified on its own line.
case: case zero => simp — The case zero.
cases: cases h — Split into cases on how h can be built.
cases': cases' h with x hx — Split into cases on how h can be built.
change: change a + 0 = a — Restate the goal as a + 0 = a (the same thing, written differently).
choose: choose f hf using h — From “for every x there is a y”, pick a function giving such a y: f hf using h.
classical: Allow classical reasoning from here on (every statement is true or false, even if we cannot compute which).
clear: clear h — Forget the assumptions h; they are not needed any more.
congr: Reduce to showing the matching parts of both sides are equal.
constructor: constructor function Object() { [native code] } — Split the goal into its parts: for “A and B” prove A and B, for “A iff B” prove both directions.
constructorm: Split every “and”-like assumption or goal into its parts.
continuity: Built automatically from the rules for continuous functions.
contradiction: Two assumptions contradict each other, so this case is done.
contrapose: Prove the contrapositive: if the conclusion fails, then so does the assumption.
contrapose!: Prove the contrapositive, with the negations pushed inward.
conv: Rewrite inside one chosen part of the goal.
conv_lhs: Rewrite inside the left-hand side only.
conv_rhs: Rewrite inside the right-hand side only.
convert: convert h using 1 — Close the goal with h, which almost matches; any differences become new goals.
decide: Lean checks it by direct computation (decide).
delta: delta f — Expand the definition of f.
dsimp: Simplify by unfolding definitions.
erw: erw [h] — Rewrite using h, matching up to unfolding definitions.
exact: exact h — Finish: h is exactly what is needed.
exact_mod_cast: exact_mod_cast h — Finish with h, ignoring conversions between number systems.
exacts: exacts [h₁, h₂] — Finish each remaining goal with [h₁, h₂].
exfalso: Switch to proving False: this case is impossible.
exists: exists 2 — Give 2 as the example that exists.
existsi: existsi 2 — Give 2 as the example that exists.
ext: Two functions (or sets) are equal when they agree at every input.
ext1: Two functions (or sets) are equal when they agree at every input.
field: Both sides are equal by algebra with division (field).
field_simp: Clear the denominators.
filter_upwards: Reduce a statement about “eventually” or “almost everywhere” to one about each point.
fin_cases: fin_cases i — Try each of the finitely many values of i, one case each.
finiteness: The quantity is finite (not ∞), checked automatically (finiteness).
first: first | simp | ring — Try these in order until one works: simp, ring
focus: Work on the first goal only.
fun_prop: Built automatically from the rules for continuity, differentiability or measurability (fun_prop).
funext: Two functions are equal when they agree at every input.
gcongr: Compare the two sides piece by piece: if each part on the left is at most the matching part on the right, so is the whole (gcongr).
generalize: generalize e : f x = y — Replace a specific expression by a general variable: e : f x = y.
grind: Automated reasoning that combines equalities, cases and arithmetic (grind).
group: Both sides are equal by the rules of a group (group).
grw: grw [h] — Rewrite with an inequality (or another relation) instead of an equation: h.
have: have h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.
have': have' h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.
haveI: haveI h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.
if: Split on a condition, if-then-else.
induction: induction n with — Prove it by induction on n: first a starting case, then a step from each case to the next.
induction': induction' n with n ih — Prove it by induction on n: a starting case, then the step to the next case.
infer_instance: Lean finds this automatically from known structures.
interval_cases: interval_cases n — Try every possible value of n in its known range, one case each.
intro: Move the next variable or assumption of the goal into view.
intros: Introduce everything the goal starts with.
left: Prove the left side of the “or”.
let: let y := x + 1 — Give a name to a value: y := x + 1.
letI: letI inst := Classical.decEq α — Give a name to a structure for Lean to use: inst := Classical.decEq α.
lia: Whole-number arithmetic, decided automatically (lia: linear integer arithmetic).
lift: lift n to ℕ using hn — Treat n to ℕ using hn as a value of a smaller number system, since it is known to fit.
linarith: It follows by adding up the linear inequalities in the assumptions (linarith).
linear_combination: linear_combination h₁ - h₂ — The goal is exactly this combination of the assumptions: h₁ - h₂.
match: match n with — Split on the shape of n, one case per pattern.
measurability: Built automatically from the rules for measurable functions.
module: Both sides are equal by algebra with vectors and scalars (module).
native_decide: Checked by running compiled code (native_decide). This also trusts the compiler, an extra axiom.
next: The next case.
nlinarith: Like linarith, but also multiplies assumptions together, which handles squares and products.
nofun: No case can occur, so there is nothing to prove.
nomatch: nomatch h — No case of h can occur.
noncomm_ring: Both sides are equal by algebra where multiplication need not commute (noncomm_ring).
norm_cast: Move the statement between number systems (ℕ, ℤ, ℚ, ℝ) to where it is simplest.
norm_num: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.
norm_num1: Do the arithmetic.
nth_rewrite: nth_rewrite 2 [h] — Rewrite one chosen occurrence using h.
nth_rw: nth_rw 2 [h] — Rewrite one chosen occurrence using h.
obtain: obtain ⟨x, hx⟩ := h — Unpack h into its pieces ⟨x, hx⟩.
omega: Whole-number arithmetic with +, −, constants and comparisons, decided automatically (omega).
on_goal: on_goal 2 => simp — On one chosen goal: 2 => simp.
order: It follows from the order facts in the assumptions (order).
peel: peel h with x hx — Strip matching quantifiers from both sides: h with x hx.
polyrith: The goal is a combination of the equations in the assumptions (polyrith).
positivity: The expression is positive (or at least 0), checked term by term (positivity).
push: Push the operation inward.
push_cast: Push the number-system conversions (↑) inward.
push_neg: Push the “not” inward: not-for-every becomes there-is-a-counterexample, and so on.
qify: Move the statement to ℚ, where division behaves normally.
rcases: rcases h with ⟨x, hx⟩ — Unpack h into its pieces ⟨x, hx⟩, one case per alternative.
refine: refine ⟨?_, ?_⟩ — Fill in the goal with ⟨?_, ?_⟩; every ?_ hole becomes a new goal.
refine': refine' ⟨_, _⟩ — Fill in the goal with ⟨_, _⟩; every _ hole becomes a new goal.
rename_i: rename_i x y — Name the unnamed variables x, y.
repeat: repeat rw [h] — Repeat as long as it works: Rewrite using h.
replace: replace h : 0 < x := by linarith — Replace an assumption with a stronger form: the fact h: 0 is less than x. Proved by: It follows by adding up the linear inequalities in the assumptions (linarith).
revert: revert x — Put x back into the goal, so the goal is about every possible value of it.
rewrite: rewrite [h] — Rewrite using h.
rfl: Both sides are the same by definition (rfl).
right: Prove the right side of the “or”.
ring: Both sides are equal by algebra: expand and collect like terms (ring).
ring_nf: Put the expressions into a standard algebraic form.
rintro: rintro ⟨x, hx⟩ — Introduce and unpack in one go: ⟨x, hx⟩.
rotate_left: Change the order of the goals.
rw: rw [h] — Rewrite using h.
rwa: rwa [h] at h₁ — Rewrite using h in h₁, and then the goal is one of the assumptions.
set: set y := x + 1 with hy — Give a name to an expression and use the name from now on: y := x + 1.
show: show a + 0 = a — Restate the goal as a + 0 = a.
simp: Simplify with Lean's standard simplification rules.
simp_all: Simplify the goal and all the assumptions together.
simp_arith: Simplify, including arithmetic on natural numbers.
simp_rw: simp_rw [h] — Rewrite using h, also inside “for every” and “there is”.
simpa: Simplify, and the goal closes.
sorry: Not proved yet: sorry is a placeholder, so this proof is unfinished.
specialize: specialize h 2 — Use the assumption h for the specific 2.
split: Split into one case for each branch of the if-then-else or match.
split_ifs: Split into a case for each branch of every if-then-else.
subst: subst h — Replace h by what it equals, everywhere.
suffices: suffices h : 0 < x by linarith — It is enough to prove 0 < x; that is shown next, then used to finish.
swap: Work on the second goal first.
symm: Swap the two sides.
tauto: Pure logic: it follows from the assumptions by the rules of and, or, not and implies (tauto).
trans: trans b — Go through a middle point b.
trivial: This goal is immediate.
try: try linarith — Try this, and carry on if it fails: It follows by adding up the linear inequalities in the assumptions (linarith).
unfold: unfold f — Expand the definition of f.
use: use 2 — Give 2 as the example that exists; what remains is to check it works.
wlog: wlog h : a ≤ b with H — Without loss of generality, h : a ≤ b; the other case follows the same way.
zify: Move the statement from ℕ to ℤ, where subtraction behaves normally.

Lean words

Words of the Lean language itself, and of how its projects are organized.

#check, #eval: #eval 2 + 2 — Commands that ask Lean a question while you write: the type of a term, or its value.
:=: def two : ℕ := 2 — “is defined as” or “is proved by”: what comes after it is the value or the proof.
@[simp] (attribute): @[simp] theorem add_zero' (n : ℕ) : n + 0 = n := rfl — Attributes add information to a declaration: @[simp] tells the simp tactic to use it.
_ and ?_: refine ⟨?_, ?_⟩ — A hole: Lean fills in _ by itself, and ?_ becomes a new goal to prove.
abbrev: abbrev Point := ℝ × ℝ — A definition that Lean unfolds freely, like a shorthand.
anonymous constructor ⟨ ⟩: ⟨2, by norm_num⟩ — Builds an object from its parts: a pair, a structure, or a proof of “and” or “there exists”.
axiom: axiom my_assumption : 1 = 1 — Something assumed without proof. Lean's three standard axioms (propext, Classical.choice, Quot.sound) are normal; anything beyond them is worth a closer look.
by: theorem t : 1 + 1 = 2 := by norm_num — Starts a proof made of tactics.
class: class Zero (α : Type) where zero : α — A structure that Lean finds by itself when it is needed (a type class), such as “this type has an addition”.
class inductive: class inductive Decidable (p : Prop) — A class given by the ways to build it, like inductive.
declaration: Any named thing in Lean: a theorem, a definition, and so on. Each one has a line on its file page.
def (definition): def double (n : ℕ) : ℕ := 2 * n — A name for a precise idea or a computation, such as “continuous” or “double a number”.
dot notation: n.succ — x.foo means Foo.foo x, where Foo is the type of x: n.succ is Nat.succ n.
example: example : 2 + 2 = 4 := rfl — A statement proved without a name, to show that something works.
explicit argument ( ): (n : ℕ) — An argument you write when you use the result.
goal: What is left to prove at a point in a proof. Each tactic changes the goal.
h.1, h.2: h.1 — The first and second part of h, for example of an “and”.
hypothesis (assumption): (h : 0 < n) — A named fact you may use in a proof, such as h : 0 < n.
implicit argument { }: {α : Type} — An argument Lean works out by itself from the others.
import: import Mathlib.Data.Real.Basic — Brings in the declarations of another file or library.
inductive: inductive Color | red | green — A new type given by the ways to build its elements. The natural numbers are 0, or one more than a natural number.
instance: instance : Zero ℕ := ⟨0⟩ — A proof or construction that a type belongs to a class. Lean then finds it by itself.
instance argument [ ]: [Field K] — An argument Lean finds by itself among the class instances it knows.
kernel: The small core of Lean that finally accepts or rejects a proof.
Lake: lake build — Lean's build tool. A project's lakefile says which libraries it has and which it needs.
lemma: lemma helper (n : ℕ) : n ≤ n + 1 := by omega — A theorem, usually a smaller helper for a bigger one.
Mathlib: import Mathlib — The big shared library of formalized mathematics that many Lean projects build on.
namespace: namespace Nat … end Nat — A family name for declarations: inside namespace Nat, succ_le means Nat.succ_le.
noncomputable: noncomputable def half : ℝ := 1 / 2 — Marks a definition Lean cannot run as a program, usually because it uses choice or real numbers.
opaque: opaque secret : ℕ — A definition whose value Lean keeps hidden: only its type is known.
open: open Real — Lets you use short names: after open Real, pi means Real.pi.
private, protected: private theorem helper : True := trivial — private: usable only in this file. protected: must always be written with its full name.
proof: The argument. In Lean, a proof is code, and Lean checks every step of it.
Prop: (p : Prop) — The type of statements. A statement is true or false; its proofs are its elements.
section: section … end — A part of a file whose variables and open commands end with it.
sorry: theorem later : 1 = 1 := sorry — Lean's “I have not proved this yet”. A result that uses it is not finished, and the site flags it.
structure: structure Point where x : ℝ y : ℝ — A new kind of object made of named parts (its fields).
tactic: by rw [h] ring — One command inside a proof that starts with by, such as “rewrite using this equation”. The Reading explains each one.
termination_by: termination_by n — Says why a recursive definition stops: something gets smaller each time.
theorem: theorem two_pos : 0 < 2 := by norm_num — A statement that has been proved. The proof follows :=.
universe: universe u — The size level of types (Type u). You can usually ignore it.
variable: variable (n : ℕ) (hn : 0 < n) — Names (and assumptions) used by every result below it, until its section ends.
· (focusing dot): constructor · norm_num · simp — Starts the proof of one goal when there are several.