13 - Disquality

In addition to definitions, like Odd and Even, Mathlib also contains lemmas and theorems we can use.

We'll see how to use a lemma to support a simple disequality proof.

Task

Given a natural number $n<5$, show that

$$n \neq 5$$

The expression $n \ne 5$ is a disequality, whereas the hypothesis n<5 is an inequality.

Maths

It is common knowledge that, given two natural numbers $a$ and $b$, if $a<b$ is true, then we can say $a\ne b$. 

That common knowledge might seem too trivial to fuss over, but we'll think of it as a small lemma.

If we can show $n<5$, then we can conclude $n \ne 5$, using that lemma.

Let's write a proof that uses this lemma.

$$\begin{align}n&<5&&\text{hypothesis}\tag{1}\label{13.1}\\n&\neq5&&\text{proof objective }\tag{2}\label{13.2}\\&&&\\a<b&\implies a\neq b&&\text{existing lemma}\tag{3}\label{13.3}\\&&&\\n&<5&&\text{sufficient goal, by lemma }(\ref{13.3})\tag{4}\label{13.4}\\&&&\\n&<5&&\text{using }(\ref{13.1})\tag{5}\label{13.5}\\&&&\\n<5&\implies n\neq5&&\text{by lemma }(\ref{13.3})\tag*{\(\Box\)}\end{align}$$

This may look a little over-cooked, but the small steps will help us write a Lean proof. 

We start with the hypothesis $n<5$, and our proof objective $n\ne5$. 

We know about a lemma (3) applicable to natural numbers, that if $a<b$ then $a\ne b$. So if we can prove $n<5$, then we can conclude $n\ne5$. 

This changes our proof goal from $n\ne5$ to $n<5$. 

To prove $n<5$ is easy because we're given it by hypothesis (1]). So $n<5$, and by lemma (3) we finally conclude $n\ne5$.

Code

The following Lean program proves that a natural number $n \ne 5$, given $n < 5$.

-- 13 - Lemma: Not Equal from Less Than

import Mathlib.Tactic

example {n : ℕ} (h: n < 5): n ≠ 5 := by
  apply ne_of_lt
  exact h

The proof header declares n as a natural number, establishes the hypothesis h: n < 5, and specifies the proof objective n ≠ 5.

The apply instruction applies a lemma or theorem to the current goal, usually resulting in a change in goal.

Here, it applies a lemma named ne_of_lt, which means “not equal from less than”. It allows us to prove the current “not equal” goal by instead proving a “less than” goal.

The Infoview will show that apply ne_of_lt does indeed change the current proof goal from n ≠ 5 to n < 5.

The current goal is now n < 5. We could use apply h to resolve the goal, but since the goal matches exactly the hypothesis h, we can instead use the instruction exact h. 

Notice that exact is applying a hypothesis here, not a lemma from Mathlib. The difference is not significant because both hypotheses and lemmas state facts.

We could have used a calc section to prove n < 5 but in this case a multi-line calc section, although familiar, is not warranted.

It may be helpful to correlate this new code back to the maths proof. Here apply ne_of_lt corresponds to line (4) of the maths proof, and exact h corresponds to line (5).

Apply & Exact

We can use apply wherever we use exact. The benefit of exact is that it is stricter than apply. 

The hypothesis or lemma must exactly match the current goal, and if a misunderstanding has led to that not being true, it will be exposed immediately.

Infoview

Placing the cursor before apply ne_of_lt shows the original proof goal.

n : ℕ
h : n < 5
⊢ n ≠ 5

Moving the cursor to the beginning of the next line after apply ne_of_lt shows the goal has indeed changed.

n : ℕ
h : n < 5
⊢ n < 5

Lemmas & Theorems

The distinction between what is called a lemma or a theorem in Mathlib is not precise. Ultimately it doesn't matter as both are used in the same way.

Searching for suitable lemmas and theorems in Mathlib is currently not ideal. Many do conform to a naming convention, which helps. The exercise at the end provides a opportunity to practice finding a lemma using the naming convention.

---

Easy Exercise

Write a Lean program to prove $n\ne5$, given $n>5$, where $n$ is a natural number.

The proof will be almost exactly the same as this chapter's example, except the lemma will be “not equal from greater than”. 

Work out the required lemma's Mathlib name fom the naming convention, or search the online Lean documentation to find it.

