Terms, types, propositions

You already know what it means for an expression to be well typed. You know that $\hat{\tau }$ is a number, that $\hat{\tau }(\cdot )$ is a function of the assignment, and that $\mathbb{E}[\hat{\tau }]=\tau$ is a claim about numbers rather than a number itself. You know that adding a vector of outcomes to a sample size is not a typo Lean should tolerate; it is nonsense.

Lean’s one idea is to take that seriously. Every expression has a type. A statement is a type too, and a proof of that statement is a term of that type. So checking a proof is exactly the same operation as checking that a function was applied to the right kind of argument, run by the same piece of code. When someone says “the proof compiles”, this is the whole of what they mean: a term was submitted, its type was computed, and the type turned out to be the theorem.

That is a good deal for a statistician. It means the object you have to learn to read is not a proof — proofs get long and boring and the machine checks them anyway — but a statement, which is short, and which is the only place an error can hide that the compiler will not catch. This chapter is about reading statements. The rest of Part I is about what to do once you can.

Everything below is quoted from lean/MrCLean/Fundamentals/Ch01Terms.lean, which CI compiles. Run the blocks; the point of a proof assistant is lost if you only read it.

Everything has a type

Two commands do all the exploring. #check reports the type of an expression without running it. #eval runs it.

/- `#check` reports the *type* of an expression.  `#eval` runs it, when it can:
`ℝ` is not computable (a real number is an infinite object), so `#eval` works on
`ℕ`, `ℤ` and `ℚ` but not on `ℝ`.  This costs you nothing — proofs never evaluate. -/
#check (7 : ℕ)              -- 7 : ℕ
#check (-3 : ℤ)             -- -3 : ℤ
#check (2.5 : ℝ)            -- 2.5 : ℝ
#check Real.sqrt            -- Real.sqrt (x : ℝ) : ℝ

#eval (17 + 25 : ℕ)         -- 42
#eval (10 : ℚ) / 4          -- 5/2

#eval refuses on ℝ, and it is worth understanding why now rather than being surprised later. A real number in Lean is a Cauchy sequence up to equivalence: an infinite object with no finite normal form. There is nothing to print. This costs you nothing at all, because proofs do not evaluate — nobody ever needed the decimal expansion of $\mathrm{Var}(\hat{\tau })$ to prove a bound on it. When you want a number you can look at, work in ℚ; when you want mathematics, work in ℝ.

Types have types.

/- Everything has a type, including types themselves.  `Prop` is the type of
*statements*; `Type` is the type of *data*.  The distinction matters exactly
once: `ℝ` holds numbers you compute with, `Prop` holds claims you prove. -/
#check ℕ                    -- ℕ : Type
#check ℝ                    -- ℝ : Type
#check Prop                 -- Prop : Type
#check Type                 -- Type : Type 1

/- `(2 : ℝ) + 2 = 4` is not a number and not a Boolean: it is a proposition. -/
#check ((2 : ℝ) + 2 = 4)    -- 2 + 2 = 4 : Prop

/- A *proof* of that proposition is a term whose type is the proposition.
This is the whole of the Curry-Howard correspondence, and the reason the two
`#check`s above and below are literally the same command.  Lean reports the type
it *inferred* for `rfl`, namely `2 + 2 = 2 + 2`; that the term was accepted where
`2 + 2 = 4` was demanded is the content, because the two sides compute to the
same numeral. -/
#check (rfl : (2 : ℕ) + 2 = 4)   -- rfl : 2 + 2 = 2 + 2

The distinction that matters is Prop against Type. ℝ : Type — real numbers are data, and different real numbers are different. Prop is the type of statements, and (2 : ℝ) + 2 = 4 is a term of type Prop: not a number, not a Boolean, a claim.

The last #check in that block is the whole chapter in one line:

#check (rfl : (2 : ℕ) + 2 = 4)

