Examples

Each example gives a statement, the view Definograph drew for it, and how to read that view: what it shows and what it leaves out.

The views are recorded output. Each statement is an entry in Definograph’s Statement menu; Lean 4.28.0 reads it with Definograph’s pinned copy of Mathlib. To draw one yourself, run Definograph on your own computer (see Try it yourself) and choose the statement from that menu.

For a library theorem read in the editor, follow Reading the Lebesgue-number lemma: identify its hypotheses, compare its choices and read its whole-ball conclusion. It has its own downloadable file and Mathlib requirements.

Which choice may depend on which

In ∀ x : ℝ, ∃ y : ℝ, x < y, may the choice of y use the value of x?

Recorded Definograph output · Lean 4.28.0 · 28 September 2026

Lean statement, as entered in Definograph

∀ x : ℝ, ∃ y : ℝ, x < y

A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.

Scope and dependency

∀ a value from the full domain∃ a candidate chosen at this stage

1
Arbitrary choicex : ℝ
An arbitrary element of this type. A displayed sample represents one choice, never every element.
2
Candidate witnessy : ℝ
Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.
May depend on
x

Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.

Definograph’s Choices view, tagged “Scope and dependency”. x is chosen first; y comes second, and its May depend on list names x. The small a before x marks its kind, a number. The view leaves out the condition x < y.

What it shows: The two quantified variables in reading order: x is an arbitrary choice at step 1, y a candidate witness at step 2. Under y, May depend on lists x, so y may be chosen differently for each x.
What it leaves out: The condition x < y, and any value for y. The view neither finds nor checks a witness, and does not say whether the statement is true. (It is true: take y = x + 1.)

A choice fixed before the others

With the quantifiers swapped, ∃ y : ℝ, ∀ x : ℝ, x < y, what may y depend on?

Recorded Definograph output · Lean 4.28.0 · 28 September 2026

Lean statement, as entered in Definograph

∃ y : ℝ, ∀ x : ℝ, x < y

A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.

Scope and dependency

∀ a value from the full domain∃ a candidate chosen at this stage

1
Candidate witnessy : ℝ
Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.
Chosen without earlier values. Later choices cannot change this witness.
2
Arbitrary choicex : ℝ
An arbitrary element of this type. A displayed sample represents one choice, never every element.
Earlier choices in this scope
y

Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.

The Choices view with the quantifiers swapped. y is chosen first, “without earlier values”; x lists y under Earlier choices in this scope. The view leaves out the condition x < y.

What it shows: y now comes first and is chosen without earlier values, so later choices cannot change it. One y would have to work for every x.
What it leaves out: The condition, and that this statement is false: no real number is larger than every real number, itself included. The view has the same kinds of steps for the true statement above and for this false one.

The outline of a longer statement

In an ε–δ statement, which parts are assumed, which are required, and under which assumptions?

Recorded Definograph output · Rendered 2 October 2026 · from saved results · Adapts to page theme · Native capture date unavailable · Dates in UTC · Saved input: Lean 4.28.0 · Lean was not rerun.

Lean statement, as entered in Definograph

∀ ε : ℝ, 0 < ε →
  ∃ δ : ℝ, 0 < δ ∧
  ∀ x : ℝ, |x| < δ → |x * x| < ε

Definograph’s outline of the whole statement, beside the first step of its Visual sequence. Each choice, assumption and requirement sits in its logical place; the highlighted entry is the current step. It is an outline of the statement, not a proof.

What it shows: The statement as nested entries. For every ε, given 0 < ε, there is a δ with all of its conditions: 0 < δ, and for every x, given |x| < δ, then |x · x| < ε. Each assumption is written before what depends on it.
What it leaves out: The figures of the individual steps, and any numerical example. The outline comes from the statement as Lean has read it; it is not a proof and does not say whether the statement is true.

Relations and the roles of their objects

In ∀ (A B : Set ℝ) (x : ℝ), A ⊆ B → x ∈ A → x ∈ B, which relations are assumed, and which one is required?