12 - Odd & Even

In Part III we'll practise using lemmas and definitions in our proofs. 

There is a huge body of commonly agreed knowledge that mathematicians refer to in their own proofs. A large, and ever-growing, number of these lemmas, theorems, and definitions are encoded in the Mathlib library, ready for us to use in our own Lean proofs. 

We'll start by using the definition of an odd number.

Task

Show the integer 13 is odd.

Maths

To show 13 is odd, we need to show it meets the definition of odd.

An odd integer is of the form $2k+1$, where $k$ is an integer. 

In more mathematical phrasing; if there exists an integer $k$ such that $n=2k+1$, then $n$ is odd.

The task has become an existence proof. If we can find an integer $k$ such that $13=2k+1$, then we have shown 13 is odd.

Let's write out a step by step proof.

$$\begin{align}13&\text{ is odd}&&\text{proof objective }\\&&&\\\exists k\in\mathbb{Z}[n=2k+1]&\implies n\text{ is odd}&&\text{definition of odd}\tag{1}\label{12.1}\\&&&\\\exists k\in\mathbb{Z}[13=2k+1]&&&\text{sufficient goal, using }(\ref{12.1})\\&&&\\\text{use }k=6&&&\text{chosen example}\tag{2}\label{12.2}\\13&=2(6)+1&&\text{using }(\ref{12.2})\\&&&\\13=2(6)+1&\implies13\text{ is odd}&&\text{by definition }(\ref{12.1})\tag*{\(\Box\)}\end{align}$$

This may look a little laborious, but the detail will help us develop a Lean proof. . 

We start with the proof objective, to show $13$ is odd.

We then state the definition, that $n$ is odd if it can be written in the form $2k+1$, where $k$ is an integer. 

So, to show $13$ is odd, it is sufficient to show it can be written in the form $2k+1$. This gives us a new goal, to show there exists an integer $k$ such that $13=2k+1$.

We choose $k=6$, and confirm that $13=2(6)+1$. 

We have shown that $13$ can indeed be written in the form $2k+1$. And so, by the definition of odd, we have finally shown that $13$ is odd.

Code

The following Lean program proves the integer 13 is odd.

-- 12 - Definition: Odd Number

import Mathlib.Tactic

example : Odd (13: ℤ)  := by
  dsimp [Odd]
  use 6
  norm_num

The proof objective states that 13 is Odd. 

If we had simply written Odd 13 as the proof objective, 13 would be interpreted, by default, as a natural number. We write (13: ℤ) to specify 13 as an integer.

The idea of Odd is defined in Mathlib. The next line dsimp [Odd] expands that definition in the Infoview so we can see what it actually is. We'll see below the goal changes from being displayed as Odd 13, to ∃ k, 13 = 2 * k + 1, which we recognise as the definition of odd applied to 13.

The instruction dsimp has no effect on the proof itself. It only changes how Odd is displayed in the Infoview. 

After this point, the proof proceeds as a simple existence proof. 

The instruction use 6 tells Lean we want to try 6 for k. This changes the goal to 13 = 2 * 6 + 1. We resolve this goal by arithmetic, using the norm_num tactic. For such a simple and clear goal, there is no need for a multi-line calc section.

What is Odd?

The proof objective was written as Odd (13: ℤ). The intention is for this to be a statement saying 13 is an odd number.

How does this work?

The idea of Odd is defined in Mathlib as a function. A definition is distinct from a lemma, and Mathlib contains many of both. A lemma needs to be justified by proof, but a definition does not.

That function Odd takes one parameter, and outputs a proposition involving that parameter, which may or may not be true.

When applied to 13, the output is a proposition  ∃k such that 13 = 2*k + 1. This proposition is true because we can prove it.

If we applied Odd to 14, the output is a proposition ∃k such that 14 = 2*k + 1. This proposition is not true because there is no proof for it.

It is interesting to see the actual definition of Odd inside Mathlib:

def Odd (a : α) : Prop := ∃ k, a = 2 * k + 1

We can see how a is mapped to a proposition about a.

Infoview

The Infoview is particularly useful when working with definitions and existence proofs.

Placing the cursor before dsimp [Odd] shows the original proof goal.

⊢ Odd 13

Moving the cursor to the end of the line after dsimp [Odd] shows the goal is now displayed using the definition of Odd.

⊢ ∃ k, 13 = 2 * k + 1

