NathanHowell · September 27, 2025 18:40
diff --git a/COMBINED b/COMBINED
 🦾 Lean4 — ultra-condensed ref

 🧠 Core: dep-TT (CIC); pure/strict FP; Curry–Howard; Sorts `Prop`/`Type u`/`Sort u`; Prop impredicative & proof-irrelevant; pipeline parse→macro→elab(cmd/term/tac)→kernel→IR/native; InfoTree/InfoView; Pratt parser; term-style vs `by` tactic-style.
 🔤 Univ: levels u v w; `max/imax/succ`; cumulativity (Sort u↪Sort u+1); `Prop = Sort 0`; `Type u = Sort (u+1)`; Π typing→`Sort (imax i j)`; universe params `.{u}`; defeq β δ ζ ι η.
 ⛳ Binders & implicits: `(x:α)` explicit; `{x}` implicit; `⦃x⦄` strict-implicit; `[x:α]` instance-implicit; `_`/`?m` holes; casts `(e : T)`; `@f` exposes implicits; section/`variable` params auto-insert; implicit lambdas & named args.
 🏗 Decls & recursion: `def`/`abbrev`/`opaque`/`theorem`/`lemma`/`example`/`axiom`; `unsafe`/`partial`/`noncomputable`; pattern-matching; structural & well-founded (`WellFounded.fix`) recursion; `mutual`; equation compiler; `termination_by`/`decreasing_by`/`wfRel`; `where` locals.
 📦 Modules & scope: file `A/B/C.lean`≡`A.B.C`; `prelude`; `import`; `namespace`/`section`; `_root_`/`protected`/`private` (hashed `_private`)/`export`/`alias`; `open`/`open scoped`/`localized`; `initialize`/`run_cmd`; `set_option …` & `trace.*` (e.g., `trace.class_instances`, `trace.simp`).
 ✍️ Terms: `λ`/`Π`/`∀`; `let`/`where`; `if`/`match`/`dite`; numerals via `OfNat`/`OfInt`/`OfScientific`; mutual defs; dot-notation & leading `.ctor`; `show` annotations.
 🧱 Inductives & records: inductive families/enums; recursors `casesOn`/`rec`; positivity; nested/mutual; `structure`→ctor/projections/recursor; deriving `Repr` `DecidableEq` `Inhabited` `BEq` `Hashable` `Ord`; object literal `{ … }`; record update `{ s with fld := v }`.
 📚 Types & data: `Nat` `Int` `UInt*` `USize` `BitVec` `Float` `Char` `String`; `Prod` (`α × β`, `.fst/.snd`) `Sum` `Sigma` `Subtype`; `Option` `Except` `List` `Array` `RBMap` `HashMap` `Fin`.
 🧩 Typeclasses & coercions: `class`/`instance`/`deriving instance`; search via `inferInstance`; `local instance`; priorities; numeric/ordering via classes (`OfNat`, `HAdd`, …); `Coe`/`CoeFun`/`CoeSort`/`CoeHead`/`CoeTail`/`CoeTrans`/`CoeSub`.
 ⚖ Eq & rewrite: `=`/`rfl`; `Eq.refl/symm/trans`; `congrArg`; `Eq.rec`/`Eq.subst`; `HEq`; `rw`/`rw ←`/`▸`; `calc`; `Subtype {x // p}`; `Sigma ⟨v,p⟩`.
 🔢 Logic: `True`/`False`; `¬ ∧ ∨ → ↔`; `∀`/`∃` (`Exists.intro`/`cases`); `Decidable p`; constructive core; classical via `open Classical`; `noncomputable` when extracting data.
 🛠 Tactics: `intro[s]/refine/apply/exact/have/rename/generalize/subst`; `constructor/cases/cases’/induction/split/left/right/exists/use/by_cases/by_contra`; `rw`/`nth_rewrite`; `simp`/`simp_all`/`dsimp`; `change/convert/symm/trans`; `injection`; `ac_nf`; `solve_by_elim`; `contrapose/exfalso/trivial/contradiction`; control `first|` `all_goals` `any_goals` `focus` `repeat` `try` `<;>` `case`; `conv`; `calc`.
 🧹 Simplifier: `[simp]`-driven; `simp`/`simp at *`; `simp [defs]`/`simp only [l*]`/`simp [← l]`; `[local simp]`; `simp?`; tracing & configs (e.g., `contextual:=true`); avoid loops via priorities; propositional simp (∧/∨/↔).
 🔣 Syntax & macros: `syntax`/`notation`/mixfix; `macro`/`macro_rules`; `elab` (term/command/tactic); scoped/localized notation; quoting `` `(…) `` with antiquotations; hygiene; pretty-printing.
 📦 Monads & `do`: `Functor`/`Applicative`/`Monad`; transformers `ReaderT` `StateT` `ExceptT` `OptionT` `WriterT`; `Alternative`/`ForIn`; `do` sugar (`let`/`match`/`if`/`for`/`while`/`try`/`catch`/`finally`); `guard`; nested actions `← e`; early return; `mut`.
 🖥 IO & conc: `IO`/`EIO`; `def main : IO Unit` (or `IO UInt32`); FS `IO.FS`/`System.FilePath`; `IO.getStdin/Stdout/Stderr`; `Process.spawn`; `Task`/`Ref`/`MVar`; `IO.asTask/await/sleep`; `IO.toEIO`.
 ⚙ Runtime/FFI/build: RC+boxing (scalars unboxed); multi-threaded; `@[extern]`/`@[export]`/`@[inline|noinline]`; Lake (`package`/`lean_lib`/`lean_exe`/`lean_shared`; `require`; `build`/`update`/`exe`/`env`/`test`); Elan toolchains.
 🏷 Attr: `[simp]` `[ext]` `[reassoc]` `[congr]` `[inline|noinline]` `[reducible|semireducible|irreducible]` `[priority:=n]` `[deprecated]` `[export]`.
 🧪 Commands & tracing: `#check` `#print` `#eval` (VM) `#reduce` (kernel) `#simp`/`#simp?` `#synth` `#guard`/`#guard_hyp` `#guard_msgs` `#help`; `unfold`; `decide` to discharge decidable goals; `set_option`/`trace.*` for pp/instances/simp/unification.
 🧭 Debug & errors: message classes parse/scope/elab/kernel/termination/macro/tactic; editor goal panes; `#print` artifacts; `#guard_msgs` to assert diagnostics.
 ✅ Tips: use `abbrev` for aliases; `opaque` to hide impl; keep instances local/scoped; tune priorities sparingly; directional `[simp]` lemmas; add `termination_by` early; prefer class-based numerals; keep term-style when simple; isolate classical with `local open Classical`; prefer `Fin`/subtypes for bounds; safe indexing `a[i]?`/`a[i]!`/`a[i]'h`.
 ➕ Extras: `conv` mode (navigate/lhs/rhs/`congr`/`intro`/pattern-rewrite); axioms `funext` `propext` `Choice` & `Quot`; `noncomputable` data via choice; `#reduce` vs `#eval` differences (casts/extensionality can block kernel eval); Unicode input via `\alpha`, `→`.