We asked Lean for the type of the term rfl and told it to expect 2 + 2 = 4. It agreed. The proposition was used exactly as ℕ was used two lines earlier — as a type — and the proof was used exactly as 7 was — as a term of that type. This is the Curry–Howard correspondence, and after this paragraph I will stop naming it and start using it.

Definitions and functions

A def names a term. Nothing more.

/-- The sample total of a three-unit study.  `y : Fin 3 → ℚ` is an outcome
vector: `Fin 3` is the type with exactly three elements `0, 1, 2`, so a function
out of it is a list of three numbers indexed by unit. -/
def totalOfThree (y : Fin 3 → ℚ) : ℚ := y 0 + y 1 + y 2

/-- A concrete outcome vector.  `![a, b, c]` is Mathlib's notation for the
function `Fin 3 → ℚ` sending `0 ↦ a`, `1 ↦ b`, `2 ↦ c`. -/
def outcomes : Fin 3 → ℚ := ![2, 5, 11]

/- Function application is juxtaposition: `f x`, never `f(x)`. -/
#eval outcomes 1                  -- 5
#eval totalOfThree outcomes       -- 18
#check totalOfThree               -- totalOfThree (y : Fin 3 → ℚ) : ℚ

/-- Definitions unfold when Lean checks an equation, so `rfl` — "both sides
reduce to the same thing" — proves that a definition means what it says. -/
theorem totalOfThree_apply (y : Fin 3 → ℚ) : totalOfThree y = y 0 + y 1 + y 2 := rfl

Note the type Fin 3 → ℚ standing in for “an outcome vector of length three”. Fin n is the type with exactly $n$ elements, so a function out of it is an $n$-vector indexed by unit, and an index is guaranteed in range by its type — there is no bounds check to write and no out-of-range case to handle. Chapter 3 takes this apart properly; for now, read Fin n → ℝ as $y\in {\mathbb{R}}^n$.

Function application is juxtaposition: f x, not f(x). Parentheses in Lean group, they do not apply, so f (x + 1) needs them and f x does not.

The last line of that snippet deserves a second look:

theorem totalOfThree_apply (y : Fin 3 → ℚ) : totalOfThree y = y 0 + y 1 + y 2 := rfl

rfl proves it because both sides reduce to the same term once the definition is unfolded. This is how you check that a definition means what you intended, and it is the cheapest sanity check available. It is also, as the last section of this chapter shows, how an empty theorem gets written by accident.

Every Lean function takes one argument.

/-- Every Lean function takes exactly one argument.  `scale c y` looks like a
two-argument function, but its type is `ℚ → ((Fin 3 → ℚ) → (Fin 3 → ℚ))`: hand
it `c` and you get back a function waiting for `y`.  This is *currying*, and it
is why partial application always works. -/
def scale (c : ℚ) (y : Fin 3 → ℚ) : Fin 3 → ℚ := fun i => c * y i

#check scale                 -- scale (c : ℚ) (y : Fin 3 → ℚ) : Fin 3 → ℚ
#check scale 2               -- (Fin 3 → ℚ) → Fin 3 → ℚ   (still a function)
#eval scale 2 ![1, 2, 3] 0   -- 2

/-- `fun i => …` is how you write an anonymous function; `scale` is defined by
one.  Doubling then reading off unit `2` is the same as reading off unit `2`
then doubling — and `rfl` sees it, because both sides compute. -/
theorem scale_apply (y : Fin 3 → ℚ) : scale 2 y 2 = 2 * y 2 := rfl

#check scale prints the signature with its binders named, but the type it denotes is ℚ → (Fin 3 → ℚ) → (Fin 3 → ℚ), and → associates to the right, so that is ℚ → ((Fin 3 → ℚ) → (Fin 3 → ℚ)): give it a scalar and you get back a function waiting for a vector, which is what #check scale 2 reports. Partial application therefore always works, and you will see it constantly in Mathlib, where a lemma about f is applied to half its arguments and passed along as an argument itself.

example, theorem, and what rfl is not