Placing the cursor after use 6 shows the goal is now specific to k = 6.

⊢ ∃ k, 13 = 2 * 6 + 1

---

Easy Exercise

Write a Lean program to prove the integer 14 is even.

Your proof should use Mathlib's definition Even for even numbers. Use dsimp to see how the definition is applied to 14.

11 - Existence

The aim of an existence proof is simply to show something exists. 

Task

Show there exists a natural number n, such that

$$n^{2}+1=10$$

You may see this written in mathematical notation, where the symbol \exists  means “there exists”.

$$\exists n\in\mathbb{N}\;[n^{2}+1=10]$$

The essence of an existence proof is to demonstrate an object exists that satisfies any given conditions. Calculating, deriving, or even guessing, what that object is, is not the central point.

Maths

For our task, intuition tells us that $n$ can't be larger than $10$, and after some mental trial and error we find that $n=3$ works. We have found our example.

We don't need to justify how we arrived at our example. We only need to show it satisfies the condition $n^{2}+1=10$.

Let's write a proof, making clear each step. 

$$\begin{align}\exists n\in\mathbb{N}&[n^{2}+1=10]&&\text{proof objective}\\&&&\\\text{use }n=3&&&\text{chosen example}\tag{1}\label{11.1}\\n^{2}+1&=(3)^{2}+1&&\text{using }(\ref{11.1})\\&=10&&\text{by arithmetic }\tag*{\(\Box\)}\end{align}$$

We first state the proof objective, which includes the condition $n^{2}+1=10$ any example must meet.

We then choose $n=3$, and show by arithmetic that indeed $n^{2}+1=10$. 

Code

The following Lean program proves there exists a natural number $n$ such that $n^{2}+1=10$.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  calc
    3^2 + 1 = 10 := by norm_num

The proof header is a little different from the ones we've looked at recently. Here there is no separate definition of variable types, and no hypothesis. The entire theorem is in the proof objective. 

The proof objective ∃ n: ℕ, n^2 + 1 = 10 says that there exists a natural number n, such that n^2 + 1 = 10.

The next step is to choose an example that meets this condition. The instruction use 3 tells Lean that we propose 3 as that example.

The infoview will confirm that use 3 changes the proof goal from ∃ n, n^2 + 1 = 10 to 3^2 + 1 = 10.

We can use a simple calc section to show by arithmetic that 3^2 + 1 is indeed 10.

Bad Example

Let's see what happens if we choose a bad example, say $n=4$. This means changing the code to use 4.

Placing the cursor after use 4 shows the proof goal.

⊢ 4 ^ 2 + 1 = 10

This goal is impossible to prove, because $17$ is not $10$.

Simpler Code

The following is a shorter version of our Lean program.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  norm_num

The goal at the point of the previous calc section was ⊢ 3^2 + 1 = 10. This is simple enough to apply the norm_num tactic to prove. It doesn't really need a calc section, which is better suited to derivations that require several steps.

As with all programming, it is better to be clear and unambiguous than overly concise. This use of one-line tactics should only be done when the context is simple and clear for anyone reading your code, including your future self.

---

Easy Exercise

Write a Lean program to prove there exists a natural number greater than $5$.

In mathematical notation, the proof objective is as follows, and should translate into Lean code fairly directly.

$$\exists n\in\mathbb{N}\;[n>5]$$

As an optional extra challenge, try writing the proof in the concise form shown above.

10 - "And" Goal

Here we look at an example of a proof goal that is a conjunction.

Task

For integer $x$, given that $x=-1$, show that

$$(x^{2}=1)\land(x^{3}=-1)$$

Maths

Recall that $P\land Q$ being true means at both $P$ and $Q$ must be true. 

That means we have to prove both $x^{2}=1$ and $x^{3}=-1$ are true, given the hypothesis $x=-1$. 

Let's write a step by step proof.

$$\begin{align}x&=-1&&\text{given fact}\tag{1}\label{10.1}\\(x^{2}=1)&\land(x^{3}=-1)&&\text{proof objective }\\&&&\\x^{2}&=(-1)^{2}&&\text{using fact }(\ref{10.1})\\&=1&&\text{using arithmetic }\tag{2}\label{10.2}\\&&&\\x^{3}&=(-1)^{3}&&\text{using fact }(\ref{10.1})\\&=-1&&\text{using arithmetic }\tag{3}\label{10.3}\\&&&\\(x^{2}=1)&\land(x^{3}=-1)&&\text{using results }(\ref{10.2}, \ref{10.3})\tag*{\(\Box\)}\end{align}$$

