mathlib-knowledge

name: mathlib-knowledge description: "Mathlib reference for lean-prover agents. Use AFTER MATH CARD analysis."

Mathlib Reference

This is a REFERENCE, not a decision tree. Use it AFTER your MATH CARD analysis to find the right tactic.

How to Use This Skill

1. Complete MATH CARD analysis first (understand what hypotheses you need to use)
2. Based on your analysis, consult this reference for:
   • Tactic syntax for your approach
   • Lemma names that match your strategy
   • Common patterns for your goal structure

Never pattern-match goal type → tactic blindly. Always reason first.

Tactic Reference

Mathlib Naming Conventions

Learn these patterns - they unlock the library:

Operations

Relations

Transformations

Structures

Critical Lemmas by Domain

Real Analysis (Mathlib.Analysis.SpecialFunctions)

Sine and Cosine:

Real.sin_zero : sin 0 = 0
Real.sin_pi : sin π = 0
Real.cos_zero : cos 0 = 1
Real.cos_pi : cos π = -1
Real.sin_nonneg_of_mem_Icc : x ∈ Icc 0 π → 0 ≤ sin x
Real.sin_pos_of_mem_Ioo : x ∈ Ioo 0 π → 0 < sin x
Real.sin_le_one : sin x ≤ 1
Real.neg_one_le_sin : -1 ≤ sin x

Exponential and Logarithm:

Real.exp_zero : exp 0 = 1
Real.exp_pos : 0 < exp x
Real.exp_lt_exp : exp x < exp y ↔ x < y
Real.log_exp : log (exp x) = x
Real.exp_log (h : 0 < x) : exp (log x) = x
Real.log_mul (hx : 0 < x) (hy : 0 < y) : log (x * y) = log x + log y
Real.log_one : log 1 = 0
Real.log_lt_log (hx : 0 < x) : log x < log y ↔ x < y

Pi:

Real.pi_pos : 0 < π
Real.pi_gt_three : 3 < π
Real.pi_lt_four : π < 4
Real.two_le_pi : 2 ≤ π

Inequalities (Mathlib.Algebra.Order)

The Big Three - Memorize These:

-- AM-GM (Arithmetic-Geometric Mean)
add_div_two_ge_sqrt_mul (ha : 0 ≤ a) (hb : 0 ≤ b) :
  (a + b) / 2 ≥ √(a * b)

-- Cauchy-Schwarz
inner_mul_le_norm_mul_norm : |⟪x, y⟫| ≤ ‖x‖ * ‖y‖

-- Triangle Inequality
norm_add_le : ‖x + y‖ ≤ ‖x‖ + ‖y‖
abs_add : |a + b| ≤ |a| + |b|

Squares and Positivity:

sq_nonneg x : 0 ≤ x^2                    -- ALWAYS use this
sq_abs x : |x|^2 = x^2
sq_le_sq' (h1 : -a ≤ b) (h2 : b ≤ a) : b^2 ≤ a^2
mul_self_nonneg : 0 ≤ a * a
add_pow_le_pow_mul_pow_of_sq_le_sq       -- for (a+b)^n bounds

Monotonicity Helpers:

mul_le_mul_of_nonneg_left (h : b ≤ c) (a0 : 0 ≤ a) : a * b ≤ a * c
mul_le_mul_of_nonneg_right (h : b ≤ c) (a0 : 0 ≤ a) : b * a ≤ c * a
div_le_div_of_nonneg_left (h : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 < c) : a / c ≤ a / b

Convexity (Mathlib.Analysis.Convex)

The Secret Weapon for Transcendental Inequalities:

-- If f is concave on [a,b], then f lies ABOVE the secant line
ConcaveOn.le_right_of_lt_left (hf : ConcaveOn ℝ (Icc a b) f)
  (ha : a < x) (hx : x ≤ b) :
  f x ≥ f a + (f b - f a) / (b - a) * (x - a)

-- If f is convex, then f lies BELOW the secant line
ConvexOn.le_left_of_lt_right (hf : ConvexOn ℝ (Icc a b) f)
  (hx : a ≤ x) (xb : x < b) :
  f x ≤ f a + (f b - f a) / (b - a) * (x - a)

Key Concavity Facts:

strictConcaveOn_sin_Icc : StrictConcaveOn ℝ (Icc 0 π) sin
strictConcaveOn_cos_Icc : StrictConcaveOn ℝ (Icc (-π/2) (π/2)) cos
strictConvexOn_exp : StrictConvexOn ℝ univ exp
strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log

Using Concavity for sin x ≥ linear bounds:

-- sin is concave on [0,π], so sin x ≥ secant line from (0,0) to (π,0)
-- The secant is y = 0, not useful
-- Better: secant from (0,0) to (π/2, 1) gives sin x ≥ (2/π)x on [0,π/2]
-- This is the "Jordan's inequality" technique

Sets and Intervals (Mathlib.Order.Interval)

-- Membership
Set.mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
Set.mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b
Set.mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b

-- Subset relations
Ioo_subset_Icc_self : Ioo a b ⊆ Icc a b
Icc_subset_Icc (h1 : a' ≤ a) (h2 : b ≤ b') : Icc a b ⊆ Icc a' b'

-- Endpoints
left_mem_Icc : a ∈ Icc a b ↔ a ≤ b
right_mem_Icc : b ∈ Icc a b ↔ a ≤ b

Number Theory (Mathlib.NumberTheory)

