Formalising Mathematics
Contents:
Introduction
Getting Lean running on your computer
Part A: the mathematics
Part B: Lean tips
Part C: Tactics
Tactic cheatsheet
Tactic documentation
apply
assumption
by_cases
by_contra
cases
change
exact
exfalso
ext
have
intro
intros
left
linarith
nlinarith
norm_num
nth_rewrite
obtain
rcases
refine
refl
right
ring
rintro
rw
simp
simpa
specialize
split
triv
use
Formalising Mathematics
»
Part C: Tactics
»
Tactic documentation
View page source
Tactic documentation
Contents:
apply
Summary
Examples
Further notes
assumption
Summary
Examples
Further notes
by_cases
Summary
Examples
Details
Further notes
by_contra
Summary
Example
Further notes
cases
Summary
Examples
Further notes
change
Summary
Example
Details
Further notes
exact
Summary
Examples
Further notes
exfalso
Summary
Examples
Details
ext
Summary
Examples
Details
Further notes
have
Summary
Examples
Further notes
intro
Summary
Examples
Details
intros
Summary
Examples
Further notes
left
Summary
Details
Further notes
linarith
Summary
Examples
nlinarith
Summary
norm_num
Summary
Examples
nth_rewrite
Summary
Examples
Further notes
obtain
Summary
Example
Details
rcases
Summary
Examples
Details
refine
Summary
Examples
Further notes
refl
Summary
Examples
Further notes
right
Summary
Details
Further notes
ring
Summary
Examples
Further notes
rintro
Summary
Examples
Details
Further notes
rw
Summary
Examples
Further notes
simp
Summary
Overview
Examples
Details
Further notes
simpa
Summary
Examples
Further notes
specialize
Summary
Examples
Further notes
split
Summary
Examples
Further notes
triv
Summary
Examples
Details
Further notes
use
Summary
Examples
Further notes