suffices

suffices は、数学でよくある「～を示せば十分である」という推論を行うタクティクです。

ゴールが ⊢ P であるときに suffices Q from を実行すると、

suffices Q from のブロック内では、仮定に this: Q が追加され、
suffices Q from 以降では、ゴールが ⊢ Q に書き換えられます。

apply と似ていますが、apply と違って「十分条件になっていること」の証明が明らかでないときにも使うことができます。

suffices Q from ... という形式の場合は、証明を直接構成することが必要です。suffices Q from by ... とすると、タクティクによって証明を構成するモードになります。

import Mathlib.Data.Nat.Order.Lemmas -- 除算 `∣` を使うため

example : 13 ∣ (2 ^ 70 + 3 ^ 70) := by
  -- 余りがゼロであることを示せば十分
  suffices (2 ^ 70 + 3 ^ 70) % 13 = 0 from by
    exact Iff.mpr (Nat.dvd_iff_div_mul_eq (2 ^ 70 + 3 ^ 70) 13) rfl

  rfl

Lean by Example

suffices