Lean4
LanguageTactics
Module 5 · Lesson 1

Introduction to Mathlib

Mathlib is the mathematical library for Lean 4. It provides a vast collection of definitions, theorems, and powerful tactics that extend Lean's capabilities.

❗
The tactics in this module require Mathlib4. They are not part of core Lean 4 and must be imported from the Mathlib library.

What is Mathlib?

Mathlib is a community-driven mathematical library containing:

  • Over a million lines of formalized mathematics
  • Algebra, analysis, topology, number theory, and more
  • Powerful automation tactics for common proof patterns
  • Type class hierarchies for abstract mathematics

Setting Up Mathlib

lean
1-- In your lakefile.lean, add Mathlib as a dependency:
2require mathlib from git
3  "https://github.com/leanprover-community/mathlib4"
4
5-- Then in your Lean files:
6import Mathlib.Tactic  -- Import all tactics
7
8-- Or import specific modules:
9import Mathlib.Tactic.Ring
10import Mathlib.Tactic.Linarith
11import Mathlib.Tactic.FieldSimp
Key Takeaway
Mathlib tactics must be imported before use. The importMathlib.Tactic brings in all common tactics.

Core Lean 4 vs Mathlib Tactics

lean
1-- Core Lean 4 tactics (always available):
2-- rfl, rw, simp, exact, apply, intro, cases, induction
3-- constructor, have, let, omega, decide, native_decide
4
5-- Mathlib tactics (require import):
6-- ring, field_simp, linarith, nlinarith, polyrith
7-- rcases, obtain, push_neg, contrapose, ext, congr
8-- norm_num, positivity, gcongr, and many more

Why Use Mathlib Tactics?

1. Domain-Specific Automation

lean
1import Mathlib.Tactic.Ring
2
3-- ring solves polynomial equations automatically
4example (x y : Int) : (x + y)^2 = x^2 + 2*x*y + y^2 := by ring
5
6-- Without ring, this requires many rewrites!

2. Proof Search

lean
1import Mathlib.Tactic.Linarith
2
3-- linarith finds linear arithmetic contradictions
4example (x y : Int) (h1 : x < y) (h2 : y < x) : False := by linarith
5
6-- It searches through hypotheses automatically

3. Structural Tactics

lean
1import Mathlib.Tactic.Cases
2
3-- rcases provides powerful pattern matching
4example (h : ∃ n : Nat, n > 0 ∧ n < 10) : True := by
5  rcases h with ⟨n, hn_pos, hn_lt⟩
6  trivial
Deep Dive: Mathlib's Philosophy

Mathlib follows several design principles:

  • Generality: Define concepts at their most general level
  • Bundling: Group related structures together
  • Automation: Provide tactics that handle routine proofs
  • Consistency: Follow naming conventions strictly

Mathlib Tactics in This Module

We'll cover the most commonly used Mathlib tactics:

Arithmetic Tactics

  • ring — Solve polynomial ring equations
  • field_simp — Simplify field expressions with division
  • linarith — Linear arithmetic reasoning
  • nlinarith — Nonlinear arithmetic
  • polyrith — Polynomial arithmetic search

Structural Tactics

  • rcases / obtain — Pattern matching
  • push_neg — Push negations inward
  • contrapose — Contrapositive reasoning
  • ext — Extensionality
  • congr — Congruence

Getting Started

lean
1-- Quick setup with all Mathlib tactics:
2import Mathlib.Tactic
3
4-- Now you can use ring, linarith, and more!
5example (a b : ℤ) : (a - b) * (a + b) = a^2 - b^2 := by ring
💡
Start with import Mathlib.Tactic to get all tactics. Later, you can import only what you need for faster compilation.
Exercise: Import and Use ring

Import Mathlib tactics and use ring on a simple identity.

lean
1import Mathlib.Tactic
2
3example (x : Int) : (x + 1)^2 = x^2 + 2*x + 1 := by
4  ring
Custom TacticsNext: ring