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

86 declarations, 12 contain sorry, 0 declared as axioms

Imports (2)

VersoManual
TPiL.Examples

example (example at line 87) line 87 source
example (example at line 116) line 116 source
example (example at line 181) line 181 source
example (example at line 267) line 267 source
example (example at line 277) line 277 source
Source comment
----
```
example : a = d := (hab.trans hcb.symm).trans hcd
…
```
example (example at line 289) line 289 source
example (example at line 290) line 290 source
example (example at line 291) line 291 source
example (example at line 299) line 299 source
Source comment
----
```
example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl
```
Mentions: α, β, x
example (example at line 300) line 300 source
example (example at line 301) line 301 source
example (example at line 318) line 318 source
example (example at line 322) line 322 source
example (example at line 344) line 344 source
example (example at line 345) line 345 source
example (example at line 346) line 346 source
example (example at line 354) line 354 source
example (example at line 355) line 355 source
example (example at line 356) line 356 source
example (example at line 357) line 357 source
example (example at line 358) line 358 source
example (example at line 359) line 359 source
example (example at line 360) line 360 source
example (example at line 361) line 361 source
example (example at line 362) line 362 source
example (example at line 363) line 363 source
example (example at line 364) line 364 source
example (example at line 365) line 365 source
example (example at line 376) line 376 source
example (example at line 392) line 392 source
theorem T line 455 source

theorem T line 478 source

Source comment

----

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
…

Mentions: h1, b, h2

theorem T line 503 source

Source comment

----

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
…

Mentions: h1, b, h2

theorem T line 520 source

Source comment

----

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
…

Mentions: h1, b, h2

theorem T line 539 source

Source comment

----

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
…

Mentions: h1, b, h2

example (example at line 555) line 555 source
def divides line 568 source
def divides_trans Divisibility is transitive, so calc can chain it line 571 source
L4DEL explanation
Compose the two witnesses by multiplying them, which is the witness for the combined divisibility.
1. divides x y is defined as ∃ k, k*x = y.
2. let ⟨k₁, d₁⟩ := h₁ and let ⟨k₂, d₂⟩ := h₂ unpack the two witnesses and their equations.
3. The new witness is k₁ * k₂, and the equation is proved by rewriting with Nat.mul_comm, Nat.mul_assoc, d₁ and d₂.
4. The book uses it to build instance Trans divides divides divides, which teaches calc about this relation.
See also: divides_mul
Sources and attribution: Pinned Lean source (4e28129fdd58)
```
def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z :=
…
```
Mentions: divides, x
def divides_mul line 576 source
instance (instance at line 579) line 579 source
example (example at line 582) line 582 source
example (example at line 590) line 590 source
example (example at line 609) line 609 source
example (example at line 628) line 628 source
example (example at line 647) line 647 source
example (example at line 650) line 650 source
example (example at line 670) line 670 source
example (example at line 674) line 674 source
example (example at line 677) line 677 source
example (example at line 692) line 692 source
example (example at line 696) line 696 source
example (example at line 699) line 699 source
theorem gex1 line 722 source
theorem gex2 line 723 source
theorem gex3 line 724 source
theorem gex4 line 725 source
example (example at line 758) line 758 source
instance of line 784 source
Distinct definitions of this name: book/TPiL/StructuresAndRecords.lean:25 (different declaration text). Qualify references as of@path.
example (example at line 793) line 793 source
example (example at line 810) line 810 source
Source comment
----
```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
…
```
Mentions: x
example (example at line 820) line 820 source
Source comment
----
```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
…
```
Mentions: x
example (example at line 830) line 830 source
Source comment
----
```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
…
```
Mentions: x
example (example at line 842) line 842 source
Source comment
----
```
example : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x :=
…
```
Mentions: x
def IsEven line 851 source
def IsEven line 860 source
theorem even_plus_even line 862 source
def IsEven line 877 source

theorem even_plus_even line 879 source

Source comment

----

theorem even_plus_even (h1 : IsEven a) (h2 : IsEven b) :
    IsEven (a + b) :=
…

Mentions: h1, IsEven, h2, b

example (example at line 898) line 898 source
example (example at line 921) sorry line 921 source
example (example at line 922) sorry line 922 source
example (example at line 923) sorry line 923 source
example (example at line 924) sorry line 924 source
example (example at line 926) sorry line 926 source
example (example at line 927) sorry line 927 source
example (example at line 928) sorry line 928 source
example (example at line 929) sorry line 929 source
example (example at line 931) sorry line 931 source
example (example at line 932) sorry line 932 source
example (example at line 933) sorry line 933 source
example (example at line 948) line 948 source
example (example at line 959) line 959 source
example (example at line 998) line 998 source
example (example at line 1014) line 1014 source
Source comment
----
```
example : f 0 ≤ f 3 :=
…
```
example (example at line 1050) line 1050 source
example (example at line 1064) sorry line 1064 source