Nat.prime_def_lt : p.Prime ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1
Nat.Prime.one_lt : p.Prime → 1 < p
Nat.Prime.ne_one : p.Prime → p ≠ 1
Nat.exists_prime_and_dvd (h : 2 ≤ n) : ∃ p, p.Prime ∧ p ∣ n
Nat.factors_prime : p ∈ n.factors → p.Prime

Strategic Patterns

Pattern 1: Prove Inequality via Monotonicity

Goal: f(a) ≤ f(b) where a ≤ b

Strategy:
1. Find/prove: Monotone f (or MonotoneOn f S)
2. Apply: Monotone.le_of_le or MonotoneOn.le_of_le

Pattern 2: Prove Inequality via Convexity

Goal: f(x) ≤ g(x) where g is linear

Strategy:
1. Check: Is f convex? Then f ≤ secant line
2. Check: Is f concave? Then f ≥ secant line
3. Use: ConvexOn.le_right or ConcaveOn.le_right

Pattern 3: Prove Bound via Known Bounds

Goal: a ≤ f(x) ≤ b

Strategy:
1. Find intermediate: a ≤ g(x) ≤ f(x) or f(x) ≤ h(x) ≤ b
2. Chain with: le_trans, lt_of_le_of_lt, lt_of_lt_of_le

Pattern 4: Prove Equality via Squeeze

Goal: f(x) = c

Strategy:
1. Prove: f(x) ≤ c (upper bound)
2. Prove: c ≤ f(x) (lower bound)
3. Apply: le_antisymm

Pattern 5: Prove Positivity

Goal: 0 < f(x)

Strategy:
1. If product: mul_pos h1 h2
2. If sum of positives: add_pos h1 h2
3. If square: sq_pos_of_ne_zero h
4. If exponential: exp_pos x
5. If specific: pi_pos, one_pos, etc.

Pattern 6: Transcendental Inequality

Goal: sin x ≤ polynomial(x) on interval

Strategy:
1. Use concavity: sin is concave on [0,π]
2. Compare to secant line between key points
3. Apply: strictConcaveOn_sin_Icc.concaveOn.le_right
4. Compute: endpoint values to verify secant bound

nlinarith Mastery

nlinarith is your workhorse for nonlinear arithmetic. Feed it the right hints:

-- Basic pattern
nlinarith [sq_nonneg x, sq_nonneg y, h1, h2]

-- Common hints to include:
sq_nonneg x          -- x^2 ≥ 0
sq_nonneg (x - y)    -- (x-y)^2 ≥ 0, expands to x^2 - 2xy + y^2 ≥ 0
mul_self_nonneg x    -- x * x ≥ 0
sq_abs x             -- |x|^2 = x^2
abs_nonneg x         -- 0 ≤ |x|

-- From hypotheses
mul_nonneg h1 h2     -- if h1 : 0 ≤ a, h2 : 0 ≤ b, then 0 ≤ a*b
mul_pos h1 h2        -- if h1 : 0 < a, h2 : 0 < b, then 0 < a*b

Pro tip: If nlinarith fails, try:

1. Adding more sq_nonneg hints
2. Multiplying inequalities: have := mul_nonneg h1 h2
3. Rewriting to simpler form first: ring_nf then nlinarith

Common Proof Skeletons

Proving IsLeast/IsGreatest

example : IsLeast S x := by
  constructor
  · -- Membership: x ∈ S
    simp [S]  -- or exact ⟨_, _⟩
  · -- Minimality: ∀ y ∈ S, x ≤ y
    intro y hy
    obtain ⟨hy1, hy2⟩ := hy
    nlinarith  -- or omega, linarith

Proving ∀ x ∈ Interval

example : ∀ x ∈ Icc a b, P x := by
  intro x hx
  obtain ⟨ha, hb⟩ := hx  -- ha : a ≤ x, hb : x ≤ b
  -- now prove P x using ha, hb

Proving Existential with Specific Witness

example : ∃ x ∈ S, P x := by
  use 42        -- the witness
  constructor
  · norm_num    -- 42 ∈ S
  · ring        -- P 42

Debugging Failed Tactics

Import Checklist

If a lemma isn't found, you may need these imports:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -- sin, cos
import Mathlib.Analysis.SpecialFunctions.Exp -- exp, log
import Mathlib.Analysis.SpecialFunctions.Pow.Real -- rpow
import Mathlib.Analysis.Convex.SpecificFunctions.Basic -- convexity of exp, etc.
import Mathlib.Analysis.MeanInequalities -- AM-GM, etc.
import Mathlib.Order.Bounds.Basic -- IsLeast, IsGreatest
import Mathlib.Topology.Order.Basic -- continuity + order

Quick Reference Card

GOAL                          TACTIC
────────────────────────────────────────
0 < 5                         norm_num
x + y = y + x                 ring
a ≤ b → b ≤ c → a ≤ c        exact le_trans h1 h2
0 ≤ x^2                       exact sq_nonneg x
x ∈ Icc 0 1                   exact ⟨by norm_num, by norm_num⟩
P ∧ Q                         exact ⟨hP, hQ⟩  or  constructor
∃ x, P x                      exact ⟨witness, proof⟩  or  use witness
sin x ≤ 1                     exact Real.sin_le_one x
0 < π                         exact Real.pi_pos
exp 0 = 1                     exact Real.exp_zero
f concave, bound needed       ConcaveOn.le_right ...
x^2 + y^2 ≥ 0                 nlinarith [sq_nonneg x, sq_nonneg y]