/-- `example` states and proves a fact without naming it: use it to check your
understanding without polluting the namespace. -/
example : (2 : ℕ) + 2 = 4 := rfl

/-- `theorem` is the same thing with a name, so later proofs can cite it.
(`lemma` is a synonym; nothing in Lean distinguishes them.) -/
theorem two_plus_two : (2 : ℕ) + 2 = 4 := rfl

/-- `rfl` is not magic: it closes a goal only when both sides reduce to the same
normal form.  It does closed arithmetic, and it unfolds definitions — which is
how you check that a definition says what you meant.  It does *not* do algebra:
`a + b = b + a` needs `add_comm`.

(`noncomputable` is required of every `ℝ`-valued definition, because real
division has no algorithm.  It changes nothing about proofs.) -/
noncomputable def sampleMean (a b : ℝ) : ℝ := (a + b) / 2

theorem sampleMean_eq (a b : ℝ) : sampleMean a b = (a + b) / 2 := rfl

example states and proves something without naming it: use it to check your understanding. theorem gives it a name so later proofs can cite it. lemma is a synonym — Lean does not distinguish them, and any hierarchy you read into the two words is yours, not the compiler’s.

rfl is not a proof method, it is a term: the constructor of Eq saying “this thing equals itself”. It closes a goal exactly when both sides reduce to the same normal form. So it does closed arithmetic (2 + 2 and 4 both reduce to 4), and it unfolds definitions, and it does not do algebra: a + b = b + a is not an instance of “both sides are the same term”, and needs add_comm.

Propositions are types, proofs are terms

Here is the payoff for taking the correspondence seriously: → is one symbol doing two jobs, and they are the same job.

/-- `→` is one symbol doing two jobs.  As a *type former* it builds functions:
`Fin 3 → ℝ` is an outcome vector. -/
def constantOutcomes : Fin 3 → ℝ := fun _ => 4

/-- As a *proposition former* it is implication.  And a proof of `p → q` is
exactly a function taking a proof of `p` to a proof of `q`, written with the
same `fun`.  Here: if every unit's treated outcome is at least its control
outcome, then in particular unit `0`'s is. -/
theorem effect_nonneg_at_zero (y1 y0 : Fin 3 → ℝ) :
    (∀ i, y0 i ≤ y1 i) → y0 0 ≤ y1 0 :=
  fun h => h 0

As a type former, Fin 3 → ℝ is the type of outcome vectors. As a proposition former, p → q is implication. And the proof of an implication is written fun h => …, with the same keyword as an anonymous function, because it is an anonymous function: it takes a proof of the hypothesis and returns a proof of the conclusion. In effect_nonneg_at_zero the proof is fun h => h 0, which reads: given the assumption h, apply it at unit 0. Applying a hypothesis and applying a function are the same operation.

This unification is why the table below is short. Each connective has one way in and one way out; in every case the way in is “build a term” and the way out is “take the term apart”.

The rest of this section is that table with one worked example per row.

∀

/-- `∀ i, P i` is introduced exactly like a function: `fun i => (proof of P i)`.
Here we prove that scaling a vector by `1` changes nothing, unit by unit. -/
theorem one_scale (y : Fin 3 → ℝ) : ∀ i, 1 * y i = y i :=
  fun i => one_mul (y i)

/-- A `∀` is *used* by applying it, again like a function. -/
theorem one_scale_at_two (y : Fin 3 → ℝ) : 1 * y 2 = y 2 :=
  one_scale y 2

∀ i, P i is a dependent function type: a function from i to a proof of P i, where the type of the output depends on the input. That is the only difference between → and ∀, and it is why fun i => one_mul (y i) is a proof of ∀ i, 1 * y i = y i. To use a ∀, apply it, as one_scale y 2 does.

If you take one thing from this chapter, take this: in a statement, ∀ costs nothing and means everything. theorem HT_unbiased (D : Design n) … quantifies over every design in the universe. Chapter 8 makes that claim; the reason it is worth making is that the ∀ is genuinely unconstrained.