We have shown both $x^{2}=1$ and $x^{3}=-1$, and so the proof goal $(x^{2}=1)\land(x^{3}=-1)$ is true.

Code

The following Lean program proves $(x^{2}=1) \lor (x^{3}=1)$ follows from $x=-1$.

-- 09 - Disjunctive "or" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∨ x^3 = 1 := by
  left
  calc
    x^2 = (-1)^2 := by rw [h]
    _ = 1 := by norm_num

As is very familiar now, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a conjunction, and uses the symbol ∧ to denote “logical and”. 

The next step is to split the two parts of the conjunctive proof goal into two separate goals, each to be proven one after another. The instruction constructor does precisely this.

The infoview will confirm that constructor replaces the single goal x^2 = 1 ∧ x^3 = 1 with two new goals, x^2 = 1 and x^3 = -1.

The rest of the proof has two calc structures, one after the other, to show x^2 = 1 and x^3 = -1. Focussing dots are used to make clear there are two sub-proofs to support the overall proof.

Infoview

Placing the cursor before the constructor instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∧ x ^ 3 = -1

Placing the cursor on the next line after constructor confirms the proof goal has been replaced by two smaller goals.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

x : ℤ
h : x = -1
⊢ x ^ 3 = -1

This is another example of manipulating the proof goal into a form that is easier to prove.

---

Easy Exercise

A longer conjunction could be $P\land Q\land R\land S$. The instruction constructor splits this into two goals, $P$ and $Q\land R\land S$.

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x^{3}=-1)\land(x^{4}=1)\land(x^{5}=-1)$$

The proof will require two uses of constructor.

09 - "Or" Goal

We've seen that a hypothesis can be a disjunction or a conjunction. 

Here we look at a slightly more interesting scenario, a proof goal that is a disjunction.

Task

For integer $x$, given that $x=-1$, show that 

$$(x^{2}=1)\lor(x^{3}=1)$$

Maths

Our initial reaction might be concern at seeing $x^{3}=1$. Clearly $(-1)^{3}=1$ is not true. 

Remember that $P\lor Q$ being true means at least one of $P$ and $Q$ is true. If $Q$ is false, but $P$ is true, then the disjunction $P\lor Q$ is still true.

Given the hypothesis $x=-1$, if we can prove $x^{2}=1$ is true, then we have proven the disjunction $(x^{2}=1)\lor(x^{3}=1)$ is also true.

Let's write a step by step proof.

$$\begin{align}x&=-1&&\text{given fact}\tag{1}\label{9.1}\\(x^{2}=1)&\lor(x^{3}=1)&&\text{proof objective }\tag{2}\label{9.2}\\&&&\\x^{2}&=1&&\text{sufficient goal }(\ref{9.2})\tag{3}\label{9.3}\\&&&\\x^{2}&=(-1)^{2}&&\text{using fact }(\ref{9.1})\\&=1&&\text{using arithmetic }\\&&&\\(x=-1)&\implies(x^{2}=1)\lor(x^{3}=1)&&\text{}\tag*{\(\Box\)}\end{align}$$

Once we state that it is sufficient to prove $(x^{2}=1)$ in order to prove $(x^{2}=1)\lor(x^{3}=1)$, the rest of the proof continues in the familiar way we've seen before.

Choice

If the proof objective were $(x^{2}=1) \lor (x^{3}=-1)$, then both statements $x^{2}=1$ and $x^{3}=-1$ can be proven to be true. 

We can choose which one of the two statements we want to prove. We don't need to prove both, because proving one is sufficient for a disjunction.

Code

The following Lean program proves $(x^{2}=1) \lor (x^{3}=1)$ follows from $x=-1$.

-- 09 - Disjunctive "or" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∨ x^3 = 1 := by
  left
  calc
    x^2 = (-1)^2 := by rw [h]
    _ = 1 := by norm_num

As usual, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a disjunction, and uses the symbol $\lor$  to denote “logical or”. 

We state our intention to prove only the “left” part of the disjunction. The instruction left does precisely this. 

