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.