diff --git a/FPiL b/FPiL
 🦾 Lean4 — ultra-condensed ref (FPiL4)

 🧠 Core: dep-TT; strict/pure FP; univ Prop/Type u; editor-integrated feedback; tools elan (toolchains)/lake (build/deps)/lean (check/compile); interactive #eval; batch build & run executables.
 🔤 Univ: universe-polymorphism; Type u towers; Prop : Type; universe params in defs; indices/parameters with levels (see “Universes” & “Indices, Parameters, and Universe Levels”).
 ⛳ Binders: (x:α) explicit; {x} implicit; [x:α] instance-implicit; holes _/metavars ?m.
 🏗 Decls: def/theorem/structure/inductive/instance; partial for non-structural recursion; mutual/where; termination hints termination_by/decreasing_by when automation needs help.
 📦 Modules&Scope: file↔module; import libs; multi-file projects via Lake; open namespaces when convenient.
 ✍️ Terms: λ/functions; numerals via OfNat/OfInt; structure fields; deriving instances (Repr/BEq/Hashable/DecidableEq/Ord); inductive + match; if … then … else …; let/where; leading .ctor & dot-syntax; parametric polymorphism.
 ⚖ Eq: = as Prop; rfl; rw/rw ← rewrite by equalities; unfold expands defs; calc chains steps.
 🔢 Logic: True/False/¬/∧/∨/→; evidence via constructors (And.intro/Or.inl/Or.inr); implication as functions; decide discharges decidable goals.
 🧪 Commands: #check show types; #eval run terms.
 🧩 Typeclasses&Coercions: class/instance/deriving; instance search powers overloading; coercions via Coe/CoeFun/CoeSort; chained coercions (e.g., Pos → Nat → Int).
 🛠 Tactics: by blocks; induction (with | zero | succ n ih); rfl/rw/unfold/simp/calc; tactics transform goals while elaborating proofs.
 🧹 Simplifier: simp rewrites using known lemmas/defs; often solves goals outright (hides low-level proof steps).
 📦 Monads&do: Functor/Applicative/Monad; transformers ReaderT/StateT/ExceptT/OptionT/WriterT; do sugar for bind/let/match/if; extras: nested actions (← e), early return, loops (for/while), mutable let mut.
 🖥 IO&Conc: IO programs; main : IO Unit or IO UInt32; IO.getStdin/Stdout/Stderr; files via System.FilePath, IO.FS.Handle/Stream, pathExists/readDir; partial recursion over IO when needed.
 ⚙ Runtime/FFI/Build: Lake builds packages/exes & manages deps; elan installs/switches toolchains; compile & lake run to execute.
 📚 Types: Nat/Int/UInt8/16/32/64/USize/BitVec/Float/Char/String; products/sums Prod/Sum; Option/Except/List/Array; subtypes Subtype; bounded Fin n.
 🧭 Debug&Errors: rich editor messages (unsolved goals, pattern/arity hints); safe indexing requires proofs i < a.size; variants: a[i]? (Option)/a[i]! (runtime check)/a[i]'h (with proof).
 ✅ Tips: use deriving to avoid boilerplate; keep effects at the edges (core pure); prefer Fin/subtypes to encode bounds/invariants and drop runtime checks; add termination_by early for non-structural recursions; lean on simp/decide for arithmetic/indexing; compose effects with transformers, expose IO at main.
 ➕ Extras: nested actions (← e); single-branched if in do; Option/checked indexing xs[n]?/xs[n]!; Unicode input via backslash names (\alpha, →); Lake quickstart for multi-file apps.
