wlog

wlog は，数学でよく使われる，一般性を失うことなく(without loss of generarity)何々と仮定してよいというフレーズの Lean での対応物です．

import Mathlib.Tactic -- 大雑把に import する

-- `n` と `m` は自然数
variable {n m : ℕ}

example (h : n ≠ m) : 0 < |(n - m : ℤ)| := by
  -- 一般性を失うことなく `m < n` と仮定して良い
  wlog hnm : m < n with H

  -- `m < n` の時に成り立つのであれば，そうでないときも成り立つことを示す
  case inr =>
    -- `m < n` ではないので，`n < m` が成り立つ
    have : m = n ∨ n < m := Nat.eq_or_lt_of_not_lt hnm
    replace : n < m := by aesop

    -- `m < n` の時に成り立つという仮定を利用できる
    replace : 0 < |(m - n : ℤ)| := @H m n h.symm this

    rw [abs_sub_comm]
    assumption

  -- `m < n` と仮定してよいことがわかったので，
  -- `m < n` だとして証明する
  apply abs_pos_of_pos
  simp_all