証明状態にあるゴールはメインゴールを上にして順番に表示されます。ゴールには名前付きのものと匿名のものがあります。名前付きゴールは先頭に case と表示され（ ケースラベル 、case label と呼ばれます）、一方で匿名のゴールにはそのような表示はありません。タクティクは通常、コンストラクタ名・パラメータ名・構造体フィールド名・タクティクなどによって実装される推論ステップの性質に基づいて、ゴール名を割り当てます。
この証明状態には4つのゴールが含まれ、そのすべてに名前が付けられています。これは Monad Option インスタンスが合法であること（つまり LawfulMonad Option インスタンスを提供すること）の証明の一部であり、ケース名（以下でハイライトしているもの）は LawfulMonad のフィールド名に由来します。
case と case' タクティクを使用すると、希望するゴール名を使用して新しいメインゴールを選択することができます。名前付きのゴールのコンテキストにて名前が割り当てられると、新しいゴールの名前はメインゴールの名前との間にドット（'.'、Unicode FULL STOP (0x2e)）を挟んだものとして追加されます。
∀ (n k : Nat), n + k = k + n を証明しようとしている過程において、以下のような証明状態が起こりえます：
⊢ 0 + 0 = 0 + 0n✝:Nata✝:0 + n✝ = n✝ + 0⊢ 0 + (n✝ + 1) = n✝ + 1 + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1) の後、2つの新しいケースの名前は接頭辞として zero を持ちます。これはその名前のゴール内で作られたためです：
各ゴールは一連の仮定と期待される結論から構成されます。それぞれの仮定には名前と型があります；結論は型です。仮定はある型の任意の要素か、真であると推定される文のどちらかです。
このゴールは4つの仮定を持ちます：
これらはそれぞれ：
α 、任意の型
x 、 α 型の任意の値
xs 、 List α 型の任意の値
ih 、帰納法の仮定で、これは空のリストを xs に追加したものが xs と等しいことを主張します。
結論は、帰納法の仮定の等号の両辺に x を先頭に追加すると等しいリストになるという文です。
いくつかの仮定は アクセス不能 （inaccessible）です。これは名前によって明示的に参照できないことを意味します。アクセス不能な仮定は、仮定が指定された名前なしで作成された時、または仮定の名前がそれより後に作られた仮定によってシャドーイングされた時に発生します。アクセス不能な仮定は匿名とみなされるべきです；それらが名前を持っているかのように表示されるのは、それらが後の仮定または結論で参照される可能性があり、名前を表示することでこれらの参照を互いに区別することができるからです。特に、アクセス不能な仮定には、その名前の後に短剣（†）が表示されます。
この証明状態では、すべての仮定がアクセス可能です。
この証明状態では1つ目と3つ目の仮定だけがアクセス可能です。2番目と4番目はアクセス不能であり、その名前には参照できないことを示す短剣が含まれています。
アクセス不能な仮定はそれでもなお使用することができます。 assumption や simp などのタクティクは、仮定のリスト全体をスキャンし、有用なものを見つけることができ、 contradiction は名前を付けずに不可能な仮定を見つけることで現在のゴールを除去することができます。その他のタクティク、例えば rename_i と next はアクセス不能な仮定に名前を付け、アクセス可能にするために使用できます。さらに、仮定はその型を単一のギュメで書くことによって、その型から参照することができます。
項を囲む単一のキュメはその型を持つスコープ内の項への参照を表します。
term ::= ...
| `‹t›` resolves to an (arbitrary) hypothesis of type `t`.
It is useful for referring to hypotheses without accessible names.
`t` may contain holes that are solved by unification with the expected type;
in particular, `‹_›` is a shortcut for `by assumption`.
これは名前ではなく定理文によってローカルの補題を参照したり、明示的な名前の有無に関係なく仮定を参照したりするのに使うことができます。
variable (n : Nat)
以下の証明において、 cases は数を解析するために繰り返し使用されています。証明の最初では、数は x という名前ですが、 cases はそれ以降の数に対してアクセス不能な名前を生成します。名前を提供する代わりに、証明は任意の時点で Nat 型の仮定が1つ存在するという事実を利用し、それを参照するために ‹Nat› を使用します。繰り返しののち、n + 3 < 3 という仮定が残り、これは contradiction を使うことでゴールを考慮から除くことができます。
example : x < 3 → x ∈ [0, 1, 2] := x:Nat⊢ x < 3 → x ∈ [0, 1, 2]
x:Nata✝:x < 3⊢ x ∈ [0, 1, 2]
iterate 3
a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2]n✝:Nata✝:n✝ + 1 + 1 + 1 < 3⊢ n✝ + 1 + 1 + 1 ∈ [0, 1, 2]
a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2] All goals completed! 🐙
All goals completed! 🐙
単一のギュメ構文は証明以外でも帰納します：
#eval
let x := 1
let y := 2
‹Nat›
2
しかし、これは非命題に対しては一般的に良いアイデアではありません。ある型の どの 要素が選択されるかが重要な場合は明示的に選択する方が良いでしょう。
証明状態の項は非常に大きくなることがあり、多くの仮定が存在することもあります。定義上の証明の irrelevance により通常、証明項はほとんど有用な情報を与えません。デフォルトでは、 アトミック でない限り、証明状態のゴールには表示されません。アトミックとは部分項を持たないことを意味します。証明の非表示は2つのオプションで制御できます： pp.proofs はこの機能のオン・オフを切り替え、 pp.proofs.threshold は証明の非表示のサイズ閾値を決定します。
pp.proofs
Default value: false
(pretty printer) display proofs when true, and replace proofs appearing within expressions by ⋯ when false
pp.proofs.threshold
Default value: 0
(pretty printer) when pp.proofs is false, controls the complexity of proofs at which they begin being replaced with ⋯
さらに、非証明項が大きすぎる場合は非表示にすることができます。特に、Lean は一定の深さの閾値（設定可能）以下の項を非表示にし、合計が一定量表示されると残りの項を非表示にします。深い項の表示の有効・無効はオプション pp.deepTerms で、深さの閾値はオプション pp.deepTerms.threshold で設定できます。プリティプリンタの最大ステップ数はオプション pp.maxSteps で設定できます。非常に大きな項の表示はツールの速度低下を招き、スタックオーバーフローになることもあります；これらのオプションの値を調整する時は控えめになるようにしましょう。
pp.deepTerms
Default value: false
(pretty printer) display deeply nested terms, replacing them with ⋯ if set to false
pp.deepTerms.threshold
Default value: 50
(pretty printer) when pp.deepTerms is false, the depth at which terms start being replaced with ⋯
pp.maxSteps
Default value: 5000
(pretty printer) maximum number of expressions to visit, after which terms will pretty print as ⋯
疑問符で始まる項は未知の値に対応する メタ変数 （metavariable）です。これらは 宇宙 レベルか項のいずれかを表すこともあります。メタ変数の中には、Lean のエラボレーションプロセスの一環として、値を決定するのに十分な情報が得られていないときに生じるものがあります。このようなメタ変数の名前の最後には ?m.392 や ?u.498 のように数字が付きます。その他のメタ変数はタクティクや named holes の結果として存在するようになります。これらのメタ変数の名前には数字の要素はありません。タクティクの結果として生じるメタ変数は ケースラベル がメタ変数の名前と一致するゴールとして現れることが多いです。
この証明状態において、宇宙レベル α は不明です：
この証明状態において、リスト要素の型は不明です。このメタ変数は繰り返し出現しています。これはこの不明な型が両方の位置で同じ出なければならないからです。
この証明状態において、
タクティク i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?mi:Natj:Natk:Nath1:i < jh2:j < k⊢ ?m < ki:Natj:Natk:Nath1:i < jh2:j < k⊢ Nat を適用すると、以下のような証明状態になり、推移性ステップの中間値 ?m が不明となります：
明示的な名前付きホールはメタ変数で表現され、さらに証明ゴールを生みます。この証明状態において、
ここでタクティク i:Natj:Natk:Nath1:i < jh2:j < k⊢ Nati:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?middlei:Natj:Natk:Nath1:i < jh2:j < k⊢ ?middle < k を適用すると、以下のような証明状態になります。このとき、推移性ステップの中間値 ?middle は不明であり、項内の名前付きホールのそれぞれに対してゴールが作成されています。
メタ変数の番号の表示はオプション pp.mvars を使うことで無効にできます。これは Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.
Basic example:
```lean
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`.
Message filters (processed in left-to-right order):
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
(the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
Message ordering:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
This helps with testing commands that are non-deterministic in their ordering.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
#guard_msgs のような Lean の出力と希望する文字列をマッチさせる機能を使うときに便利です。さらにカスタムのタクティクに対するテストを書くときに非常に便利です。
pp.mvars
Default value: true
(pretty printer) display names of metavariables when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables)
Demonstrate and explain diff labels that show the difference between the steps of a proof state.
Tracked at issue #68