Lean statement, as entered in Definograph

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

Read each relation through its objects and their roles. Repeated objects stay linked across views.

Symbolic view

Set inclusion

is a subset of

Premise of an implication

subsetASet ℝsupersetBSet ℝ

Membership

belongs to

Conditional on the premisePremise of an implicationUnder 1 assumption

elementxℝsetASet ℝ

Membership

belongs to

Conditional on the premiseUnder 2 assumptions

elementxℝsetBSet ℝ

These are diagrams of mathematical roles. Relative position and distance carry no geometric meaning.

Definograph’s Relationships view, tagged “Symbolic view”: one card per relation, with each object in its role and tags that say where the relation sits in the statement. A relation under an assumption is not claimed to hold.

What it shows: Three cards. A ⊆ B is a set inclusion with A as subset and B as superset; x ∈ A and x ∈ B are memberships with x as element. The tags say where each relation sits: the inclusion is the premise of an implication, x ∈ A is under one assumption, and the conclusion x ∈ B is under two.
What it leaves out: Whether any relation holds. A relation drawn under an assumption is not a claim that it holds, and the positions of the cards carry no meaning.

Every object and relation at once

In the same statement, which objects does each relation use, and which objects do the relations share?

Lean statement, as entered in Definograph

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

Shared objects connect the parts of this statement.

Structural view

Context carried by these fragments

Premise of an implication

Conditional on the premiseUnder 1 assumption

Conditional on the premisePremise of an implicationUnder 1 assumption

1 further context; inspect an individual relation.

Connections show expression structure. A relation may occur inside an assumption, negation, or alternative; its presence is not a claim that it holds.

The Structure view with nothing selected: the objects on the left, the three relations on the right, and a connector for each role an object fills. Position and the curves of the connectors carry no meaning.

What it shows: Nine objects and three relations. The inclusion uses A as subset and B as superset; each membership uses x as element and A or B as set. So A, B and x each connect to two relations. Some objects are not written in the statement: a, the name Lean gives each unnamed hypothesis, and x.cauchy, a field of the structure of ℝ. The propositions appear under Lean’s internal names: HasSubset.Subset(A, B) is A ⊆ B, and Membership.mem(A, x) is x ∈ A.
What it leaves out: Which relation is assumed. The context tags under the map say that relations occur as premises and under assumptions, but not which tag belongs to which relation; the Relationships view above shows that. Position, distance and the curves of the connectors carry no meaning.

Trace one object through a statement

In ∀ (A B C : Type) (f : A → B) (g : B → C) (h : A → C) (x : A), g (f x) = h x, which relations does x take part in?

Recorded Definograph output · Lean 4.28.0 · 28 September 2026

Lean statement, as entered in Definograph

∀ (A B C : Type) (f : A → B) (g : B → C)
  (h : A → C) (x : A), g (f x) = h x

Shared objects connect the parts of this statement.

Structural view

Connections show expression structure. A relation may occur inside an assumption, negation, or alternative; its presence is not a claim that it holds.

The Structure view with the object x selected. The connectors of x are drawn heavier, the others are muted, and the relations that use x are marked. Position and the curves of the connectors carry no meaning.

What it shows: The Structure view with x selected, as you would select it in the app; the relations that use x are marked. Both sides of the equation start from x: one through f and then g, the other through h.
What it leaves out: Anything about x beyond the relations it appears in. There are no concrete functions or coordinates, and the equation is what the statement claims, not something Definograph checks.

In the app, the Visual sequence can trace x too: with x selected, a dashed line, the identity thread, joins every place where the same x appears. The line’s route means nothing: it only links the places, and it is not a path or a movement. Definograph draws the thread from the positions of the page’s elements, so this site has no recorded figure of it.

Membership regions of a compound set

In ∀ (α : Type) (A B C : Set α) (x : α), x ∈ (A ∪ B) ∩ Cᶜ → x ∈ (A \ C) ∪ (B \ C), what does the assumption allow for x?

Lean statement, as entered in Definograph

