現状では lean4:v4.3.0-rc2 ですが，最新は /lean4:v4.4.0-rc1 です

simp_arith, norm_num, linarith はどれも 1 < 2 のようなゴールを閉じることができるタクティクですが，このうち linarith だけ紹介されています．しかし linarith は重めのタクティクです．linarith が必要でない場面では，機能は制限されていてもより軽量なタクティクを使った方が良いように思います．

上記のような注意書きを付け加えるのはいかがでしょうか？

以下のタクティクを追加する：

• nlinarith
• replace

補足
補題を示すだけでなく，ある特定の形をした主張を分解するのにも have は使うことができます．これは実は have に特有の機能ではありませんが，have と組み合わせて使うことが多いのでここで紹介します．

匿名コンストラクタという名前を出し，TPiL へのリンクを貼る

show のドキュメントとしての使い道しか紹介しないのはまずい

この部分が古い．lake-packages はもう使わない．

      - name: Cache dependencies
        uses: actions/cache@v3
        with:
          path: |
            ./lake-packages
          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
          restore-keys: |
            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}

Theorem Proving をちょうど読んでいて，そこで触れられているもので載っていないものを探してみました

• let
• intros (introでも特に触れられていない)
• rename_i
• revert
• match
• simp_arith
• generalize

コンビネータ寄り？

• #35
• #36
• all_goals/any_goals

コンビネータも入れたい？（別 Issue にすべきであればそうします，セクションをそもそも分けたほうがいいかもしれません)

• ;
• <;>
• first| tac| ...

また，以下細かい点

• (目次に) rwはあるがrewriteはない
• (目次に) sorryはあるがadmitはない

あくまでも good first issue として役立てばと思い列挙させていただきました，私も取り組めそうなとこから触ってみようかなと思います

TPiL は初心者にとっては読みづらい文献．

重要なキーワードである calc 構文の使い方を雑でいいので紹介しておくべきだと思う．

コード例にはフィボナッチ数列の例を使えばいいかな

import Mathlib.Tactic

theorem T (x y : Nat) (h: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
  apply?

  -- なぜ subgoal が残ってるのに done が通るのか
  done

#explode T

出力の中に sorryAx がある．勝手に sorry しているし，警告も出ない

leanprover-community/batteries#463

TPiL を紹介するのを忘れていたので，追加する．

コード例の案. apply? と少し挙動が異なる

import Mathlib.Tactic

variable (P Q : Prop)

example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
  -- `Try this: exact hQR (hPQ hQ)` と出力される
  exact?

  -- 証明は `exact?` だけで終わっている!
  done

wlog を使うありがたみを感じさせる例に変更したい

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60fun_prop.60.20new.20tactic.20for.20Differentiable.2C.20Continuous.2C.20.2E.2E.2E

import Mathlib.Tactic

variable {u v : ℝ → ℝ} (hu : Continuous u) (hv : Continuous v)

/-- 連続関数の積は連続関数 -/
example : Continuous (fun x ↦ u x * v x) := by 
  fun_prop

/-- 有理関数が可測関数であることを示す -/
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x * x) := by
  fun_prop

find
eval
check
print
guard
time
check_failure （優先度低い）
guard_msgs （要らないかも）
help

unfold と rw, dsimp 等がどう違うのかについても，できれば説明したい

any_goals に比べて使う機会も多そうに思えるので，all_goals 単体でまず紹介する

どう考えても rel より先に gcongr を紹介すべきだったと思う

hint は証明に残さない

rwは書き換え可能な箇所をすべて書き換えるタクティックですが、これに対して式中で書き換え可能な箇所のうちn番目のみ書き換えるnth_rewriteというタクティックがあります。
https://leanprover-community.github.io/mathlib_docs/tactic/nth_rewrite/default.html
例えば以下のように用いることができます。
https://github.com/s-taiga/lean-math-workshop-my-solution/blob/d58278dc98ac95129c3ce7d7627dec70110dc2f4/Tutorial/Advanced/Algebra/Lecture1.lean#L262
個人的には先日の勉強会時にはかなりお世話になったタクティックだったので、言及があると良いのではないかと思います。

