Formalisation of Quillen's homotopical algebra (model categories, etc.), localization of categories (towards the fundamental lemma of homotopical algebra, and also localization of triangulated categories).
Get the code using leanproject get joelriou/homotopical_algebra.
The fundamental lemma of homotopical algebra appears in src/for_mathlib/algebraic_topology/homotopical_algebra/fundamental_lemma.lean.
The localization results for triangulated categories are obtained in src/for_mathlib/category_theory/localization/triangulated_subcategory.lean.