InteractingWithLean.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 26 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index

84 declarations, 3 contain sorry, 0 declared as axioms

Imports (2)

VersoManual
TPiL.Examples

def x sorry line 59 source
def double line 150 source
Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:547 (different declaration text). Qualify references as double@path.
theorem t1 line 158 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:224 (different declaration text). Qualify references as t1@path.
theorem t2 line 165 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:319 (different declaration text). Qualify references as t2@path.
def Foo.bar line 193 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:611 (different declaration text). Qualify references as Foo.bar@path.
def Foo.bar line 206 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:611 (different declaration text). Qualify references as Foo.bar@path.
def Foo.bar line 213 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:611 (different declaration text). Qualify references as Foo.bar@path.
def String.add line 225 source
def Bool.add line 228 source
def add line 231 source
Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:600 (different declaration text), book/TPiL/InductionAndRecursion.lean:505 (different declaration text). Qualify references as add@path.
def Foo.bar line 255 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:611 (different declaration text). Qualify references as Foo.bar@path.
def isPrefix line 339 source
theorem List.isPrefix_self line 342 source
example (example at line 345) line 345 source
def isPrefix line 354 source
theorem List.isPrefix_self line 357 source
Source comment
----
```
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
…
```
Mentions: as, α, isPrefix
def isPrefix line 368 source
theorem List.isPrefix_self line 373 source
example (example at line 378) line 378 source
example (example at line 385) line 385 source
def isPrefix line 396 source
instance (instance at line 399) line 399 source
theorem List.isPrefix_self line 402 source
def isPrefix line 411 source
abbrev instLe line 414 source
Source comment
----
```
abbrev instLe : LE (List α) :=
…
```
Mentions: α
example (example at line 420) line 420 source
example (example at line 432) line 432 source
def f line 468 source
Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.
example (example at line 470) line 470 source
Source comment
Equivalent:
```
example := f 7
```
example (example at line 471) line 471 source
def f line 482 source
Distinct definitions of this name: book/TPiL/AxiomsComputation.lean:340 (different declaration text), book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.
example (example at line 484) line 484 source
Source comment
Just f 7
```
example := f 7
```
example (example at line 486) line 486 source
Source comment
These are equivalent:
```
example := @f 7 _ 3
```
example (example at line 487) line 487 source
def f' Alternative syntax: line 489 source
Source comment
Alternative syntax:
```
def f' (x : Nat) ⦃y : Nat⦄ (z : Nat) : Nat := x + y + z
…
```
Mentions: x
def reflexive line 507 source
def symmetric line 510 source
def transitive line 513 source
def Euclidean line 516 source
theorem th1 line 519 source
theorem th2 line 526 source
theorem th3 line 533 source
def reflexive line 553 source
def symmetric line 556 source
def transitive line 559 source
def Euclidean line 562 source
theorem th1 line 565 source
theorem th2 line 572 source
theorem th3 line 579 source
def wobble sorry line 679 source
def wobble sorry line 687 source
def foo a user-defined function line 784 source
Source comment
a user-defined function

Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:779 (different declaration text), book/TPiL/InductionAndRecursion.lean:115 (different declaration text). Qualify references as foo@path.
```
def foo {α : Type u} (x : α) : α := x
…
```
Mentions: α, x
example {lit}`Nat`.(example at line 935) line 935 source
def {lit}`Nat`.compose line 996 source
def {lit}`Nat`.compose line 1006 source
def {lit}`Nat`.compose line 1025 source
def {lit}`Nat`.compose line 1067 source
instance {lit}`Nat`.(instance at line 1091) line 1091 source
Source comment
----
```
instance : Monad (ReaderT ρ m) where
…
```
Mentions: m
def {lit}`Nat`.Ex2.id1 line 1105 source
Source comment
----
```
def id1 : {α : Type} → α → α :=
…
```
Mentions: α
def {lit}`Nat`.Ex2.listId line 1108 source
def {lit}`Nat`.Ex2.id2 In this example, implicit lambda introduction has been disabled because we use @ before {kw}fun line 1113 source
Source comment
In this example, implicit lambda introduction has been disabled because we use `@` before {kw}`fun`
```
def id2 : {α : Type} → α → α :=
…
```
Mentions: α
def {lit}`Nat`.Ex2.id3 line 1116 source
def {lit}`Nat`.Ex2.id4 line 1119 source
def {lit}`Nat`.Ex2.id5 In this example, implicit lambda introduction has been disabled because we used the binder annotation {...} line 1124 source
Source comment
In this example, implicit lambda introduction has been disabled because we used the binder annotation `{...}`
```
def id5 : {α : Type} → α → α :=
…
```
Mentions: α
def {lit}`Nat`.Ex3.f line 1150 source
def {lit}`Nat`.sum line 1180 source
example {lit}`Nat`.(example at line 1186) line 1186 source
def {lit}`Nat`.f line 1196 source
example {lit}`Nat`.(example at line 1199) line 1199 source
example {lit}`Nat`.(example at line 1201) line 1201 source
example {lit}`Nat`.(example at line 1203) line 1203 source
example {lit}`Nat`.(example at line 1205) line 1205 source
example {lit}`Nat`.(example at line 1207) line 1207 source
example {lit}`Nat`.(example at line 1209) line 1209 source
def {lit}`Nat`.g line 1211 source
example {lit}`Nat`.(example at line 1218) line 1218 source
example {lit}`Nat`.(example at line 1220) line 1220 source
example {lit}`Nat`.(example at line 1222) line 1222 source
example {lit}`Nat`.(example at line 1224) line 1224 source
example {lit}`Nat`.(example at line 1226) line 1226 source
inductive {lit}`Nat`.Term line 1233 source
def {lit}`Nat`.getBinderName line 1239 source
def {lit}`Nat`.getBinderType line 1243 source
example {lit}`Nat`.(example at line 1252) line 1252 source