The infoview will confirm that left replaces the goal x^2 = 1 ∨ x^3 = 1 with x^2 = 1.

The rest of the proof uses the familiar calc structure to show x^2 = 1. This matches the new proof goal, and because it is sufficient, the original goal x^2 = 1 ∨ x^3 = 1 is proven.

Infoview

Placing the cursor before the left instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∨ x ^ 3 = 1

Placing the cursor on the next line after left confirms the proof goal has been replaced by a smaller, but sufficient, statement.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

This manipulation of the proof goal might appear to be a hack, something to be discouraged. In fact, it is quite common, and considered quite normal.

---

Easy Exercise

A longer disjunction could be $P\lor Q\lor R\lor S$. The instruction left selects the left-most statement $P$ as the new goal. The instruction right selects the remainder $Q\lor R\lor S$ as the new goal. 

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x=1)\lor(x^{2}=1)\lor(x^{3}=1)$$

Both the right and left instructions will be needed to write the proof.

08 - "And' Hypothesis

The previous task started with an “or” hypothesis. Here we'll look start with anl “and” hypothesis. 

Task

For integers $x$ and $y$, where the following is true

$$(x=5)\land(y=x+3)$$

show that

$$y=8$$

The symbol $\land$  means “logical and”. The statement $P\land Q$ means both $P$ and $Q$ are true. Statements of the form $P\land Q$ are called conjunctions.

Maths

Once we realise a hypothesis of the form $P\land Q$ is the same as hypotheses $P$ and $Q$ both being true, the proof proceeds just like our earlier examples with two hypotheses.

In this sense, conjunctive hypotheses are not particularly interesting, but we do need to learn how to handle them.

Let's write a proof, making clear each step.

$$\begin{align} (x=5)&\land(y=x+3)&&\text{given fact}\tag{1}\label{8.1}\\&&&\\x&=5&&\text{derived fact }(\ref{8.1})\tag{2}\label{8.2}\\y&=x+3&&\text{derived fact }(\ref{8.1})\tag{3}\label{8.3}\\&&&\\y&=x+3&&\text{using fact }(\ref{8.3})\\&=(5)+3&&\text{using fact }(\ref{8.2})\\&=8&&\text{using arithmetic}\tag*{\(\Box\)} \end{align}$$

From the single conjunctive hypothesis $(x=5)\land(y=x+3)$ we derive two smaller hypotheses, $x=5$ and $y=x+3$, both of which are true.

We start with $y=x+3$ from derived fact (3), and then use $x=5$ from derived fact (2) to finally conclude $y=8$.

Code

The following Lean program proves $y=8$ follows from $(x=5)\land(y=x+3)$.

-- 08 - Conjunctive "and" Hypothesis

import Mathlib.Tactic

example {x y : ℤ} (h : x = 5 ∧ y = x + 3) : y = 8 := by
  obtain ⟨ ha , hb ⟩ := h
  calc
    y = x + 3 := by rw [hb]
    _ = (5) + 3 := by rw [ha]
    _ = 8 := by norm_num

As usual, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof goal. The hypothesis is a conjunction, and uses the symbol ∧ to denote “logical and”. 

The next step is to replace the conjunctive hypothesis with two smaller hypotheses. The instruction obtain ⟨ ha, hb ⟩ := h does this. It splits the conjunctive hypothesis h into ha and hb, and then removes h.

Notice the comma and angle brackets ⟨⟩ used to split a conjunction, unlike the vertical bar | and no brackets used to split a disjunction.

The rest of the proof uses the familiar calc structure to show y = 8. 

Infoview

Placing the cursor before the obtain instruction shows there is only one hypothesis g.

x y : ℤ
h : x = 5 ∧ y = x + 3
⊢ y = 8

Placing the cursor on the next line after obtain, confirms h has been replaced by ha and hb.

x y : ℤ
ha : x = 5
hb : y = x + 3
⊢ y = 8

Notice the hypothesis h has been entirely removed.

---

Easy Exercise

Write a Lean program to show that $y\ge 8$, given the conjunctive hypothesis

$$(x \ge 5) \land (y=x+3)$$

where $x$ and $y$ are integers.

07 - Proof By Cases

A proof by cases divides a task into separate cases, and proves each one leads to the desired conclusion. 

Task

Given the following fact about the real number $x$,

$$(x=3)\lor(x=-3)$$

our task is to show

$$x^{2}=9$$

