Theorem Proving in Lean 4 Theorem Proving in Lean 4 Introduction Dependent Type Theory Propositions and Proofs Quantifiers and Equality Tactics Interacting with Lean Inductive Types Induction and Recursion Structures and Records Type Classes The Conversion Tactic Mode Axioms and Computation