YouTubeでLeanのやつ - コラッツ予想がとけたらいいな2

https://www.youtube.com/watch?v=ArGLTAjak3g
YouTubeでLeanの動画があるのだけれど、
結構すごそうなので、自分でもやってみたいと思った。

拡張ライブラリmathlibを使う。
Coqに対するSSReflectのような物か。

インストール

https://leanprover-community.github.io/install/windows.html
の手順に従う。Windowsです。

elanのインストール
elanはLeanのパッケージマネージャだ。
https://github.com/Kha/elan/releases/
Git for Windowsを入れているなら、git bashが使えるから、それで実行した。
C:\Users\[user]\.elan\binにlean.exeとかが配置された。
こっちでpathを通す必要はなかった。
Python 3.xのインストール
インストール後、
git bashで$ git config --global core.autocrlf input
コマンドプロンプトで$ pip3 install mathlibtools
pip3のアップデートを促されたら、それに従う。
VSCode
VSCodeの拡張機能「Lean for VS Code」を入れる。
（1回だけ）適当な場所で$ source ~/.profile
適当な場所で$ leanproject new test
これで「test」というプロジェクトが作られる。
$ cd testして、$ code .
別窓で、testプロジェクトが開かれる。
「src」の下に「primes01.lean」というファイルを作って、
以下を貼り付ける。

import data.nat.prime

open nat

theorem exists_infinite_primes :
  ∀ n : ℕ, ∃ p, p ≥ n ∧ prime p :=
begin
  intro N,
  let M := fact N + 1,
  let p := min_fac M,

  have pp : prime p := sorry,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ M      := sorry,
    have h₂ : p ∣ fact N := sorry,
    have h  : p ∣ 1      := sorry,
    sorry,
  },
  { assumption, },
end

ソース上で適当にカーソルを動かして、
右のLean Goalタブにゴールが出たら成功だ。

そして、
彼のリポジトリ（semorrison/lean-tidy）を動かしても、backというタクティクは出来なかった。
まあ、「Warning --- the automation in this demo is cheating;...」
って書いてるし、出来ないのかもしれない。

この定理の完成版を貼っておきます。

import data.nat.prime

open nat

theorem exists_infinite_primes :
  ∀ n : ℕ, ∃ p, p ≥ n ∧ prime p :=
begin
  intro N,
  let M := fact N + 1,
  let p := min_fac M,

  have pp : prime p := 
    begin
      apply min_fac_prime,
      apply ne_of_gt,
      apply succ_lt_succ,
      apply fact_pos,
    end,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ M      , { library_search },
    have h₂ : p ∣ fact N :=
      dvd_fact (prime.pos pp) (le_of_lt (not_le.mp a)),
    have h  : p ∣ 1      , { library_search },
    exact prime.not_dvd_one pp h,
  },
  { assumption, },
end