11# Tactics
22
3- Mathlib version: ` 3aa3aca5742a8520388e668df501f753cb7ca679 `
3+ Mathlib version: ` 24899e1184118f6ac3a1584767be5e6ad9c8d18e `
44
55## \# adaptation_note
66Defined in: ` «tactic#adaptation_note_» `
@@ -2474,6 +2474,38 @@ Defined in: `tacticFconstructor`
24742474(it calls ` apply ` using the first matching constructor of an inductive datatype)
24752475except that it does not reorder goals.
24762476
2477+ ## field
2478+ Defined in: ` Mathlib.Tactic.FieldSimp.field `
2479+
2480+ The ` field ` tactic proves equality goals in (semi-)fields. For example:
2481+ ``` lean
2482+ example {x y : ℚ} (hx : x + y ≠ 0) : x / (x + y) + y / (x + y) = 1 := by
2483+ field
2484+ example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by field
2485+ ```
2486+ The scope of the tactic is equality goals which are * universal* , in the sense that they are true in
2487+ any field in which the appropriate denominators don't vanish. (That is, they are consequences purely
2488+ of the field axioms.)
2489+
2490+ Checking the nonvanishing of the necessary denominators is done using a variety of tricks -- in
2491+ particular this part of the reasoning is non-universal, i.e. can be specific to the field at hand
2492+ (order properties, explicit ` ≠ 0 ` hypotheses, ` CharZero ` if that is known, etc). The user can also
2493+ provide additional terms to help with the nonzeroness proofs. For example:
2494+ ``` lean
2495+ example {K : Type*} [Field K] (hK : ∀ x : K, x ^ 2 + 1 ≠ 0) (x : K) :
2496+ 1 / (x ^ 2 + 1) + x ^ 2 / (x ^ 2 + 1) = 1 := by
2497+ field [hK]
2498+ ```
2499+
2500+ The ` field ` tactic is built from the tactics ` field_simp ` (which clears the denominators) and ` ring `
2501+ (which proves equality goals universally true in commutative (semi-)rings). If ` field ` fails to
2502+ prove your goal, you may still be able to prove your goal by running the ` field_simp ` and ` ring_nf `
2503+ normalizations in some order. For example, this statement:
2504+ ``` lean
2505+ example {a b : ℚ} (H : b + a ≠ 0) : a / (a + b) + b / (b + a) = 1
2506+ ```
2507+ is not proved by ` field ` but is proved by ` ring_nf at *; field ` .
2508+
24772509## field_simp
24782510Defined in: ` Mathlib.Tactic.FieldSimp.fieldSimp `
24792511
@@ -2497,6 +2529,10 @@ example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
24972529 -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
24982530```
24992531
2532+ A very common pattern is ` field_simp; ring ` (clear denominators, then the resulting goal is
2533+ solvable by the axioms of a commutative ring). The finishing tactic ` field ` is a shorthand for this
2534+ pattern.
2535+
25002536Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
25012537side conditions. The ` field_simp ` tactic attempts to discharge these, and will omit such steps if it
25022538cannot discharge the corresponding side conditions. The discharger will try, among other things,
@@ -5561,11 +5597,16 @@ Defined in: `Lean.Parser.Tactic.open`
55615597but it opens a namespace only within the tactics ` tacs ` .
55625598
55635599## order
5564- Defined in: ` Mathlib.Tactic.Order.tacticOrder `
5600+ Defined in: ` Mathlib.Tactic.Order.tacticOrder_ `
55655601
55665602A finishing tactic for solving goals in arbitrary ` Preorder ` , ` PartialOrder ` ,
55675603or ` LinearOrder ` . Supports ` ⊤ ` , ` ⊥ ` , and lattice operations.
55685604
5605+ ## order_core
5606+ Defined in: ` Mathlib.Tactic.Order.order_core `
5607+
5608+ ` order_core ` is the part of the ` order ` tactic that tries to find a contradiction.
5609+
55695610## peel
55705611Defined in: ` Mathlib.Tactic.Peel.peel `
55715612
0 commit comments