Lean4
LanguageTacticsCourse
Module 5 · Lesson 3

field_simp

Simplify expressions involving division by clearing denominators.field_simp transforms field equations into polynomial equations that ring can solve.

❗
field_simp requires Mathlib. Add import Mathlib.Tactic.FieldSimp to use this tactic.

Basic Usage

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- field_simp clears denominators
5example (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) : 
6    1/a + 1/b = (a + b)/(a * b) := by
7  field_simp
8  ring
9
10-- It handles complex fractions
11example (x : ℚ) (hx : x ≠ 0) : (1 + 1/x) * x = x + 1 := by
12  field_simp
13  ring
Key Takeaway
field_simp multiplies through by denominators to eliminate division, then you typically use ringto finish the proof.

Handling Division

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- x/x = 1 when x ≠ 0
5example (x : ℚ) (hx : x ≠ 0) : x / x = 1 := by
6  field_simp
7
8-- Nested fractions
9example (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) :
10    (a/b) / (b/a) = a^2 / b^2 := by
11  field_simp
12  ring
13
14-- Adding fractions
15example (x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) :
16    1/x - 1/y = (y - x) / (x * y) := by
17  field_simp
18  ring

Non-Zero Conditions

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- field_simp uses hypotheses that terms are non-zero
5example (a : ℚ) (ha : a ≠ 0) : a * (1/a) = 1 := by
6  field_simp  -- Uses ha to know a ≠ 0
7
8-- Without the hypothesis, it can't simplify fully
9-- example (a : ℚ) : a * (1/a) = 1 := by field_simp  -- Leaves goal
10
11-- You can provide side conditions
12example (a b : ℚ) (h : a * b ≠ 0) : 1/(a*b) = 1/a * (1/b) := by
13  field_simp
14  ring
ℹ
field_simp automatically uses hypotheses of the form x ≠ 0 to justify clearing denominators.

The field_simp + ring Pattern

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- This combination solves most field equations
5example (x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) :
6    (x^2 - y^2) / (x + y) = x - y := by
7  field_simp
8  ring
9
10-- Complex algebraic identity
11example (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a - b ≠ 0) :
12    1/(a - b) * (1/b - 1/a) = 1/(a*b) := by
13  field_simp
14  ring
Deep Dive: How field_simp Works

field_simp performs these transformations:

  1. Finds all division operations in the goal
  2. Computes the least common denominator
  3. Multiplies both sides by this denominator
  4. Simplifies using field axioms (assuming denominators ≠ 0)
  5. May generate side goals for non-zero conditions

Side Goals

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- Sometimes field_simp generates side goals
5example (x : ℚ) : (x^2 + 1) / (x^2 + 1) = 1 := by
6  field_simp
7  -- May need to prove x^2 + 1 ≠ 0
8  -- In ℚ, x^2 + 1 > 0 for all x
9
10-- Using positivity to handle side goals
11-- example (x : ℚ) : (x^2 + 1) / (x^2 + 1) = 1 := by
12--   field_simp
13--   positivity  -- From Mathlib.Tactic.Positivity

Real-World Examples

Harmonic Series Manipulation

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- Telescoping fractions
5theorem telescope (n : ℚ) (hn : n ≠ 0) (hn1 : n + 1 ≠ 0) :
6    1/n - 1/(n+1) = 1/(n*(n+1)) := by
7  field_simp
8  ring

Physics Formula

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- Lens equation: 1/f = 1/u + 1/v
5-- Prove: f = uv/(u+v)
6theorem lens_equation (u v f : ℚ) 
7    (hu : u ≠ 0) (hv : v ≠ 0) (huv : u + v ≠ 0)
8    (h : 1/f = 1/u + 1/v) : f = (u*v)/(u+v) := by
9  have hf : f ≠ 0 := by
10    intro hf
11    simp [hf] at h
12    field_simp at h
13    linarith
14  field_simp at h ⊢
15  linarith

Common Patterns

lean
1import Mathlib.Tactic.FieldSimp
2import Mathlib.Tactic.Ring
3
4-- Reciprocal of reciprocal
5example (x : ℚ) (hx : x ≠ 0) : 1 / (1/x) = x := by
6  field_simp
7
8-- Sum to product
9example (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) :
10    (a + b) / (a * b) = 1/a + 1/b := by
11  field_simp
12  ring
13
14-- Difference quotient
15example (x h : ℚ) (hh : h ≠ 0) :
16    ((x + h)^2 - x^2) / h = 2*x + h := by
17  field_simp
18  ring
ringNext: linarith