Constructing numbers, then proving convergence#

This is an advanced course. Begin with confidence in Lean's functions, structures, propositions, intro, rw, calc, and existential witnesses. You should also be comfortable with fractions, inequalities, and the idea of an epsilon argument. The unit notes introduce quotient constructions and explain how the mathematics determines the shape of a Lean proof.

The course has three connected tasks: identify fractions that represent the same rational number; identify Cauchy sequences that represent the same real number; prove that Cauchy sequences of reals have limits. The last task is stronger than showing that a rational Cauchy sequence represents a real.

MyRat and MyReal are this course's constructions in the Analysis namespace. They are distinct from Lean's built-in numeric types and from Mathlib's types. A theorem name such as MyRat.add_comm tells you which number system it concerns. Sequence indices use ordinary natural numbers.

The imports provide substantial proved infrastructure: quotient operations, boundedness and product estimates, positivity, inverse construction, and order tools. You prove the statements in the exercise files using that infrastructure. A completed exercise does not mean that you independently constructed every supporting theorem.

Exercise files state the theorem, its role, and at most a sentence of strategy. The unit notes carry the toolkit: every lemma a world needs is listed there once, with its statement, next to a worked example on a statement that is not one of the exercises. Choosing which tool to use, and in what order, is the exercise. #check @name shows a lemma's statement, exact? in place of a proof searches for a lemma that closes the goal, and lake exe leanlings hint gives a next step when you are stuck.

Before starting a proof, write its mathematical plan in two or three sentences. In a quotient proof, name the representatives and the relation you must establish. In a convergence proof, name the tolerance, threshold, and eventual estimate. Then translate one sentence at a time into Lean.

Three passes through the construction#

Pass	Units	Central proof obligation
Fractions to rationals	Setoid, WellDef, Rat, RatOrder	Equivalent representatives give the same arithmetic and order.
Rational sequences to reals	Cauchy, Real, Capstone	Differences tending to zero define equality, and a rational Cauchy sequence represents its limit.
Completeness for real sequences	Metric, RealField, Complete	Rational approximations connect a Cauchy sequence of reals to a represented limit.

Pause after each pass. For the first, explain why reading a fraction's numerator cannot define a function on rationals. For the second, explain why pointwise equality is sufficient but unnecessary for two sequences to represent the same real. For the third, identify what must be proved about the approximating sequence before it can represent a real.

Keep the proof obligations separate#

A quotient proof often ends in integer arithmetic. Before using grind, name the relation or operation you unfolded and read the resulting equation. Automation checks that equation; the choice to reduce to representatives is the mathematical part you need to understand and be able to repeat.

In an epsilon argument, maintain a small ledger: the target tolerance, the share allocated to each error, and the threshold where each bound holds. Take a maximum only after identifying all the bounds it must satisfy. Use Nat.le_trans to pass from the common threshold to an individual one.

Finally, keep types visible. Indices are Nat, tolerances are positive MyRat values, and distances between reals are MyReal values. An ofRat conversion often marks the boundary between two parts of the argument. The final unit practices its three-error Cauchy estimate and two-error convergence estimate separately, then asks you to assemble them.

Welcome to Real Analysis from Scratch! You will construct the rational and real numbers with supplied core-Lean libraries, and develop their theory through Cauchy sequences toward the completeness of ℝ. The path: construct ℚ as a quotient of fractions (proving the equivalence relation and that the operations are well defined), develop its arithmetic and order theory (absolute value, the Archimedean property, density), build Cauchy sequences, and assemble ℝ as their quotient. Two ideas recur. (1) A statement about ℚ reduces, via `mk_eq` and the computation lemmas, to one about integers that `grind`/`omega` close. (2) A statement about ℝ reduces, via the quotient, to one about its Cauchy-sequence representatives — often pointwise to the ℚ fact you already proved. Each world's unit notes (`lake exe leanlings guide`) introduce its idea and list the lemmas it needs; each exercise states the theorem and at most a sentence of strategy. Choosing the tools is the exercise. Use `#check` to read a lemma and `exact?` to search; `lake exe leanlings hint` gives a next step when you are stuck. Replace the `sorry` with a proof, then run `lake exe leanlings run` (or use watch mode). This is an advanced course: bring the tactics from Intro plus confidence with fractions, inequalities, and epsilon arguments. The guides introduce quotients. The imports supply proved infrastructure for operations, bounds, and inverses; your exercises prove the selected steps connecting them to completeness.