field_simp

field_simp は，体における等式を示す際の「分母を払う」操作に対応するタクティクです．

import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring

example (n m : Rat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  -- 分母を払う
  field_simp

  -- Rat は可換環なので， 示すべきことが言える
  ring

分母がゼロでないことが判らない場合は動作しません．分母がゼロでないことを証明してローカルコンテキストに加えると動作することがあります．

example {x y z : Rat} (hy : y = z ^ 2 + 1) : (x + 2 * y) / y = x / y + 2 := by
  -- 最初 `field_simp` は動作しない
  fail_if_success field_simp

  -- 分母がゼロでないことを示す
  have ypos : y ≠ 0 := by
    rw [hy]
    nlinarith

  -- 動作するようになった
  field_simp

制約

field_simp という名前の通り，割り算が体の割り算でなければ動作しません．たとえば 自然数 Nat における割り算は field_simp では扱うことができず，次のコード例のように工夫する必要があります．

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  -- field_simp は動作しない
  fail_if_success field_simp

  -- 分母を払う
  symm
  apply Nat.div_eq_of_eq_mul_right (by simp_arith)

  -- `(n + m) ^ 2` を展開する
  rw [show (n + m) ^ 2 = n ^ 2 + 2 * n * m + m ^ 2 from by ring]

  -- 打消し合う項を消して簡単にすれば，示すべきことが言える
  simp [add_assoc, mul_assoc]

また field_simp の扱うのは等式のみで，順序関係は扱いません．体の定義に順序関係は含まれていないので，体を扱うタクティクとしては自然なことかもしれません．

variable (x y : Rat)

example : x * y ≤ (x ^ 2 + y ^ 2) / 2 := by
  -- 何も起こらない
  fail_if_success field_simp

  suffices x ^ 2 - 2 * x * y + y ^ 2 ≥ 0 from by
    linarith
  calc
    x ^ 2 - 2 * x * y + y ^ 2 = (x - y) ^ 2 := by ring
    _ ≥ 0 := by apply sq_nonneg

example (h : x = y) : x * y = (x ^ 2 + y ^ 2) / 2 := by
  -- 等式ならば扱える
  field_simp

  -- ゴールの分母を払うことができた
  show x * y * 2 = x ^ 2 + y ^ 2

  rw [h]
  ring