∀ (α : Type) (A B C : Set α) (x : α),
  x ∈ (A ∪ B) ∩ Cᶜ → x ∈ (A \ C) ∪ (B \ C)

In scope∀ α : Type∀ A : Set α∀ B : Set α∀ C : Set α∀ x : α

Given assumption

Condition

Read the membership condition

The condition places x in ((A ∪ B) ∩ Cᶜ) within this logical context.

x belongs to ((A ∪ B) ∩ Cᶜ)

x∈((A ∪ B) ∩ Cᶜ)

upper leftA

upper rightB

lowerC

The named element must belong somewhere in the highlighted region; no particular membership combination is chosen.

How this set is constructed 3 steps

A∪B(A ∪ B)
CᶜCᶜ
(A ∪ B)∩Cᶜ((A ∪ B) ∩ Cᶜ)

Regions encode membership combinations, not elements or sizes. Drawing a region does not assert that it contains an element.

Lean fragment and source context

x ∈ (A ∪ B) ∩ Cᶜ

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

Step 6 of 10, “Read the membership condition”: the assumption x ∈ (A ∪ B) ∩ Cᶜ as the membership regions it allows inside the type α.

What it shows: The type α as a box with circles for A, B and C. The highlighted regions are the membership combinations the assumption allows: in A only, in B only, or in both, each outside C. The element must lie somewhere in the highlighted part.
What it leaves out: Sizes, elements and whether any region is inhabited: the regions encode membership combinations only. This condition is the assumption of an implication, not a claim that it holds.

What a coloring requires on each edge

In ∀ (V C : Type) (G : SimpleGraph V) (c : G.Coloring C) (u v : V), G.Adj u v → c u ≠ c v, what does the coloring c promise?

Lean statement, as entered in Definograph

∀ (V C : Type) (G : SimpleGraph V)
  (c : G.Coloring C) (u v : V),
  G.Adj u v → c u ≠ c v

In scope∀ V : Type∀ C : Type∀ G : SimpleGraph V∀ c : G.Coloring C∀ u : V∀ v : V

Conditional conclusion

Given

G.Adj u v

Construction

Follow the coloring

Read the color assignment and the different-color constraint on every edge. No concrete coloring is chosen.

Constructing part of c(u) is not equal to c(v)

Apply the proper coloringSymbolic graph structure

GraphGusing coloringc

Inputuapplycc(u)source application

This typed coloring assigns a label to each vertex. For every adjacent pair, its two assigned labels must differ.

Color type or boundC

This type or bound is retained symbolically; no finite palette or cardinality is inferred.

Endpoint slots stand for arbitrary inputs to the rule. They do not instantiate vertices, assert that an edge exists, or determine the graph’s size or shape.

Lean fragment and source context

c u ≠ c v

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

Step 4 of 6 of Definograph’s Visual sequence, “Follow the coloring”. Its stage label, Construction, means that the step builds part of the conclusion: here c(u), one side of c(u) ≠ c(v). The figure shows the rule the coloring c carries for every edge; v₁ and v₂ stand for the two endpoints of any edge, not for u and v.

What it shows: The step applies c to u, under the assumption that u and v are adjacent. The figure shows the rule a proper coloring carries for every edge: if two endpoints are adjacent, their labels differ. The color type C stays symbolic.
What it leaves out: A graph. The endpoint slots stand for arbitrary inputs to the rule; they do not pick vertices, assert that an edge exists, or fix the size or shape of the graph. No coloring and no number of colors is chosen.

A ball as a distance condition

In the statement below, what does P ∈ Metric.ball c ε require of P?

Lean statement, as entered in Definograph

∀ (c : EuclideanSpace ℝ (Fin 2)) (ε : ℝ),
  0 < ε → ∀ P : EuclideanSpace ℝ (Fin 2),
  P ∈ Metric.ball c ε → dist P c < ε

In scope∀ c : EuclideanSpace ℝ (Fin 2)∀ ε : ℝ∀ P : EuclideanSpace ℝ (Fin 2)

