InductiveTypes.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

152 declarations, 6 contain sorry, 0 declared as axioms

Imports (2)

VersoManual
TPiL.Examples

inductive Foo line 40 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:608 (same statement text; different proof or body). Qualify references as Foo@path.
inductive Foo line 48 source
Distinct definitions of this name: book/TPiL/PropositionsAndProofs.lean:608 (same statement text; different proof or body). Qualify references as Foo@path.
inductive Weekday line 101 source
inductive Weekday line 115 source
inductive Weekday line 138 source
inductive Weekday line 150 source
inductive Weekday line 190 source
def numberOfDay line 201 source
inductive Weekday line 224 source
def numberOfDay line 235 source
inductive Weekday line 262 source
structure in line 279 source
inductive Weekday line 287 source
def Weekday.next line 298 source
def Weekday.previous line 308 source
example Weekday.(example at line 322) line 322 source
inductive Weekday line 335 source
def Weekday.next line 345 source
def Weekday.previous line 354 source
theorem Weekday.next_previous next undoes previous, by cases on the constructors line 364 source
Source comment
----
L4DEL explanation
Weekday has seven constructors, so match gives seven cases, each true by computation.
1. Weekday is an inductive type with constructors sunday through saturday, and next and previous move one day forward and back.
2. theorem next_previous (d : Weekday) : next (previous d) = d is proved with match d with.
3. In each of the seven cases the two sides reduce to the same constructor, so the proof is rfl.
4. The book follows this with a shorter version of the proof.
Sources and attribution: Pinned Lean source (4e28129fdd58)
inductive type: a type generated freely by a list of constructors, such as the seven weekdays.
```
theorem next_previous (d : Weekday) : next (previous d) = d :=
…
```
Mentions: Weekday.Weekday, Weekday.next, Weekday.previous
inductive Weekday.Weekday line 379 source
def Weekday.Weekday.next line 389 source
def Weekday.Weekday.previous line 398 source
theorem Weekday.Weekday.next_previous line 408 source
Source comment
----
```
theorem next_previous (d : Weekday) : next (previous d) = d := by
…
```
Mentions: Weekday.Weekday, Weekday.Weekday.next, Weekday.Weekday.previous
inductive Weekday.Weekday.Hidden.Bool line 427 source
Source comment
----
```
inductive Bool where
…
```
def Weekday.Weekday.Hidden.and line 450 source
Source comment
----
```
def and (a b : Bool) : Bool :=
…
```
Mentions: b, Weekday.Weekday.Hidden.Bool
inductive Weekday.Weekday.Hidden.Prod line 480 source
Source comment
----
```
inductive Prod (α : Type u) (β : Type v)
  | mk : α → β → Prod α β
```
Mentions: α, β
inductive Weekday.Weekday.Hidden.Sum line 483 source
inductive Weekday.Weekday.Hidden.Prod line 501 source
def Weekday.Weekday.Hidden.fst line 504 source
Source comment
----
```
def fst {α : Type u} {β : Type v} (p : Prod α β) : α :=
…
```
Mentions: α, β, Weekday.Weekday.Hidden.Prod
def Weekday.Weekday.Hidden.snd line 508 source
def Weekday.Weekday.prod_example line 531 source
def Weekday.Weekday.sum_example line 564 source
inductive Weekday.Weekday.Hidden.Prod line 623 source
Source comment
----
```
inductive Prod (α : Type u) (β : Type v) where
…
```
Mentions: α, β
inductive Weekday.Weekday.Hidden.Sum line 626 source
structure Weekday.Weekday.Hidden.Prod line 646 source
Source comment
----
```
structure Prod (α : Type u) (β : Type v) where
…
```
Mentions: α, β
example Weekday.Weekday.(example at line 660) line 660 source
structure Weekday.Weekday.Color line 664 source
def Weekday.Weekday.yellow line 670 source
structure Weekday.Weekday.Semigroup line 684 source
inductive Weekday.Weekday.Hidden.Sigma line 698 source
Source comment
----
```
inductive Sigma {α : Type u} (β : α → Type v) where
…
```
Mentions: α, β
inductive Weekday.Weekday.Hidden.Option line 710 source
Source comment
----
```
inductive Option (α : Type u) where
…
```
Mentions: α
inductive Weekday.Weekday.Hidden.Inhabited line 714 source
inductive Weekday.Weekday.Hidden.False line 762 source
Source comment
----
```
inductive False : Prop
```
inductive Weekday.Weekday.Hidden.True line 764 source
inductive Weekday.Weekday.Hidden.And line 767 source
inductive Weekday.Weekday.Hidden.Or line 770 source
inductive Weekday.Weekday.Hidden.Exists line 798 source
Source comment
----
```
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
…
```
Mentions: α
inductive Weekday.Weekday.Hidden.Subtype line 828 source
Source comment
----
```
inductive Subtype {α : Type u} (p : α → Prop) where
…
```
Mentions: α
structure Weekday.Weekday.Hidden.Subtype line 845 source
Source comment
----
```
structure Subtype {α : Sort u} (p : α → Prop) where
…
```
Mentions: α
inductive Weekday.Weekday.Hidden.Nat line 875 source
Source comment
----
```
inductive Nat where
…
```
def Weekday.Weekday.add line 939 source
inductive Weekday.Weekday.Hidden.Nat line 957 source
Source comment
----
```
inductive Nat where
…
```
def Weekday.Weekday.Hidden.add line 962 source
inductive Weekday.Weekday.Hidden.Nat line 981 source
def Weekday.Weekday.Hidden.Nat.add line 988 source
instance Weekday.Weekday.Hidden.Nat.(instance at line 993) line 993 source
theorem Weekday.Weekday.Hidden.Nat.add_zero line 996 source
theorem Weekday.Weekday.Hidden.Nat.add_succ line 997 source
theorem Weekday.Weekday.Hidden.zero_add line 1027 source
theorem Weekday.Weekday.Hidden.zero_add line 1053 source
theorem Weekday.Weekday.Hidden.add_assoc line 1077 source
theorem Weekday.Weekday.add_assoc line 1095 source
theorem Weekday.Weekday.add_comm First attempt at commutativity of Nat addition (contains sorry) sorry line 1105 source
L4DEL explanation
Induct on the second argument; one equation in the step is not yet proved and is left as sorry.
1. This is a work-in-progress block in the book: the last calc step ends with := sorry, so Lean accepts it only with a warning.
2. Nat.recOn with motive fun x => m + x = x + m does induction on n; the base case m + 0 = 0 + m is proved with Nat.zero_add and Nat.add_zero.
3. In the inductive step a calc rewrites m + succ n to succ (m + n), then to succ (n + m) using the induction hypothesis.
4. The missing step succ (n + m) = succ n + m is what the book proves next as succ_add, then plugs in to replace the sorry.
See also: Weekday.Weekday.succ_add
Sources and attribution: Pinned Lean source (4e28129fdd58)
induction hypothesis: in the inductive step, the assumption that the property holds for n, used to prove it for succ n.
```
theorem add_comm (m n : Nat) : m + n = n + m :=
…
```
Mentions: m, n
theorem Weekday.Weekday.succ_add sorry line 1122 source
inductive Weekday.Weekday.Hidden.Nat line 1137 source
def Weekday.Weekday.Hidden.add line 1142 source
instance Weekday.Weekday.Hidden.(instance at line 1147) line 1147 source
theorem Weekday.Weekday.Hidden.Nat.add_zero line 1151 source
theorem Weekday.Weekday.Hidden.Nat.add_succ line 1153 source
theorem Weekday.Weekday.Hidden.Nat.zero_add line 1155 source
theorem Weekday.Weekday.Hidden.succ_add line 1163 source
theorem Weekday.Weekday.Hidden.add_comm line 1168 source
inductive Weekday.Weekday.Hidden.List line 1189 source
Source comment
----
```
inductive List (α : Type u) where
…
```
Mentions: α
def Weekday.Weekday.Hidden.List.append line 1195 source
theorem Weekday.Weekday.Hidden.List.nil_append line 1200 source
theorem Weekday.Weekday.Hidden.List.cons_append line 1203 source
inductive Weekday.Weekday.Hidden.List line 1222 source
def Weekday.Weekday.Hidden.List.append line 1226 source
theorem Weekday.Weekday.Hidden.List.nil_append line 1230 source
theorem Weekday.Weekday.Hidden.List.cons_append line 1232 source
theorem Weekday.Weekday.Hidden.List.append_nil sorry line 1236 source
Source comment
----
```
theorem append_nil (as : List α) :
    append as nil = as :=
…
```
Mentions: as, Weekday.Weekday.Hidden.List, α, Weekday.Weekday.Hidden.List.append
theorem Weekday.Weekday.Hidden.List.append_assoc sorry line 1240 source
def Weekday.Weekday.length line 1251 source
def Weekday.Weekday.append line 1252 source
inductive Weekday.Weekday.BinaryTree line 1263 source
inductive Weekday.Weekday.CBTree line 1271 source
def Weekday.Weekday.CBTree.succ line 1277 source
def Weekday.Weekday.CBTree.toCBTree line 1280 source
def Weekday.Weekday.CBTree.omega line 1284 source
example Weekday.Weekday.(example at line 1312) line 1312 source
example Weekday.Weekday.(example at line 1355) line 1355 source
def Weekday.Weekday.f line 1369 source
example Weekday.Weekday.(example at line 1372) line 1372 source
example Weekday.Weekday.(example at line 1373) line 1373 source
def Weekday.Weekday.Tuple line 1379 source
def Weekday.Weekday.f line 1382 source
def Weekday.Weekday.myTuple line 1385 source
example Weekday.Weekday.(example at line 1388) line 1388 source
inductive Weekday.Weekday.Foo line 1395 source
def Weekday.Weekday.silly line 1399 source
inductive Weekday.Weekday.Foo line 1409 source
def Weekday.Weekday.silly line 1413 source
Source comment
----
```
def silly (x : Foo) : Nat := by
…
```
Mentions: x, Weekday.Weekday.Foo
inductive Weekday.Weekday.Foo line 1425 source
def Weekday.Weekday.silly line 1429 source
Source comment
----
```
def silly (x : Foo) : Nat := by
…
```
Mentions: x, Weekday.Weekday.Foo
inductive Weekday.Weekday.Foo line 1439 source
def Weekday.Weekday.silly line 1443 source
Source comment
----
```
def silly (x : Foo) : Nat := by
…
```
Mentions: x, Weekday.Weekday.Foo
example Weekday.Weekday.(example at line 1457) line 1457 source
example Weekday.Weekday.(example at line 1471) line 1471 source
example Weekday.Weekday.(example at line 1493) line 1493 source
example Weekday.Weekday.(example at line 1509) line 1509 source
example Weekday.Weekday.(example at line 1527) line 1527 source
theorem Weekday.Weekday.Hidden.zero_add line 1549 source
Source comment
----
```
theorem zero_add (n : Nat) : 0 + n = n := by
…
```
Mentions: n, Weekday.Weekday.Hidden.Nat
theorem Weekday.Weekday.Hidden.zero_add line 1564 source
Source comment
----
```
theorem zero_add (n : Nat) : 0 + n = n := by
…
```
Mentions: n, Weekday.Weekday.Hidden.Nat
inductive Weekday.Weekday.Hidden.Nat line 1579 source
def Weekday.Weekday.Hidden.Nat.toNat line 1583 source
def Weekday.Weekday.Hidden.Nat.ofNat line 1587 source
def Weekday.Weekday.Hidden.add line 1591 source
instance Weekday.Weekday.Hidden.(instance at line 1596) line 1596 source
instance Weekday.Weekday.Hidden.(instance at line 1599) line 1599 source
theorem Weekday.Weekday.Hidden.zero_zero line 1603 source
theorem Weekday.Weekday.Hidden.add_zero line 1604 source
theorem Weekday.Weekday.Hidden.add_succ line 1605 source
theorem Weekday.Weekday.Hidden.zero_add line 1609 source
theorem Weekday.Weekday.Hidden.succ_add line 1612 source
theorem Weekday.Weekday.Hidden.add_comm line 1615 source
theorem Weekday.Weekday.Hidden.add_assoc line 1618 source
example Weekday.Weekday.(example at line 1637) line 1637 source
example Weekday.Weekday.(example at line 1655) line 1655 source
example Weekday.Weekday.(example at line 1666) line 1666 source
example Weekday.Weekday.(example at line 1670) line 1670 source
example Weekday.Weekday.(example at line 1691) line 1691 source
example Weekday.Weekday.(example at line 1708) line 1708 source
example Weekday.Weekday.(example at line 1711) line 1711 source
example Weekday.Weekday.(example at line 1714) line 1714 source
inductive Weekday.Weekday.foo line 1735 source
inductive Weekday.Weekday.Vect line 1756 source
inductive Weekday.Weekday.Hidden.Eq line 1772 source
Source comment
----
```
inductive Eq {α : Sort u} (a : α) : α → Prop where
…
```
Mentions: α
theorem Weekday.Weekday.Hidden.subst line 1813 source
Source comment
----
```
theorem subst {α : Type u} {a b : α} {p : α → Prop}
    (h₁ : Eq a b) (h₂ : p a) : p b :=
…
```
Mentions: α, b, Weekday.Weekday.Hidden.Eq
theorem Weekday.Weekday.Hidden.subst line 1825 source
Source comment
----
```
theorem subst {α : Type u} {a b : α} {p : α → Prop}
    (h₁ : Eq a b) (h₂ : p a) : p b :=
…
```
Mentions: α, b, Weekday.Weekday.Hidden.Eq
theorem Weekday.Weekday.subst line 1837 source
theorem Weekday.Weekday.Hidden.symm line 1864 source
theorem Weekday.Weekday.Hidden.trans sorry line 1868 source
theorem Weekday.Weekday.Hidden.congr sorry line 1871 source
inductive Weekday.Weekday.definitions, line 1879 source
inductive Weekday.Weekday.type line 1902 source
inductive Weekday.Weekday.types line 1909 source
inductive Weekday.Weekday.definitions line 1972 source
inductive Weekday.Tree line 2027 source
def Weekday.length line 2048 source
def Weekday.reverse line 2051 source
inductive Weekday.Term line 2058 source