∃

/-- `∃ i, P i` is introduced with the anonymous constructor `⟨witness, proof⟩`:
you must actually produce the unit, Lean will not take your word for it. -/
theorem exists_treated : ∃ i : Fin 3, (![2, 5, 11] : Fin 3 → ℚ) i = 5 :=
  ⟨1, rfl⟩

/-- An `∃` is *used* by taking it apart, which in term mode is a pattern-matching
`fun ⟨i, hi⟩ => …`: from a unit whose treated outcome is `3` we get a unit whose
treated outcome is positive. -/
theorem exists_pos_of_exists_eq_three (y : Fin 3 → ℝ) :
    (∃ i, y i = 3) → ∃ i, 0 < y i :=
  fun ⟨i, hi⟩ => ⟨i, by rw [hi]; norm_num⟩

The anonymous constructor ⟨_, _⟩ builds a term of any structure type, and ∃ i, P i is a structure with two fields: the witness and the proof. You must produce the unit. Lean will not accept “such a unit must exist” as an argument unless you have a term that says why.

Going the other way, an ∃ in a hypothesis is taken apart by pattern matching: fun ⟨i, hi⟩ => … binds the witness to i and its property to hi. The tactic spelling of the same move is obtain, in chapter 2.

∧ and ∨

/-- `p ∧ q` is introduced by `⟨proof of p, proof of q⟩` and eliminated by the
projections `.1` and `.2`.  Structurally it is an ordered pair of proofs. -/
theorem and_intro_example (y : Fin 3 → ℝ) (h0 : 0 ≤ y 0) (h1 : 0 ≤ y 1) :
    0 ≤ y 0 ∧ 0 ≤ y 1 :=
  ⟨h0, h1⟩

theorem and_elim_example (y : Fin 3 → ℝ) (h : 0 ≤ y 0 ∧ 0 ≤ y 1) : 0 ≤ y 1 :=
  h.2

Structurally, p ∧ q is an ordered pair. Build it with ⟨_, _⟩, project out of it with .1 and .2. There is no more to it.

/-- `p ∨ q` is introduced by naming *which* side you can prove: `Or.inl` for the
left, `Or.inr` for the right.  A unit is either treated or not; here we know
which. -/
theorem or_intro_example (i : Fin 3) (h : i ∈ ({0, 1} : Finset (Fin 3))) :
    i ∈ ({0, 1} : Finset (Fin 3)) ∨ i = 2 :=
  Or.inl h

/-- `p ∨ q` is *used* by handling both cases: `Or.elim` takes the disjunction and
one function per side.  This is case analysis on the treatment status. -/
theorem or_elim_example (y : Fin 3 → ℝ) (h : y 0 = 1 ∨ y 0 = 2) : 0 < y 0 :=
  Or.elim h (fun h1 => by rw [h1]; norm_num) (fun h2 => by rw [h2]; norm_num)

p ∨ q is the asymmetric one. To prove a disjunction you must say which side you have: Or.inl for the left, Or.inr for the right. To use one you must handle both sides, which is what Or.elim takes its two function arguments for. In this subject the disjunction is almost always “unit $i$ was treated, or it was not”, and the two-case structure of or_elim_example is the shape of every argument about an indicator.

¬

/-- `¬ p` is *defined* to be `p → False`: a proof of `¬ p` is a machine turning a
proof of `p` into a contradiction.  So it is introduced by `fun hp => …`. -/
theorem not_neg_of_nonneg (x : ℝ) (h : 0 ≤ x) : ¬ (x < 0) :=
  fun hlt => absurd h (not_le.mpr hlt)