Conditional conclusion
Given assumption

Given

0 < ε

Condition

Read the membership condition

The condition places P in Metric.ball(c, ε) within this logical context.

P belongs to Metric.ball(c, ε)

Open ballSymbolic geometry

dist(P, c) < ε

Uses the local assumption 0 < ε. Schematic positions; no coordinates chosen. Named points may coincide. Boundary excluded.

Lean fragment and source context

P ∈ Metric.ball c ε

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

Step 7 of 9 of the Visual sequence, “Read the membership condition”: membership in the open ball read as the distance condition, drawn schematically.

What it shows: The membership read as dist(P, c) < ε, drawn as an open disc with center c, radius ε and a named point P. The figure notes that it uses the local assumption 0 < ε and that the boundary is excluded.
What it leaves out: Coordinates and sizes: the positions are schematic, and named points may coincide. Here the membership is an assumption of the implication, not a claim that P lies in the ball. Numerical samples belong to a different view.

One numerical sample

What does the same statement look like for particular values?

Lean statement, as entered in Definograph

∀ (c : EuclideanSpace ℝ (Fin 2)) (ε : ℝ),
  0 < ε → ∀ P : EuclideanSpace ℝ (Fin 2),
  P ∈ Metric.ball c ε → dist P c < ε

01Open ball in 2D

Numerical illustration

Assumption of an implicationUnder 1 local assumption

Euclidean metric · L2Full two-dimensional view

Open ball · boundary excludedRepresentative point

Why this view

The elaborated metric supports an explicit geometric view of this region.

A numerical illustration from Explore a sample: the open ball with ε = 1 around c = (0, 0) and the point P at its center. It is one sample of values, not the statement. In the app you can move the point by clicking or dragging; in this recording nothing moves.

What it shows: One sample from Explore a sample: ε = 1, the center c at the origin and the point P at the center, so here P lies in the ball. The disc is the open ball in the Euclidean metric, boundary excluded.
What it leaves out: The statement itself. A sample is an illustration under chosen values, not a proof, and other values can make the condition fail.

A map that is inverse only on a region

In ∀ (A B : Type) (e : PartialEquiv A B) (x : A), x ∈ e.source → e.symm (e x) = x, why is the assumption x ∈ e.source needed?

Lean statement, as entered in Definograph

∀ (A B : Type) (e : PartialEquiv A B) (x : A),
  x ∈ e.source → e.symm (e x) = x

In scope∀ A : Type∀ B : Type∀ e : PartialEquiv A B∀ x : A

Conditional conclusion

Given

x ∈ e.source

Construction

Follow the inverse map

Follow the stored map to its output. Applying the function does not by itself establish membership in a validity region.

Constructing part of e.symm(e(x)) equals x

Apply the inverse mapAbstract regions and maps

MapebetweenAandB

Source expressione.toFun(x)inverse map e.symm(e(x))

Region membership must come from the surrounding statement.

For every element in the source region

x

$e$

{e}\left(x\right)

${e}^{-1}$

x

Back to the same source element

For every element in the target region

y

${e}^{-1}$

{{e}^{-1}}\left(y\right)

$e$

y

Back to the same target element

This is the application appearing in the statement. Its type alone does not establish membership in the valid region; the round-trip law requires that membership.

The letters in the round trips are schematic bound variables, not chosen points. Region frames indicate containment, not shape, size, dimension, connectedness, or a proper subset. The inverse laws apply on the specified regions; no inverse law is asserted on the whole carriers.

Lean fragment and source context

↑e.symm (↑e x) = x

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

Step 6 of 7 of the Visual sequence, “Follow the inverse map”: from x through e and back through e.symm, on the designated source region.

What it shows: The two carriers with the regions e.source and e.target, each marked as possibly empty; the maps e and its inverse between them; and the two round trips that return to their start, for every element of each region.
What it leaves out: Geometry: the carriers are abstract containers without shape, size or dimension. The inverse laws hold on the designated regions only. Applying e to x does not by itself put x in the source region; the statement assumes it.

