ダメな証拠：ゴールのゴール

https://leanprover.github.io/reference/tactics.html#basic-tactics

This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation,

この言い回しにはさんざん悩まされた。「ゴール」に意味が。

1. 証明状態
2. メインゴール
3. 一般的なゴール
4. ゴールのターゲット
5. CoqのGoal選言

ほんとに腹たったわ！