/-- `absurd : p → ¬p → q` is the term-level "from a contradiction, anything".
Once you have both a claim and its negation, every goal is provable — which is
exactly why a formalization with contradictory hypotheses proves nothing. -/
theorem anything_from_contradiction (n : ℕ) (h : 0 < n) (h' : n = 0) : 1 = 2 :=
  absurd h (by rw [h']; exact lt_irrefl 0)

¬ p is not primitive. It is notation for p → False, where False is the proposition with no proofs. So a proof of ¬ p is a function turning a proof of p into a contradiction, and it is introduced with fun like any other function.

The second theorem in that block is the one to remember:

theorem anything_from_contradiction (n : ℕ) (h : 0 < n) (h' : n = 0) : 1 = 2

From contradictory hypotheses, anything follows — absurd : p → ¬p → q, with q arbitrary. A formalization whose hypotheses cannot all hold is provable and says nothing whatsoever. This is not a hypothetical failure mode; it is the single most common way an autoformalized theorem is wrong while being green in the editor, and chapter 5 turns it into a checklist item.

↔

/-- `p ↔ q` is a structure with two fields, the two implications.  Build it with
`Iff.intro` (or `⟨_, _⟩`) and use it with `.mp` (left-to-right) and `.mpr`. -/
theorem nonneg_iff_zero_le (x : ℝ) : 0 ≤ x ↔ ¬ (x < 0) :=
  Iff.intro (fun h => not_lt.mpr h) (fun h => not_lt.mp h)

theorem use_iff (x : ℝ) (h : 0 ≤ x) : ¬ (x < 0) :=
  (nonneg_iff_zero_le x).mp h

p ↔ q is a structure with two fields, the two implications. .mp is left-to-right (modus ponens), .mpr is right-to-left (reverse). You will use these constantly, because a large fraction of Mathlib’s usable content is stated as ↔ — sub_eq_zero, not_lt, div_lt_one, Nat.cast_ne_zero — and picking the right projection is half of applying it.

Implicit and instance arguments

Three kinds of brackets appear in a Lean signature, and the difference is who supplies the argument.

/-- Arguments in `{ }` are *implicit*: Lean infers them from the other
arguments, so you never write the type `α` or the size `n` by hand. -/
theorem first_eq_first {α : Type} {n : ℕ} (y : Fin (n + 1) → α) : y 0 = y 0 := rfl

/- `@` turns every implicit argument back into an explicit one.  Reading a
Mathlib lemma with `#check @` is the fastest way to see what it really takes. -/
#check @first_eq_first          -- ∀ {α : Type} {n : ℕ} (y : Fin (n+1) → α), y 0 = y 0
#check @add_comm                -- ∀ {G} [AddCommMagma G] (a b : G), a + b = b + a

(x : ℝ) is explicit: you write it. {α : Type} is implicit: Lean works it out from the other arguments, which is why you write first_eq_first y and never mention α or n. @ makes every implicit argument explicit again, and #check @some_lemma is the fastest way to see what a Mathlib lemma really takes — worth doing before every use of a lemma you have not used before.

/-- Arguments in `[ ]` are *instance* arguments: Lean fills them by searching a
database of registered instances.  This is how one definition of "sum" works for
`ℕ`, `ℤ`, `ℝ` and matrices at once: `[AddCommMonoid M]` says "whatever `M` is, it
has an associative, commutative `+` with a zero". -/
def totalOver {M : Type} [AddCommMonoid M] (y : Fin 3 → M) : M := y 0 + y 1 + y 2

#eval totalOver (![1, 2, 3] : Fin 3 → ℕ)   -- 6
#check @totalOver                          -- {M : Type} → [AddCommMonoid M] → (Fin 3 → M) → M

/- When you read an autoformalized statement, the `[ ]` arguments are where the
mathematical setting hides: `[Fintype ι]` means "finitely many units",
`[LinearOrder R]` means "the outcomes are comparable", and so on. -/

[AddCommMonoid M] is an instance argument, filled by a search over a database of registered instances. This is how one ∑ works for ℕ, ℝ, matrices and functions at once: the notation is defined for any type with a registered commutative addition, and Lean finds the registration.

Exercises

Every exercise below is a region of the same verified file, with the proof replaced by sorry. The solutions compile in CI. Do them in term mode, with at most a by norm_num tucked inside a bracket, because the point is to feel that a proof is a term you build rather than a sequence of commands you run. Tactics are chapter 2.

/-- The individual treatment effect of unit `i`. -/
def effect (y1 y0 : Fin 2 → ℚ) (i : Fin 2) : ℚ := y1 i - y0 i

/-- Exercise (warm-up).  Show that the definition means what it says at unit `1`.
Both sides reduce to the same term once `effect` is unfolded, so this needs no
tactic at all: one four-letter term will do. -/
theorem ex_effect_apply (y1 y0 : Fin 2 → ℚ) : effect y1 y0 1 = y1 1 - y0 1 :=
  sorry

/-- The individual treatment effect of unit `i`. -/
def effect (y1 y0 : Fin 2 → ℚ) (i : Fin 2) : ℚ := y1 i - y0 i

/-- Exercise (warm-up).  Show that the definition means what it says at unit `1`.
Both sides reduce to the same term once `effect` is unfolded, so this needs no
tactic at all: one four-letter term will do. -/
theorem ex_effect_apply (y1 y0 : Fin 2 → ℚ) : effect y1 y0 1 = y1 1 - y0 1 :=
  rfl

/-- Exercise (warm-up).  From "unit 0 and unit 1 both benefit" conclude "unit 1
and unit 0 both benefit".  Build the pair with `⟨_, _⟩` and take the given one
apart with `.1` and `.2`. -/
theorem ex_and_comm (y1 y0 : Fin 2 → ℝ) (h : y0 0 ≤ y1 0 ∧ y0 1 ≤ y1 1) :
    y0 1 ≤ y1 1 ∧ y0 0 ≤ y1 0 :=
  sorry

/-- Exercise (warm-up).  From "unit 0 and unit 1 both benefit" conclude "unit 1
and unit 0 both benefit".  Build the pair with `⟨_, _⟩` and take the given one
apart with `.1` and `.2`. -/
theorem ex_and_comm (y1 y0 : Fin 2 → ℝ) (h : y0 0 ≤ y1 0 ∧ y0 1 ≤ y1 1) :
    y0 1 ≤ y1 1 ∧ y0 0 ≤ y1 0 :=
  ⟨h.2, h.1⟩

/-- Exercise (warm-up).  Exhibit a unit whose treatment effect is `2`.  You have
to name the unit: `⟨i, proof⟩`. -/
theorem ex_exists_effect :
    ∃ i : Fin 3, (![1, 5, 2] : Fin 3 → ℚ) i - (![1, 3, 2] : Fin 3 → ℚ) i = 2 :=
  sorry

/-- Exercise (warm-up).  Exhibit a unit whose treatment effect is `2`.  You have
to name the unit: `⟨i, proof⟩`. -/
theorem ex_exists_effect :
    ∃ i : Fin 3, (![1, 5, 2] : Fin 3 → ℚ) i - (![1, 3, 2] : Fin 3 → ℚ) i = 2 :=
  ⟨1, by norm_num⟩

/-- Exercise (core).  A *constant treatment effect* assumption says every unit
has the same effect `c`.  Deduce that unit `0` and unit `1` have equal effects.
Apply the `∀` twice and chain the two equations. -/
theorem ex_constant_effect (y1 y0 : Fin 3 → ℝ) (c : ℝ) (h : ∀ i, y1 i - y0 i = c) :
    y1 0 - y0 0 = y1 1 - y0 1 :=
  sorry

/-- Exercise (core).  A *constant treatment effect* assumption says every unit
has the same effect `c`.  Deduce that unit `0` and unit `1` have equal effects.
Apply the `∀` twice and chain the two equations. -/
theorem ex_constant_effect (y1 y0 : Fin 3 → ℝ) (c : ℝ) (h : ∀ i, y1 i - y0 i = c) :
    y1 0 - y0 0 = y1 1 - y0 1 :=
  (h 0).trans (h 1).symm

/-- Exercise (core).  Under a completely randomised design every unit is either
treated or control, and the observed outcome is the corresponding potential
outcome.  Given that dichotomy, show the observed outcome is nonnegative.
Use `Or.elim`, or the pattern-matching `fun` with `Or.inl h`/`Or.inr h`. -/
theorem ex_obs_nonneg (yobs y1 y0 : ℝ) (h1 : 0 ≤ y1) (h0 : 0 ≤ y0)
    (h : yobs = y1 ∨ yobs = y0) : 0 ≤ yobs :=
  sorry

/-- Exercise (core).  Under a completely randomised design every unit is either
treated or control, and the observed outcome is the corresponding potential
outcome.  Given that dichotomy, show the observed outcome is nonnegative.
Use `Or.elim`, or the pattern-matching `fun` with `Or.inl h`/`Or.inr h`. -/
theorem ex_obs_nonneg (yobs y1 y0 : ℝ) (h1 : 0 ≤ y1) (h0 : 0 ≤ y0)
    (h : yobs = y1 ∨ yobs = y0) : 0 ≤ yobs :=
  Or.elim h (fun e => e ▸ h1) (fun e => e ▸ h0)

/-- Exercise (core).  "The estimator is exactly right" and "the estimator's error
is zero" are the same statement.  Prove the equivalence; `sub_eq_zero` is the
Mathlib lemma, and `Iff.intro` (or `⟨_, _⟩`) assembles the two directions. -/
theorem ex_error_iff (est tau : ℝ) : est = tau ↔ est - tau = 0 :=
  sorry

/-- Exercise (core).  "The estimator is exactly right" and "the estimator's error
is zero" are the same statement.  Prove the equivalence; `sub_eq_zero` is the
Mathlib lemma, and `Iff.intro` (or `⟨_, _⟩`) assembles the two directions. -/
theorem ex_error_iff (est tau : ℝ) : est = tau ↔ est - tau = 0 :=
  Iff.intro (fun h => by rw [h, sub_self]) (fun h => sub_eq_zero.mp h)

/-- Exercise (stretch).  Currying, as a proposition.  A rule that needs two
separate facts is the same as a rule that needs their conjunction.  The proof is
one line and uses only `fun`, `.1` and `.2`. -/
theorem ex_curry (p q r : Prop) : (p → q → r) → (p ∧ q → r) :=
  sorry

/-- Exercise (stretch).  Currying, as a proposition.  A rule that needs two
separate facts is the same as a rule that needs their conjunction.  The proof is
one line and uses only `fun`, `.1` and `.2`. -/
theorem ex_curry (p q r : Prop) : (p → q → r) → (p ∧ q → r) :=
  fun f h => f h.1 h.2

/-- Exercise (stretch).  If a design is unbiased, it is not the case that it is
biased.  Unfold `¬`: the goal `¬ ¬ p` is `(p → False) → False`, so it is
introduced by `fun`, and then there is only one thing to do. -/
theorem ex_not_not (p : Prop) : p → ¬ ¬ p :=
  sorry

/-- Exercise (stretch).  If a design is unbiased, it is not the case that it is
biased.  Unfold `¬`: the goal `¬ ¬ p` is `(p → False) → False`, so it is
introduced by `fun`, and then there is only one thing to do. -/
theorem ex_not_not (p : Prop) : p → ¬ ¬ p :=
  fun hp hnp => hnp hp

Reading autoformalized Lean

Two failures you can already diagnose, with nothing in them but this chapter.

Both failures share a shape, and it is the shape to look for: the statement is true, and the truth has nothing to do with the mathematics you asked about. Lean will not warn you, because there is nothing wrong. The only defense is reading the statement, which is why this chapter came before the one on how to prove things.

Next: the goal state, and the tactics that move it.