Lean phrasebook

	A	B	C	D	E
1	Goal	(Selected) hypotheses	Step (in mathematical english)	Lean equivalent	Notes

2			Observe that A holds because of reason r	have h:A := by r	Can omit h, in which case the result is called `this` by default If the reason r is a one-liner, "observe h:A" can work
3			Observe that X is equal to Y by definition	have : X = Y := by rfl	or "observe : X = Y"
4			We claim that A holds. ...	have h:A := by <proof of A>
5	A	h: A	The claim follows	assumption	Can also use `exact h`
6			This follows by definition	rfl
7			This follows by reason r	exact r	Can try exact? to find if an exact solution already exists
8			By A, it suffices to show that ...	apply A
9		h: A	Using h, we may reduce to	simp [h]	can combine multiple simplfiications using simp [h1, h2, ...] can use `simp only [hypotheses]` for a more targeted simplification can try simp? to suggest tools to use
10		h: A	We can rewrite our goal using A as ...	rw [h]	also have `nth_rewrite n [h]` for more precise rewriting can combine multiple rewrites using rw [h,h',...] If one wants to apply h in reverse, use rw [<- h] A rewrite that turns a goal into an existing assumption can close the proof using rwa [h] If one needs to use associativity before rewriting, use assoc_rw
11			We can rewrite our goal using A (which is true for reason r) as ...	rw [(show A by r)]	Can also use (by r: A) instead of (show A by r)
12		A	Applying reason r to A, we conclude B	have h:B := r A
13	A ∧ B		First we prove A. ... Now we prove B. ...	constructor . <proof of A> <proof of B>
14	A ∧ B ∧ C ∧ D		We now prove each of A, B, C, D in turn.	refine ⟨ ?_, ?_, ?_, ?_ ⟩
15		h: A ∧ B	By hypothesis, we have A and B	rcases h with \langle hA, hB \rangle	can also use h.1 and h.2 an intro followed by rcases can be merged into an rintro. A rcases item that is used immediately for rw can be replaced with an rfl
16		h: A ∧ B ∧ C ∧ D	By hypothesis, we have A, B, C, D	obtain ⟨ hA, hB, hC, hD ⟩ := h
17			From h, we obtain A and B		Also works for more complex expressions than simple conjunctions
18	A \iff B		First we prove A implies B. ... Now we prove B implies A	constructor . <proof of A implies B> <proof of B implies A>
19			We will obtain a contradiction	exfalso
20	A \Or B		It will suffice to prove A	left	can also use Or.inl
21	A \Or B		It will suffice to prove B	right	can also use Or.inr
22		h: A \Or B	We divide into cases. First, suppose that A holds. ... Now, suppose that B holds ...	rcases h with ha \| hb
23			We divide into cases depending on the natural number n First, suppose that n=0. ... Now, suppose that n=m+1 for some m ...	rcases n with _ \| m	Also works for other inductive types than the natural numbers, e.g., finite sets
24			We divide into cases. First, suppose that A is true. ... Now, suppose that A is false ...	by_cases h:A . <proof assuming A> <proof assuming not-A>	can also use rcases em A with ha \| hna . <proof assuming A> <proof assuming not-A>
25			We divide into cases. First, suppose that n=0. ... Next, suppose that n=1. ... Finally, suppose that n is of the form n+2...	match n with \| 0 => ... \| 1 => ... \| n+2 => ...
26		h: A, nh: not-A	But this is absurd.	absurd h nh	One can save a line or two sometimes by deriving A or not-A directly, e.g., using the `(show A by r)` syntax
27		A, not-A	This gives the required contradiction.	contradiction
28	A		Suppose for contradiction that A fails	by_contra nh
29	not-A		Suppose for contradiction that A holds	intro ha
30	A	h: B	Taking contrapositives, it suffices to show that not-A implies not-B.	contrapose! h
31			We compute x = y (by reason r) = z (by reason s) = w (by reason t)	calc x = y := by r _ = z := by s _ = w := by t	Calc can also handle chained inequalities like \leq and <. gcongr is a useful tactic to justify intermediate steps in such cases
32	A implies B		Thus, suppose that A holds.	intro ha	For complex hypotheses it can be convenient to use rintro instead Can omit ha, in which case the hypothesis of A is placed in `this`
33	\forall x \in X, A		Now let x be an element of X.	intro x, hx
34		ha: a \in X h: \forall x \in X: A(x)	Since a is in X, A(a) holds	have haa := h a ha	If one wants to use A(a) directly one can just use `h a ha` anywhere one would have otherwise used haa Can also use `specialize h a ha`, but this replaces h with `h a ha`.
35	\exists x, A		We will take x to equal a	use a
36		h: \exists x A	By hypothesis, there exists x obeying A	rcases h with \langle x, hxa \rangle
37	A		We need to show A'	show A'	If there are multiple goals, show finds the goal that matches A' and moves it to the front of the goal queue
38		A	By definition, we may rewrite the hypothesis A as A'	change A' at A	can siimilarly use "change X" to change the goal to a definitionally equivalent X
39		h:A f: A \implies B	By f, we may replace A by B	replace h := f h
40		h: A	We may replace A with B by reason r	replace h : B := by r
41		h: A	The hypothesis A is no longer needed and can be discarded.	clear h
42		ha: A hb: B	The only hypotheses we will use in the sequel are A and B	clear_except hA hB
43			We simplify this as	simp	If one simplifies to one of the assumptions, we can use `simpa` instead of `simp` and `assumption`
44		h : A	We can simplify the hypothesis A as	simp at h	Can be combined with [hypotheses], `simp only`, etc. Can also use wildcard *
45			By definition, this can be rewritten as	dsimp	Is a more restrictive version of simp, only uses definitional equalities.
46			But this follows from the laws of algebra in a ring	ring
47			Since we are in a field, we can simplify this to	field_simp [hypotheses]	field_simp is good for clearing denominators; often followed by ring. Hypotheses of denominators being non-zero are located automatically, or introduced as additional goals
48		h : A	Since we are in a field, we can simplify A to	field_simp [hypotheses] at h
49			But this follows from the laws of linear inequalities	linarith
50			But this follows (by logical tautology)	tauto
51			Which can be numerically verified	norm_num
52			negating all the quantifiers, we reduce to showing	push_neg
53			One is now tempted to try...	apply?
54			To conclude, one could try	exact?
55	f=g		It suffices to show that f(x)=g(x) for every x	ext x
56	S = T		It suffices to show that x \in S iff x \in T	ext x
57	sum_{x in X} f(x) = sum_{x in X} g(x)		It suffices to show that for all x in X, that f(x) = g(x)	Finset.sum_congr rfl	If g is ranging over another set Y, can replace rfl here with a proof that X=Y
58	f(x)=f(y)		It will suffice to show that x=y	congr	sometimes congr! works better. Sometimes congr breaks things down too much, and one has to use congr 1, congr 2, etc. instead or the more precise congrm
59	x+y \leq x'+y'		It suffices to show that x \leq x' and y \leq y'	gcongr	Works well with calc. If sums or products are involved, may need to use "gcongr with i hi" etc. in order to access the bound variables
60	X \subset Y		Let x \in X. We need to show that x \in Y	intro x hx
61	x in X \cup Y		x is in X or x is in Y	rintro xX \| xY
62	x in X \cap Y		x is in X and x is in Y	rintro \langle xX, xY \rangle
63	X = Y		It suffices to show X \subset Y and Y \subset X	apply Subset.antisymm
64	x = y		It suffices to show x \leq y and y \leq x	apply le_antisymm
65			We induct on n. First we establish the base case n=0. ... Now suppose inductively that the claim holds for n. ..	induction' n with n ih . <proof of base case> <proof of inductive case>
66	X=Y		We rewrite our goal as Y=X	symm
67	A		We claim it suffices to show B. ... Now we show B. ...	suffices B by <proof of A given B> <proof of B>	If B is very close in form to A, convert can work (and if B is definitionally equal to A, change can work)
68			We replace X by Y, which is possible thanks to r	rw [(show X=Y by r)]
69		h: X = Y	Applying f to both sides, we conclude f(X)=f(Y)	apply_fun f at h	Can also use `replace h := congr_arg f h` or `replace h := by congrm (f $h)`. Similarly can use congrm (1 + $h) to add 1 to both sides, etc. gcongr can be used in situations where one is proving inequalities rather than equalities.
70	something involving (if A then x else y)		First suppose that A is true. Now suppose that A is false.	split . <proof if A is true> <proof if A is false>
71			Expanding out all the definitions, our goal is to establish	unfold	Can also "unfold at h" to expand out h. Can use dunfold if one only wants to expand using definitional equalities
72	x>0 or x >= 0		This positivity is clear from the hypotheses	positivity
73	f(x:\N) = f(x:\R)		This expression is the same whether we think of x as a natural number or a real	norm_cast
74	c + b + a = b + a + d		We move all the a terms to the left, and the b terms to the right	move_add [<- a b]	move_mul is similar, but for products
75			Let X denote the quantity Y	let X := Y
76			We will abbreviate the expression Y as X	set X := Y	The difference between this and let is that it actively seeks out all occurrences of Y and replaces them with X Can use set X := Y with h if one wants to use h : X = Y as a hypothesis Can also use generalize : Y = X (or generalize h : Y = X) to make X a new variable rather than definitionally equal to Y
77			We prove the latter goal first	swap	Also `swap n`, `rotate`, and `rotate n` for similar goal permuting maneuvers
78			We claim A. (proof of A). We now continue with the rest of the proof.	have h:A
79			Later we will prove A. Assuming this claim for the moment .... . Now, we prove A.	suffices h : A from <proof assuming h> <proof of A>	can also use `have h : A; swap`
80			Suppose P is true. (some arguments) we now conclude Q is true. In summary, P implies Q.	have hPQ (hP: P) : ?Q := by -- (some arguments reaching a conclusion hQ:Q) exact hQ
81			We now perform the following arguments. (some arguments). In summary, we have established P.	have hP: ?P := by -- (some arguments reaching a conclusion hP:P) exact hP
82			Let n be a natural number. (some arguments) We now conclude that P(n) is true. In summary, P(n) is true for all natural numbers .	have hP (n : \Nat) : ?P := by -- (some arguments reaching a conclusion hP: P n) exact hP
83			Without loss of generality we may assume P.	wlog h : P . <proof assuming not-P, and that the goal was provable assuming P> <proof assuming P>	See also "wlog h : P generalizing ..." to generalize selected variables
84	X \leq Y	h: X' \leq Y'	It suffices to show that X=X' and Y=Y'	convert h using 1	Works for many more general relations than \leq here; can also work with other depths of conversion than 1
85	X \leq Y	h: X \leq Z	It suffices to show that Z \leq Y	apply h.trans	can also use `apply le_trans h _`
86	X<Y	h: X \leq Z	It suffices to show that Z < Y	apply h.trans_lt
87	X \leq Y	h: Z \leq Y	It suffices to show that X \leq Y	apply le_trans _ h
88	X \leq Y	h: X = Z	It suffices to show that Z \leq Y	rw [h]
89	X \leq Y	h: Z = Y	It suffices to show that X \leq Z	rw [<- h]
90	X \leq Y	h: X' \leq Y'	It suffices to show that X \leq X' and Y' \leq Y	apply le_trans _ (le_trans h _)
91	X \leq Y		Suppose for contradiction that Y < X	by_contra h; simp at h
92	X \leq Y		It suffices to show that f(X) \leq f(Y) (because f is an order isomorphism)	apply_fun f	See https://leanprover-community.github.io/mathlib_docs/tactics.html#apply_fun for several variants of this
93	X \leq Y		It suffices to show that X + Z \leq Y + Z	rw [<- add_le_add_right]	many variants, e.g., add_le_add_left, sub_le_sub_right , etc.
94	X \leq Y		It suffices to show that X Z \leq Y Z (and that Z>0)	apply mul_le_mul_right
95	A B C		We establish all these goals by the same argument:	all_goals { <list of tactics> }	Can enclose <list of tactics> inside (try ...) in case some of the goals cannot be accomplished this way The braces {} can be dropped if there is only one tactic, and you do not expect to always close the argument
96			We conjecture that A holds	theorem A_conj : A := by sorry	Can use `have` instead of `theorem` inside a proof environment
97			We may rewrite our goal using the identity (x+y)(x-y)=x^2-y^2 as	rw [show ∀ x :ℝ, ∀ y : ℝ, (x+y)(x-y) = xx-y*y by intros; ring]
98	∀ᶠ x in f, Q x	h: ∀ᶠ x in f, P x h': ∀ᶠ x in f, P' x	It suffices to show Q x for x obeying P x and P' x	filter_upwards [h, h']
99		h: Nonempty A	We arbitrarily select an element x from the nonempty set A	obtain ⟨ x ⟩ := h
100		h: Nonempty A	We use a canonical choice function to select an element x from the nonempty set A	x = h.some	Can also use x = h.arbitrary or x = Classical.choice h