コード例がコンパイルできることを、git hub action を用いて確かめる

main へのプッシュと pull request ごとに走らせる

tauto は古典論理に依存するものも示せるが、aesopでは示せないようだ。これは偶然ではなさそう

便利なわりに知名度が低いようなので紹介する価値はありそう

cheat sheet が正しい.

GitHub Page の URLが変わってしまうため、リダイレクトも設定する必要がある

現在の記述 https://lean-ja.github.io/tactic-cheetsheet/rfl.html ではrflは項のdefinitional equalityを証明するもののように書かれていますが, ドキュメント https://leanprover-community.github.io/mathlib4_docs//Mathlib/Tactic/Relation/Rfl.html によるとこれは refl attributeのついた定理を用いて関係の反射性を示すといったほうが正確ではないかと思います。例えば以下のように順序の反射性を証明することが可能です.

example (n : ℕ) : n ≤ n := by rfl

トップの、全タクティクリストのところの説明に誤字が残ってる

GitHub Pages へのリンクは修正し，リダイレクトも行ったが，リポジトリ自体へのリンクが古いままになってしまっている．

メリット

• 今までは md ファイルと lean ファイルの両方を作成していたが，mdgen で一本化できる （既にかなりのタクティクを紹介済みなのでメリットは薄いが…）
• 一つの大きなコードブロックに説明を書くと，読みづらくなってしまう．今まで特にコマンド紹介欄でそれが顕著だった．（コマンド紹介欄はもう対応済み）

デメリット

• 作業が大変．残り 55 個のタクティクに対して行わないといけない．

作業内容

1. Examples/Tactic ディレクトリに lean ファイルを移し，そこからビルドした md ファイルを src ディレクトリに配置するように変更する．
2. 従来 md ファイルと lean ファイルに分かれている内容を，lean ファイルに一本化する
3. 1-2 を 55 タクティクに対して繰り返す

デバッグに便利なので紹介する価値はある

タクティクではあるけど、証明と関係がないので紹介しない方が良いかもしれない。「数学に役立つ」リストとしては要らないはず

現在は racses と cases が同じページだったり，simp と dsimp が同じページだったりしている．

派生タクティクは，一言説明を考えるのが難しいので同じページにまとめたくなってしまい，このようにしていた．

しかし，紹介するタクティクが多くなってきて，（当初の想定の早見表としてだけでなく）辞書のような使われ方をすることも今後想定される．そうなった場合，一ページあたり一タクティクの方が統一感がある．

mdgen でleanからmdファイルを生成するようになったことで、リンク切れが多くなっているようだ

統一するか、きちんと違いを説明するべき

普通は ∃ x P x を示すとき，先に x を具体的に渡す．

しかし，P を変形してから x を考えることもできる．

example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  intro y
  use ?term
  simp
  show c * ?term = y

  case term =>
    exact c⁻¹ * y

  case h =>
    rw [mul_inv_cancel_left₀ h y]

rw のページに追記する

直接 Action からデプロイする方式に変更する

MIL を参考に例を取るとよいかもしれない

example (h : Monotone f) (h' : f a < f b) : a < b := by
  contrapose! h'
  apply h
  assumption

sorry を使わない非自明な例にしたい。

コード例の中で使用したいこともあるので

プルリクエストに対してデプロイは行うことができない．しかし，mdbook のビルドが通るかチェックはできるし，生成されたアーティファクトを確認することもできる．

この設定がないと，GitHub Pages の見た目を変えるための PR の結果をテストするのに，main ブランチにいったんマージする必要が生じてしまう．

guard_hyp のところ

たとえば apply at 構文などは，「追加の import 文が必要」とだけ書かれていて何を import すればいいのか書かれていない．

これは露骨に不親切なので，きちんと書くべき．

当初は「便利なタクティクを集めて，早見表を作る」のが目的でしたが，紹介するタクティクが多くなってきて辞書のようになりつつあります．早見表としての利便性は確保できているのでしょうか…？

個人的には日本語検索が可能になった時点で十分だと感じていましたが，まだ足りないかもしれません．

Lean 初心者の意見を聞きたいところです．