norm_cast タクティクを紹介する

[Seasawher]

このタクティクはなんと論文も出ている。

https://arxiv.org/abs/2001.10594

[Seasawher]

レイリーの定理の過程でこのタクティクが活躍する場面があった。

    -- `x` と `m + n` はともに自然数なので、これは矛盾である。
    have : False := by
      /-
      x m n : ℕ
      left : ↑x < ↑m + ↑n
      right : ↑m + ↑n < ↑x + 1
      ⊢ False
      -/
      norm_cast at left right
      omega

[Seasawher]

age