Inside a structure

In the same statement, what does e : PartialEquiv A B contain?

Lean statement, as entered in Definograph

∀ (A B : Type) (e : PartialEquiv A B) (x : A),
  x ∈ e.source → e.symm (e x) = x

Objects and choices

For every A, B, e, x

Read these objects as arbitrary choices of their stated types, in the displayed binder order.

Read the underlying fields and laws

Object structure

Inside e

PartialEquiv A B

4 data fields · 3 laws

These fields belong to this object, within the statement’s current quantifiers and assumptions.

What it contains

Field names and declared types

toFun: A → B
invFun: B → A
source: Set A
target: Set B

Arrows show function types. Set frames show membership domains, with no coordinates, shape, size, or chosen elements.

What its fields must satisfy

Read each law in declaration order.

1 / 3

1map_source'2map_target'3left_inv'

map_source'Law of this object

Visual readingSymbolic schematics · no numerical choices

In scopeA : TypeB : Typee : PartialEquiv A B

Objects and choices

For every x

Read these objects as arbitrary choices of their stated types, in the displayed binder order.

x:A

Types and maps

Atype · in scope

x: A

Arrows show declared function types. Named elements retain their types; no coordinates, cardinalities, or additional properties are assigned.

Lean fragment and source context

∀ ⦃x : A⦄, x ∈ e.source → ↑e x ∈ e.target

Full visual statement

Parameters

A:Type

B:Type

e:PartialEquiv A B

Types and maps

Atype

Btype

Arrows show declared function types. Named elements retain their types; no coordinates, cardinalities, or additional properties are assigned.

An equivalence between specified regionsAbstract regions and maps

MapebetweenAandB

For every element in the source region

x

$e$

{e}\left(x\right)

${e}^{-1}$

x

Back to the same source element

For every element in the target region

y

${e}^{-1}$

{{e}^{-1}}\left(y\right)

$e$

y

Back to the same target element

The forward map takes the source region to the target region. The inverse takes the target back to the source, and each undoes the other on its valid region.

For every

x:A

Types and maps

Atype · in scope

x: A

Arrows show declared function types. Named elements retain their types; no coordinates, cardinalities, or additional properties are assigned.

Given

x belongs to e.source

Membership condition · the named element belongs to the region

Then

e.toFun(x) belongs to e.target

Membership condition · the named element belongs to the region

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

1 further field remains in the declared type. Further field readings exceed the optional structure payload budget.

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

Step 1 of 7 opens the declared structure of e: four data fields and three laws, and a closing line saying that one further field is not shown.

What it shows: The fields of e with their declared types: the maps toFun and invFun, the sets source and target, and the laws that link them, read in declaration order. The fields belong to this e, inside the statement’s quantifiers.
What it leaves out: One further law: the view says that a field is not shown, because reading it would exceed Definograph’s size limit for this part. The laws are requirements of the structure, not extra assumptions and not proofs.

Opening a definition

In ∀ (α β : Type) (f : α → β), Function.Injective f → ∀ x y : α, f x = f y → x = y, what does the assumption Function.Injective f say?

Lean statement, as entered in Definograph

∀ (α β : Type) (f : α → β),
  Function.Injective f →
  ∀ x y : α, f x = f y → x = y

The Whole statement outline after Function.Injective f has been opened: the assumption now quantifies over its own two inputs. It is an outline of the statement, not a proof.

What it shows: The whole statement after Function.Injective f has been opened one step. The assumption now reads: for every a₁, a₂, given f(a₁) equals f(a₂), then a₁ equals a₂. Definograph opened it with a definition step that Lean checked for definitional equality.
What it leaves out: The figures of the individual steps, and a proof that f is injective: the opened assumption is still an assumption.

What Definograph could not interpret

In ∀ (P : ℝ × ℝ) (ε : ℝ), P ∈ Metric.ball 0 ε → Nat.Prime 17, which parts does Definograph interpret?

