Here we look at 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$.
-- 10 - Conjunctive "and" Goal
import Mathlib.Tactic
example {x : ℤ} (h : x = -1) : x^2 = 1 ∧ x^3 = -1 := by
constructor
· calc
x^2 = (-1)^2 := by rw [h]
_ = 1 := by norm_num
· calc
x^3 = (-1)^3 := 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
