Metamatematico---Razonamiento-Formal-con-Lean

Lean 4 fundamentals including syntax, structures, inductive types, and polymorphism. Use when writing basic Lean code, defining custom data types, pattern matching, or learning core language patterns.

Dependent types for type-safe APIs and compile-time guarantees. Use for Vect, Fin, indexed families, universes, or making illegal states unrepresentable.

Functor, Applicative, Alternative, and the abstraction hierarchy. Use when transforming values in containers, combining independent computations, or choosing abstraction level.

Monadic effect handling in Lean including Option, Except, State, Reader, and do-notation. Use when chaining computations that may fail, need state, or require environment access.

Tail recursion, array mutation, Fin, and performance patterns. Use when optimizing recursive functions, avoiding stack overflow, or working with large data.

Combining multiple effects with monad transformers including StateT, ExceptT, ReaderT, and OptionT. Use when you need error handling AND state, or multiple effects together.

Ad-hoc polymorphism and operator overloading in Lean. Use when defining type classes, creating instances, implementing interfaces, deriving, or working with coercions.

Consolidated cheatsheets for Lean 4 syntax, tactics, type classes, monads, and common patterns. Use for quick lookup or when you need a reminder.

Axioms, classical logic, quotients, and noncomputable definitions. Use for excluded middle, proof by contradiction, quotient types, or understanding Lean's foundational axioms.

Dependent type theory fundamentals for theorem proving. Use when understanding universes, Type/Prop, dependent types, or the Calculus of Constructions foundation.

Curry-Howard correspondence and logical connectives. Use when constructing proofs, understanding proof terms, or working with And/Or/Not/implication.

Universal/existential quantifiers and equality reasoning. Use when proving forall/exists, equational reasoning with rfl, calc chains, or substitution.

Decision trees for choosing tactics based on goal type and proof strategy. Use when unsure which tactic to apply or planning proof approach.

Core tactics for theorem proving including apply, exact, intro, rw, simp, cases, and induction. Use when constructing proofs step-by-step in tactic mode.