Lean statement, as entered in Definograph

∀ (P : ℝ × ℝ) (ε : ℝ),
  P ∈ Metric.ball 0 ε → Nat.Prime 17

Interpretation coverage 1 interpreted · 0 partial · 1 structural fragment

This reports the vocabulary used in the selected fragment. It does not measure understanding or establish the statement.

Interpreted: 1
Partly interpreted: 0
Structure only: 1

Recognized constructions

Sets and membership1 relation
Metric regions and distance1 relation

Meaning still folded or uninterpreted

Typed objects and surrounding logic remain visible. Looking inside a definition may expose constructions the reader knows.

Nat.Prime1 occurrence · 1 clause

A checked definition body is available for inspection.

Locate in statementLook inside definition

The Interpretation coverage section of the Inspect panel, for a statement with a ball condition and Nat.Prime 17: one fragment interpreted, one kept as structure only, and Nat.Prime listed under meaning still folded.

What it shows: Definograph’s Interpretation coverage: the ball condition is interpreted (sets and membership, metric regions), Nat.Prime is kept as structure only, and its definition is available to look inside.
What it leaves out: Understanding: the report counts the vocabulary a statement uses. It does not measure understanding or establish the statement.

Lean files

These files accompany the tutorial and the reference. They use Lean 4.28.0 with its standard implicit Init import; none needs Mathlib. To check one, run lean FileName.lean in its directory. The example notes give the expected result of checking each file used in the tutorial.

Downloadable Lean files
File	What it contains
QuantifierForallExists.lean	The proposition `∀ x : Nat, ∃ y : Nat, y = x`. It supplies no proof.
QuantifierExistsForall.lean	The same proposition with the quantifiers swapped. It supplies no proof.
QuantifierProofs.lean	A proof of the first proposition and a refutation of the second, shown below.
Scope.lean	Both quantifier orders, the same statement with renamed variables, and a statement that allows a constant choice.
RotorLaw.lean	A record with a law field, used in the reference. It has an intentionally unused parameter.
RotorExamples.lean	Two records of that kind, one with natural-number carrier and one with an empty carrier, and the law applied to an input.
Evidence.lean	A proof from a local hypothesis beside an unfinished proof, with their axiom reports.
ReturnMap.lean	A record of two maps and a return law, a counterexample to its converse, and a proof of injectivity.
RecordedAxiom.lean	A deliberately unfinished proof and its `sorryAx` dependency, explained under checking evidence. Checking it produces a warning that the declaration uses `sorry`.

Proof supplement: prove one order, refute the other

QuantifierProofs.leanDownload

theorem each_has_equal : ∀ x : Nat, ∃ y : Nat, y = x := by
  intro x
  exact ⟨x, rfl⟩

theorem no_one_equals_all : ¬ (∃ y : Nat, ∀ x : Nat, y = x) := by
  intro h
  obtain ⟨y, hy⟩ := h
  have impossible : (0 : Nat) = 1 := (hy 0).symm.trans (hy 1)
  exact Nat.noConfusion impossible

#print axioms each_has_equal
#print axioms no_one_equals_all

The two proofs are kept apart from the source files that form the propositions. each_has_equal chooses x as the witness for each x. no_one_equals_all derives the impossible equality 0 = 1 from the claim that one number equals every number.

Both theorems have been independently checked with Lean 4.28.0 and have no axiom dependencies. Lesson 6: Checking evidence is about the difference between forming a proposition and proving it.

Which choice may depend on which

A choice fixed before the others

The outline of a longer statement

Relations and the roles of their objects

is a subset of

belongs to

belongs to

Every object and relation at once

Trace one object through a statement

Membership regions of a compound set

What a coloring requires on each edge

A ball as a distance condition

One numerical sample

A map that is inverse only on a region

Inside a structure

What it contains

What its fields must satisfy

Given

→ Then

Opening a definition

What Definograph could not interpret

Recognized constructions

Meaning still folded or uninterpreted

Lean files

Proof supplement: prove one order, refute the other

Then