The symbol $\lor$  means “logical or”. The statement $P \lor Q$ means either $P$ is true, or $Q$ is true, or possibly even both are true. 

Statements of the form $P \lor Q$ are called disjunctions.

Maths

Our aim is to show $x^{2}=9$ follows from the hypothesis $(x=3) \lor (x=-3)$. 

This hypothesis tells us that either $x=3$ is true, or $x=-3$ is true. We don't know which, so we have to consider both cases, and show the conclusion follows from each case.

The following illustrates this.

Let's write a proof by cases, making clear each step.

$$\begin{align}(x=3)&\lor(x=-3)&&\text{given fact}\tag{1}\label{7.1}\\&&&\\\text{case }x=3&&&\text{using fact }(\ref{7.1})\tag{2}\label{7.2}\\x^{2}&=(3)^{2}&&\text{using case }(\ref{7.2})\\&=9&&\\&&&\\\text{case }x=-3&&&\text{using fact }(\ref{7.1})\tag{3}\label{7.3}\\x^{2}&=(-3)^{2}&&\text{using case }(\ref{7.3})\\&=9&&\\&&&\text{}\\(x=3)\lor(x=-3)&\implies x^{2}=9&&\text{}\tag*{\(\Box\)}\end{align}$$

The given fact (1) splits into two cases, $x=3$ and $x=-3$. 

• The first case (2) is $x=3$. We want to prove something about $x^{2}$. This case gives us $x^{2}=(3)^{2}$, leading to the conclusion $x^{2}=9$.
• The second case (3) is $x=-3$. This gives us $x^{2}=(-3)^{2}$, also leading to the conclusion $x^{2}=9$.

The two cases $x=3$ and $x=-3$ are sufficient to fully cover the hypothesis $(x=3)\lor(x=-3)$. There is no third option. So we have shown that, given the hypothesis, $x^{2}$ is indeed always $9$.

Code

The following Lean program proves $x^{2}=9$ follows from $(x=3)\lor(x=-3)$.

-- 07 - Proof by Cases

import Mathlib.Tactic

example {x : ℤ} (h : x = 3 v x = -3) : x^2 = 9 := by
  obtain ha | hb := h
  · calc
    x^2 = (3)^2 := by rw [ha]
    _ = 9 := by norm_num
  · calc
    x^2 = (-3)^2 := by rw [hb]
    _ = 9 := by norm_num

The proof header is no different to the ones we've seen before, setting out the variable type, the hypothesis, and the proof objective. The hypothesis is a disjunction, and uses the letter v, to denote “logical or”. 

The next line is new. The obtain ha | hb := h splits the disjunction hypothesis h into ha and hb. These new hypotheses correspond to the two cases.

The Infoview will show that ha : x = 3 and hb : x = -3. 

We now need to show that each case, with ha and hb as hypotheses, leads to the desired conclusion . The two calc sections, one after the other, do exactly this.

In the first calc section, we start with x^2 because that is what we want to prove something about. We use the newly created hyopthesis ha : x = 3 to justify x^2 = (3)^2, and then show this is 9 by simple arithmetic.

The second calc section is almost exactly the same, but uses the hypothesis for second case hb : x = -3.

Notice the calc sections have a dot preceding them, · calc. This focussing dot is considered good style when writing sub-proofs within a larger proof. They help us visually see, at a glance, the structure of the proof, and the Infoview restricts information to the current goal. You can enter the focussing dot by typing \. and your Lean editor should turn it into a focussing dot.

Infoview

Placing the cursor before obtain shows only one goal, the overall proof goal.

1 goal
x : ℤ
h : x = 3 v x = -3
⊢ x ^ 2 = 9

Moving the cursor after the obtain instruction, just before the first · calc, shows the two sub-goals and their respective hypotheses ha and hb.

2 goals
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9

case inr
x : ℤ
hb : x = -3
⊢ x ^ 2 = 9

Moving the cursor past the focussing dot, placing it just before calc, shows only the sub-goal and hypothesis relevant to the first case.

1 goal
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9

---

Easy Exercise

Write a Lean program to prove $x^{2}-3x+2=0$, given

$$(x=1)\lor(x=2)$$

where $x \in \mathbb{R}$. 

In your proof create two cases $x=1$ and $x=2$ from the given hypothesis $(x=1) \lor (x=2)$.