diff --git a/REF b/REF
 🦾 Lean4 — ultra‑condensed ref

 🧠 Core: dep‑TT; Sorts Prop/Type u/Sort u; pipeline parse→macro→elab(cmd/term/tac)→kernel→IR/native; InfoTree; Pratt parser.
 🔤 Univ: levels u v w; ops max/imax/succ; cumulativity; defeq β,δ,ζ,ι,η.
 ⛳ Binders: (x:α) explicit; {x} implicit; ⦃x⦄ strict‑implicit; [x:α] instance; (x:=t) default; (x:=by tac) autoParam.
 🏗 Decls: def/abbrev/opaque/theorem/lemma/example/axiom; unsafe/partial/noncomputable/(section); termination_by/decreasing_by/wfRel.
 🏷 Attr: [simp]/simp? [ext] [reassoc] [congr] [inline|noinline] [reducible|semireducible|irreducible] [priority:=n] [deprecated] [export].
 📦 Modules&Scope: A/B/C.lean≡A.B.C; prelude; import; namespace/section; private/protected/export (private hashed=_private); alias/export; open/ open scoped; localized; initialize; run_cmd; set_option & trace.* (e.g. trace.class_instances, trace.simp).
 ✍️ Terms: λ fun; Π/∀; holes _ ?m; numerals via OfNat/OfInt/OfScientific; structure/inductive deriving Repr DecidableEq Inhabited BEq Hashable Ord; match/if/dite; let/where; mutual; dot field & leading .ctor.
 ⚖ Eq: rfl; (=); Eq.rec; HEq; Subtype {x // p}; Sigma ⟨v,p⟩; calc; rw/←.
 🔢 Logic: True/False; ¬ ∧ ∨ → ↔; ∀ ∃; Decidable p; open Classical; noncomputable.
 🧪 Tools: #check #eval #reduce #simp #simp? #print #synth #guard #guard_hyp #guard_msgs #help.
 🧩 Classes&Coe: class/instance/deriving instance; inferInstance; local instance; priority; Coe/CoeFun/CoeSort/CoeTail/CoeHead/CoeTrans/CoeSub.
 🛠 Tactics: intro/intros/refine/apply/exact/have/rename/generalize/subst; cases/cases’/induction/constructor/split/left/right/exists/use/by_cases/by_contra; rw/nth_rewrite; simp/simp_all/dsimp; change/convert/symm/trans; injection; ac_nf; solve_by_elim; contrapose/exfalso/trivial/contradiction; control: first| all_goals any_goals focus repeat try <;> case; conv; calc.
 🧹 Simp: driven by [simp]; simp [defs]; simp only [l*]; simp at *; simp [← l]; simp?; tracing; config (e.g. contextual:=true); avoid loops via priorities.
 📦 Monads&do: Functor/Applicative/Monad; transformers ReaderT StateT ExceptT OptionT WriterT; Alternative/ForIn; do sugar (let/match/if/for/while/try/catch/finally); guard.
 🖥 IO&Conc: IO/EIO; def main : IO Unit; FS IO.FS; Process.spawn; Task/Ref/MVar; IO.asTask/await/sleep; IO.toEIO.
 🔣 Syntax&Macros: syntax/notation/mixfix; macro/macro_rules; elab (term/command/tactic); scoped/localized notation; quoting `(…) with antiquotations; hygiene; pretty‑printing.
 ⚙ Runtime&FFI&Build: RC+boxing (scalars unboxed); multi‑threaded; @[extern]/@[export]/@[inline]; Lake (package/lean_lib/lean_exe/lean_shared, require; build/update/exe/env/test); Elan.
 📚 Types: Nat Int UInt* USize BitVec Float Char String; Prod Sum Sigma Subtype; Option Except List Array RBMap HashMap Fin.
 🧭 Debug&Errors: InfoView; error classes parse/scope/elab/kernel/termination/macro/tactic; set_option + trace.* to diagnose (instances/simp/unification).
 ✅ Tips: use abbrev for aliases; opaque to hide impl; keep instances local/scoped; tune priorities sparingly; directional [simp] lemmas; add termination_by early; prefer class‑based numerals.
diff --git a/TPiL b/TPiL
 🦾 Lean4 — ultra‑condensed ref (TPiL4)

 🧠 Core: dep‑TT (CIC); universes non‑cumulative; Prop impredicative & proof‑irrelevant; Curry‑Howard (terms‑as‑proofs); def≃theorem to kernel; term‑style vs tactic‑style (by …); rewriting via rw/▸/calc; messages: error/warning/info; #guard_msgs to assert expected msgs.
 🔤 Univ: Prop = Sort 0; Type u = Sort (u+1); universe polymorphism .{u}; typing of Π/∀: (x:α:Sort i)→β x:Sort (imax i j); impredicativity: ∀ x:α, p x : Prop when p:α→Prop.
 ⛳ Binders & implicits: (x:α)/∀; {x} implicit; [C α] instance‑implicit; _/?m placeholders; (e : T) casts; @f exposes implicits; variable/section insert params.
 🏗 Decls: def (data), theorem/lemma/example (proofs, irreducible); axiom (use sparingly); pattern matching match; recursion: structural / well‑founded (WellFounded.fix) / mutual; where/local defs.
 📦 Scope: import; namespace … end; section … end; open (aliases/selected names); _root_/protected; export to make aliases; names are hierarchical.
 ✍️ Terms: λ/fun; Π/∀; products/pairs, ×, Prod.snd/.fst; let; show annotations; calc chains; dot‑notation on records & names; numeric literals via typeclasses.
 ⚖ Eq & rewrite: rfl; Eq.refl/symm/trans; congrArg; Eq.rec/Eq.subst; rewrite rw [h]/rw [←h]/h ▸ …; calc chains.
 🔢 Logic: True/False; ¬ ∧ ∨ → ↔; ∀ ∃; Exists.intro/cases; by_cases/by_contra; constructive core; classical via open Classical/LEM.
 🧪 Commands: #check/#print/#eval (VM) /#reduce (kernel) /#guard_msgs; set_option … to tweak pp/behavior.
 🧩 Typeclasses & coercions: class/instance; instance search & chaining; inferInstance; local/scoped instances; standard numeric/ordering ops via classes (OfNat, HAdd, …); coercions & notation configured in library; Coee style coercions and export helpers.
 🛠 Tactics: intro/apply/exact/refine/have; constructor/cases/induction; left/right/exists/use; by_cases/by_contra; rw/nth_rewrite; simp/dsimp; change/convert; combinators ; <;> first | case bullets.
 🧹 Simplifier: uses [simp] lemmas; simp/simp at h*; simp [defs]/simp only [l*]/simp [← l]; [local simp] via attribute; ordered rewriting avoids loops; propositional simp (∧/∨/↔).
 🧱 Inductives: enums/ctors; inductively defined props; recursors casesOn/rec; positivity restriction; mutual & nested inductives; inductive families.
 🔁 Induction & recursion: pattern matching; wildcards & overlapping patterns (first match wins); dependent pattern matching; functional induction; well‑founded recursion; equation compiler (patterns→recursors).
 🏗 Structures & records: structure generates ctor/projections/recursor; inheritance/parents; object literals { … }; record update { s with fld := v }; dot‑notation methods.
 🧭 Interacting with Lean: importing files; sections/namespaces details; attributes; notation/coercions; displaying info; Auto Bound Implicit, implicit lambdas, named args.
 📚 Builtins: Nat/Int/Bool/String/List/Option/Prod/Sum (+ Sigma, etc.).
 🧭 Debug: message classes; inspect goals in editors; #print artifacts; use set_option to control traces in examples.
 ✅ Tips: keep proofs term‑style when simple; use calc + rw/simp for equational work; craft [simp] lemmas directionally; keep instances minimal/local; prefer Exists.intro/cases for ∃; isolate classical with local open Classical.
 ➕ Extras: conv mode (navigate/lhs/rhs/congr/intro/pattern‑rewrite); axioms: propext (propositional ext.), funext (from Quot), Quot (quotients), Choice; noncomputable when producing data from existence; #reduce vs #eval divergence when casts/extensionality block kernel eval.
	🦾 Lean4 — ultra-condensed ref

	🧠 Core: dep-TT (CIC); pure/strict FP; Curry–Howard; Sorts `Prop`/`Type u`/`Sort u`; Prop impredicative & proof-irrelevant; pipeline parse→macro→elab(cmd/term/tac)→kernel→IR/native; InfoTree/InfoView; Pratt parser; term-style vs `by` tactic-style.
	🔤 Univ: levels u v w; `max/imax/succ`; cumulativity (Sort u↪Sort u+1); `Prop = Sort 0`; `Type u = Sort (u+1)`; Π typing→`Sort (imax i j)`; universe params `.{u}`; defeq β δ ζ ι η.
	⛳ Binders & implicits: `(x:α)` explicit; `{x}` implicit; `⦃x⦄` strict-implicit; `[x:α]` instance-implicit; `_`/`?m` holes; casts `(e : T)`; `@f` exposes implicits; section/`variable` params auto-insert; implicit lambdas & named args.
	🏗 Decls & recursion: `def`/`abbrev`/`opaque`/`theorem`/`lemma`/`example`/`axiom`; `unsafe`/`partial`/`noncomputable`; pattern-matching; structural & well-founded (`WellFounded.fix`) recursion; `mutual`; equation compiler; `termination_by`/`decreasing_by`/`wfRel`; `where` locals.
	📦 Modules & scope: file `A/B/C.lean`≡`A.B.C`; `prelude`; `import`; `namespace`/`section`; `_root_`/`protected`/`private` (hashed `_private`)/`export`/`alias`; `open`/`open scoped`/`localized`; `initialize`/`run_cmd`; `set_option …` & `trace.*` (e.g., `trace.class_instances`, `trace.simp`).
	✍️ Terms: `λ`/`Π`/`∀`; `let`/`where`; `if`/`match`/`dite`; numerals via `OfNat`/`OfInt`/`OfScientific`; mutual defs; dot-notation & leading `.ctor`; `show` annotations.
	🧱 Inductives & records: inductive families/enums; recursors `casesOn`/`rec`; positivity; nested/mutual; `structure`→ctor/projections/recursor; deriving `Repr` `DecidableEq` `Inhabited` `BEq` `Hashable` `Ord`; object literal `{ … }`; record update `{ s with fld := v }`.
	📚 Types & data: `Nat` `Int` `UInt*` `USize` `BitVec` `Float` `Char` `String`; `Prod` (`α × β`, `.fst/.snd`) `Sum` `Sigma` `Subtype`; `Option` `Except` `List` `Array` `RBMap` `HashMap` `Fin`.
	🧩 Typeclasses & coercions: `class`/`instance`/`deriving instance`; search via `inferInstance`; `local instance`; priorities; numeric/ordering via classes (`OfNat`, `HAdd`, …); `Coe`/`CoeFun`/`CoeSort`/`CoeHead`/`CoeTail`/`CoeTrans`/`CoeSub`.
	⚖ Eq & rewrite: `=`/`rfl`; `Eq.refl/symm/trans`; `congrArg`; `Eq.rec`/`Eq.subst`; `HEq`; `rw`/`rw ←`/`▸`; `calc`; `Subtype {x // p}`; `Sigma ⟨v,p⟩`.
	🔢 Logic: `True`/`False`; `¬ ∧ ∨ → ↔`; `∀`/`∃` (`Exists.intro`/`cases`); `Decidable p`; constructive core; classical via `open Classical`; `noncomputable` when extracting data.
	🛠 Tactics: `intro[s]/refine/apply/exact/have/rename/generalize/subst`; `constructor/cases/cases’/induction/split/left/right/exists/use/by_cases/by_contra`; `rw`/`nth_rewrite`; `simp`/`simp_all`/`dsimp`; `change/convert/symm/trans`; `injection`; `ac_nf`; `solve_by_elim`; `contrapose/exfalso/trivial/contradiction`; control `first\|` `all_goals` `any_goals` `focus` `repeat` `try` `<;>` `case`; `conv`; `calc`.
	🧹 Simplifier: `[simp]`-driven; `simp`/`simp at `; `simp [defs]`/`simp only [l]`/`simp [← l]`; `[local simp]`; `simp?`; tracing & configs (e.g., `contextual:=true`); avoid loops via priorities; propositional simp (∧/∨/↔).
	🔣 Syntax & macros: `syntax`/`notation`/mixfix; `macro`/`macro_rules`; `elab` (term/command/tactic); scoped/localized notation; quoting `` `(…) `` with antiquotations; hygiene; pretty-printing.
	📦 Monads & `do`: `Functor`/`Applicative`/`Monad`; transformers `ReaderT` `StateT` `ExceptT` `OptionT` `WriterT`; `Alternative`/`ForIn`; `do` sugar (`let`/`match`/`if`/`for`/`while`/`try`/`catch`/`finally`); `guard`; nested actions `← e`; early return; `mut`.
	🖥 IO & conc: `IO`/`EIO`; `def main : IO Unit` (or `IO UInt32`); FS `IO.FS`/`System.FilePath`; `IO.getStdin/Stdout/Stderr`; `Process.spawn`; `Task`/`Ref`/`MVar`; `IO.asTask/await/sleep`; `IO.toEIO`.
	⚙ Runtime/FFI/build: RC+boxing (scalars unboxed); multi-threaded; `@[extern]`/`@[export]`/`@[inline\|noinline]`; Lake (`package`/`lean_lib`/`lean_exe`/`lean_shared`; `require`; `build`/`update`/`exe`/`env`/`test`); Elan toolchains.
	🏷 Attr: `[simp]` `[ext]` `[reassoc]` `[congr]` `[inline\|noinline]` `[reducible\|semireducible\|irreducible]` `[priority:=n]` `[deprecated]` `[export]`.
	🧪 Commands & tracing: `#check` `#print` `#eval` (VM) `#reduce` (kernel) `#simp`/`#simp?` `#synth` `#guard`/`#guard_hyp` `#guard_msgs` `#help`; `unfold`; `decide` to discharge decidable goals; `set_option`/`trace.*` for pp/instances/simp/unification.
	🧭 Debug & errors: message classes parse/scope/elab/kernel/termination/macro/tactic; editor goal panes; `#print` artifacts; `#guard_msgs` to assert diagnostics.
	✅ Tips: use `abbrev` for aliases; `opaque` to hide impl; keep instances local/scoped; tune priorities sparingly; directional `[simp]` lemmas; add `termination_by` early; prefer class-based numerals; keep term-style when simple; isolate classical with `local open Classical`; prefer `Fin`/subtypes for bounds; safe indexing `a[i]?`/`a[i]!`/`a[i]'h`.
	➕ Extras: `conv` mode (navigate/lhs/rhs/`congr`/`intro`/pattern-rewrite); axioms `funext` `propext` `Choice` & `Quot`; `noncomputable` data via choice; `#reduce` vs `#eval` differences (casts/extensionality can block kernel eval); Unicode input via `\alpha`, `→`.
	🦾 Lean4 — ultra-condensed ref (FPiL4)

	🧠 Core: dep-TT; strict/pure FP; univ Prop/Type u; editor-integrated feedback; tools elan (toolchains)/lake (build/deps)/lean (check/compile); interactive #eval; batch build & run executables.
	🔤 Univ: universe-polymorphism; Type u towers; Prop : Type; universe params in defs; indices/parameters with levels (see “Universes” & “Indices, Parameters, and Universe Levels”).
	⛳ Binders: (x:α) explicit; {x} implicit; [x:α] instance-implicit; holes _/metavars ?m.
	🏗 Decls: def/theorem/structure/inductive/instance; partial for non-structural recursion; mutual/where; termination hints termination_by/decreasing_by when automation needs help.
	📦 Modules&Scope: file↔module; import libs; multi-file projects via Lake; open namespaces when convenient.
	✍️ Terms: λ/functions; numerals via OfNat/OfInt; structure fields; deriving instances (Repr/BEq/Hashable/DecidableEq/Ord); inductive + match; if … then … else …; let/where; leading .ctor & dot-syntax; parametric polymorphism.
	⚖ Eq: = as Prop; rfl; rw/rw ← rewrite by equalities; unfold expands defs; calc chains steps.
	🔢 Logic: True/False/¬/∧/∨/→; evidence via constructors (And.intro/Or.inl/Or.inr); implication as functions; decide discharges decidable goals.
	🧪 Commands: #check show types; #eval run terms.
	🧩 Typeclasses&Coercions: class/instance/deriving; instance search powers overloading; coercions via Coe/CoeFun/CoeSort; chained coercions (e.g., Pos → Nat → Int).
	🛠 Tactics: by blocks; induction (with \| zero \| succ n ih); rfl/rw/unfold/simp/calc; tactics transform goals while elaborating proofs.
	🧹 Simplifier: simp rewrites using known lemmas/defs; often solves goals outright (hides low-level proof steps).
	📦 Monads&do: Functor/Applicative/Monad; transformers ReaderT/StateT/ExceptT/OptionT/WriterT; do sugar for bind/let/match/if; extras: nested actions (← e), early return, loops (for/while), mutable let mut.
	🖥 IO&Conc: IO programs; main : IO Unit or IO UInt32; IO.getStdin/Stdout/Stderr; files via System.FilePath, IO.FS.Handle/Stream, pathExists/readDir; partial recursion over IO when needed.
	⚙ Runtime/FFI/Build: Lake builds packages/exes & manages deps; elan installs/switches toolchains; compile & lake run to execute.
	📚 Types: Nat/Int/UInt8/16/32/64/USize/BitVec/Float/Char/String; products/sums Prod/Sum; Option/Except/List/Array; subtypes Subtype; bounded Fin n.
	🧭 Debug&Errors: rich editor messages (unsolved goals, pattern/arity hints); safe indexing requires proofs i < a.size; variants: a[i]? (Option)/a[i]! (runtime check)/a[i]'h (with proof).
	✅ Tips: use deriving to avoid boilerplate; keep effects at the edges (core pure); prefer Fin/subtypes to encode bounds/invariants and drop runtime checks; add termination_by early for non-structural recursions; lean on simp/decide for arithmetic/indexing; compose effects with transformers, expose IO at main.
	➕ Extras: nested actions (← e); single-branched if in do; Option/checked indexing xs[n]?/xs[n]!; Unicode input via backslash names (\alpha, →); Lake quickstart for multi-file apps.
	🦾 Lean4 — ultra‑condensed ref

	🧠 Core: dep‑TT; Sorts Prop/Type u/Sort u; pipeline parse→macro→elab(cmd/term/tac)→kernel→IR/native; InfoTree; Pratt parser.
	🔤 Univ: levels u v w; ops max/imax/succ; cumulativity; defeq β,δ,ζ,ι,η.
	⛳ Binders: (x:α) explicit; {x} implicit; ⦃x⦄ strict‑implicit; [x:α] instance; (x:=t) default; (x:=by tac) autoParam.
	🏗 Decls: def/abbrev/opaque/theorem/lemma/example/axiom; unsafe/partial/noncomputable/(section); termination_by/decreasing_by/wfRel.
	🏷 Attr: [simp]/simp? [ext] [reassoc] [congr] [inline\|noinline] [reducible\|semireducible\|irreducible] [priority:=n] [deprecated] [export].
	📦 Modules&Scope: A/B/C.lean≡A.B.C; prelude; import; namespace/section; private/protected/export (private hashed=_private); alias/export; open/ open scoped; localized; initialize; run_cmd; set_option & trace.* (e.g. trace.class_instances, trace.simp).
	✍️ Terms: λ fun; Π/∀; holes _ ?m; numerals via OfNat/OfInt/OfScientific; structure/inductive deriving Repr DecidableEq Inhabited BEq Hashable Ord; match/if/dite; let/where; mutual; dot field & leading .ctor.
	⚖ Eq: rfl; (=); Eq.rec; HEq; Subtype {x // p}; Sigma ⟨v,p⟩; calc; rw/←.
	🔢 Logic: True/False; ¬ ∧ ∨ → ↔; ∀ ∃; Decidable p; open Classical; noncomputable.
	🧪 Tools: #check #eval #reduce #simp #simp? #print #synth #guard #guard_hyp #guard_msgs #help.
	🧩 Classes&Coe: class/instance/deriving instance; inferInstance; local instance; priority; Coe/CoeFun/CoeSort/CoeTail/CoeHead/CoeTrans/CoeSub.
	🛠 Tactics: intro/intros/refine/apply/exact/have/rename/generalize/subst; cases/cases’/induction/constructor/split/left/right/exists/use/by_cases/by_contra; rw/nth_rewrite; simp/simp_all/dsimp; change/convert/symm/trans; injection; ac_nf; solve_by_elim; contrapose/exfalso/trivial/contradiction; control: first\| all_goals any_goals focus repeat try <;> case; conv; calc.
	🧹 Simp: driven by [simp]; simp [defs]; simp only [l]; simp at ; simp [← l]; simp?; tracing; config (e.g. contextual:=true); avoid loops via priorities.
	📦 Monads&do: Functor/Applicative/Monad; transformers ReaderT StateT ExceptT OptionT WriterT; Alternative/ForIn; do sugar (let/match/if/for/while/try/catch/finally); guard.
	🖥 IO&Conc: IO/EIO; def main : IO Unit; FS IO.FS; Process.spawn; Task/Ref/MVar; IO.asTask/await/sleep; IO.toEIO.
	🔣 Syntax&Macros: syntax/notation/mixfix; macro/macro_rules; elab (term/command/tactic); scoped/localized notation; quoting `(…) with antiquotations; hygiene; pretty‑printing.
	⚙ Runtime&FFI&Build: RC+boxing (scalars unboxed); multi‑threaded; @[extern]/@[export]/@[inline]; Lake (package/lean_lib/lean_exe/lean_shared, require; build/update/exe/env/test); Elan.
	📚 Types: Nat Int UInt* USize BitVec Float Char String; Prod Sum Sigma Subtype; Option Except List Array RBMap HashMap Fin.
	🧭 Debug&Errors: InfoView; error classes parse/scope/elab/kernel/termination/macro/tactic; set_option + trace.* to diagnose (instances/simp/unification).
	✅ Tips: use abbrev for aliases; opaque to hide impl; keep instances local/scoped; tune priorities sparingly; directional [simp] lemmas; add termination_by early; prefer class‑based numerals.
	🦾 Lean4 — ultra‑condensed ref (TPiL4)

	🧠 Core: dep‑TT (CIC); universes non‑cumulative; Prop impredicative & proof‑irrelevant; Curry‑Howard (terms‑as‑proofs); def≃theorem to kernel; term‑style vs tactic‑style (by …); rewriting via rw/▸/calc; messages: error/warning/info; #guard_msgs to assert expected msgs.
	🔤 Univ: Prop = Sort 0; Type u = Sort (u+1); universe polymorphism .{u}; typing of Π/∀: (x:α:Sort i)→β x:Sort (imax i j); impredicativity: ∀ x:α, p x : Prop when p:α→Prop.
	⛳ Binders & implicits: (x:α)/∀; {x} implicit; [C α] instance‑implicit; _/?m placeholders; (e : T) casts; @f exposes implicits; variable/section insert params.
	🏗 Decls: def (data), theorem/lemma/example (proofs, irreducible); axiom (use sparingly); pattern matching match; recursion: structural / well‑founded (WellFounded.fix) / mutual; where/local defs.
	📦 Scope: import; namespace … end; section … end; open (aliases/selected names); _root_/protected; export to make aliases; names are hierarchical.
	✍️ Terms: λ/fun; Π/∀; products/pairs, ×, Prod.snd/.fst; let; show annotations; calc chains; dot‑notation on records & names; numeric literals via typeclasses.
	⚖ Eq & rewrite: rfl; Eq.refl/symm/trans; congrArg; Eq.rec/Eq.subst; rewrite rw [h]/rw [←h]/h ▸ …; calc chains.
	🔢 Logic: True/False; ¬ ∧ ∨ → ↔; ∀ ∃; Exists.intro/cases; by_cases/by_contra; constructive core; classical via open Classical/LEM.
	🧪 Commands: #check/#print/#eval (VM) /#reduce (kernel) /#guard_msgs; set_option … to tweak pp/behavior.
	🧩 Typeclasses & coercions: class/instance; instance search & chaining; inferInstance; local/scoped instances; standard numeric/ordering ops via classes (OfNat, HAdd, …); coercions & notation configured in library; Coee style coercions and export helpers.
	🛠 Tactics: intro/apply/exact/refine/have; constructor/cases/induction; left/right/exists/use; by_cases/by_contra; rw/nth_rewrite; simp/dsimp; change/convert; combinators ; <;> first \| case bullets.
	🧹 Simplifier: uses [simp] lemmas; simp/simp at h; simp [defs]/simp only [l]/simp [← l]; [local simp] via attribute; ordered rewriting avoids loops; propositional simp (∧/∨/↔).
	🧱 Inductives: enums/ctors; inductively defined props; recursors casesOn/rec; positivity restriction; mutual & nested inductives; inductive families.
	🔁 Induction & recursion: pattern matching; wildcards & overlapping patterns (first match wins); dependent pattern matching; functional induction; well‑founded recursion; equation compiler (patterns→recursors).
	🏗 Structures & records: structure generates ctor/projections/recursor; inheritance/parents; object literals { … }; record update { s with fld := v }; dot‑notation methods.
	🧭 Interacting with Lean: importing files; sections/namespaces details; attributes; notation/coercions; displaying info; Auto Bound Implicit, implicit lambdas, named args.
	📚 Builtins: Nat/Int/Bool/String/List/Option/Prod/Sum (+ Sigma, etc.).
	🧭 Debug: message classes; inspect goals in editors; #print artifacts; use set_option to control traces in examples.
	✅ Tips: keep proofs term‑style when simple; use calc + rw/simp for equational work; craft [simp] lemmas directionally; keep instances minimal/local; prefer Exists.intro/cases for ∃; isolate classical with local open Classical.
	➕ Extras: conv mode (navigate/lhs/rhs/congr/intro/pattern‑rewrite); axioms: propext (propositional ext.), funext (from Quot), Quot (quotients), Choice; noncomputable when producing data from existence; #reduce vs #eval divergence when casts/extensionality block kernel eval.