Blueprint Used-By Preview Wiring

 Blueprint Used-By Preview Wiring🔗

Compiled2026-07-01T21:39:42ZProject5f17f8aMerge pull request #222 from leanprover/chore/reference-blueprints-catalog-all-v4.30.0-v4.31.0Leanleanprover/lean4:v4.31.0VersoBlueprint5f17f8a
Definition3
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Target statement with associated Lean code.

Lean code for Definition3def usedByPreviewTarget : Nat := 0
Lemma4
uses 1used by 0XL∃∀N

Statement depends on Definition 3.

Theorem5
uses 0used by 0XL∃∀N

Separate theorem with a proof-only dependency.

Proof for Theorem 5
uses 1

Proof depends on Definition 3.