• There are 38,139 files with 5,889,779 lines of code.
• 773 very long files (1,432,701 lines of code)
• 2,051 long files (1,419,878 lines of code)
• 4,938 medium size files (1,558,958 lines of code)
• 4,904 small files (710,409 lines of code)
• 25,473 very small files (767,833 lines of code)

There are 30629 files with lines longer than 120 characters. In total, there are 194956 long lines.

File	# lines	# units	# long lines
lean S_LanglandsTunnell_P2_raySymbol_artinValue_span_eq_one_of_artinPairCore.lean in P2M/Sol	3958	-	529
lean S_AutomorphicForm_semilocal_central_transfer_referenceMeasures_peel_step.lean in P2M/Sol	5695	-	444
lean S_LanglandsTunnell_Artin_exists_artinFieldCore_exists_artinPairCore_of_isAdmissibleModulusOfDegree.lean in P2M/Sol	2921	-	423
lean S_LanglandsTunnell_P2_raySymbol_artinValue_span_eq_one_of_artinFieldCore.lean in P2M/Sol	2909	-	399
lean S_CerednikDrinfeld_QM_FakeEllipticCurve_Rigidification_n_eq_n_add_sub_slackExponent_of_isRigTransport_of_isRigTransport_translate_of_isActBy.lean in P2M/Sol	1894	-	398
lean S_LanglandsTunnell_Artin_exists_artinFieldCore_nonempty_artinPairCore.lean in P2M/Sol	2785	-	392
lean S_AlgebraicCurve_tateAgreement_v2.lean in P2M/Sol	3861	-	338
lean S_AlgebraicCurve_tateAgreement.lean in P2M/Sol	3861	-	335
lean S_NumberField_exists_addSubgroup_forall_finsum_units_mul_prod_zpow_neg_mul_sum_integral_discWindow_eq_tsum_mul_tsum_ite_kinkWindow_of_contDiff_of_forall_eq_of_norm_sub_le.lean in P2M/Sol	3483	-	334
lean S_AlgebraicCurve_tateTraceCompat_of_isSeparable.lean in P2M/Sol	3463	-	333
lean S_NumberField_TateGlobal_zetaIntegral_meromorphic_continuation_fe.lean in P2M/Sol	6511	-	297
lean S_LanglandsTunnell_Artin_exists_Ni_eq_Ni_and_symbol_eq_of_artinPairCore.lean in P2M/Sol	2849	-	288
lean S_AutomorphicForm_semilocal_central_transfer_peel_step.lean in P2M/Sol	4442	-	280
lean S_LanglandsTunnell_RankinSelberg_forall_godementZeta2_whittaker_clearedFE_of_forall_torusZeta_fe_of_cuspidal.lean in P2M/Sol	3715	-	273
lean S_LanglandsTunnell_RankinSelberg_exists_purifier_whittakerCoefficient_eq_mul_pSlot_of_finiteFamily_arch.lean in P2M/Sol	1565	-	255
lean S_NumberField_TateGlobal_exists_differentiable_eq_partialEulerProduct_of_exists_mem_normOneIdeles_ne_one.lean in P2M/Sol	5449	-	247
lean S_NumberField_TateGlobal_exists_meromorphicOn_eq_partialEulerProduct.lean in P2M/Sol	5396	-	246
lean S_NumberField_TateGlobal_exists_meromorphicOn_analyticAt_one_eq_partialEulerProduct_of_ne_one.lean in P2M/Sol	5367	-	246
lean S_NumberField_TateGlobal_integrable_zetaIntegrand.lean in P2M/Sol	5200	-	245
lean S_LocalNewvector_PSCarrier_isIrreducibleGLRep_of_hasCharConductor_of_ratio.lean in P2M/Sol	5618	-	244
lean S_LanglandsTunnell_RankinSelberg_exists_ne_zero_forall_integrable_and_rsFinIntegral_indicator_eq_mul_finprod_rsLocalIntegral_of_pure_of_measurable.lean in P2M/Sol	1606	-	241
lean S_LanglandsTunnell_Converse_dualTorusPair_iwasawa_fibre_eq_const_mul_integral_torusQuadruple_detPow_blockQuadratic_colHarmonic.lean in P2M/Sol	1218	-	238
lean S_Ihara_mennickeCSP_of_prime.lean in P2M/Sol	7680	-	236
lean S_LocalNewvector_PSCarrier_finrank_inf_fixedSubmodule_padicK1_of_stable.lean in P2M/Sol	7751	-	229
lean S_LanglandsTunnell_Artin_Ni_mem_normRaySubgroup_of_symbol_eq_one.lean in P2M/Sol	1920	-	227
lean S_LocalNewvector_PSCarrier_existsUnique_mem_inf_fixedSubmodule_padicK1_one_of_stable.lean in P2M/Sol	7747	-	218
lean S_NumberField_TateGlobal_exists_forall_zetaIntegral_mul_eulerFactors_eq_of_eq_indicator.lean in P2M/Sol	4698	-	216
render.py in tools/docs-site/gen	1059	21	215
lean S_AutomorphicForm_continuous_bruhatTransversal_tsum_of_re_gt_half.lean in P2M/Sol	2272	-	214
lean S_QuadraticForm_exists_rat_ternary_pureNrd_eq_of_forall_adicCompletion_of_real.lean in P2M/Sol	6794	-	211
lean S_AutomorphicForm_bruhatTransversal_summand_norm_summable_of_re_gt_half.lean in P2M/Sol	2250	-	210
lean S_ModularCurve_XHDRModelAtP_exists_iso_pullback_toBase_specMap_atkinLehner_complement_placePin.lean in P2M/Sol	1849	-	209
lean S_ModularCurve_XHDRModelAtP_ord_placeOn_germ_chart_eq_one_of_chart_of_residue_surjective.lean in P2M/Sol	561	-	207
lean S_LanglandsTunnell_RankinSelberg_exists_rsLocalIntegral_jacquetWhittaker3_iotaGL_eq_sum_and_dual_eq_mul_sum_of_chamber_ed2.lean in P2M/Sol	1564	-	205
lean S_AlgebraicGeometry_nonempty_towerQuotientDatum_of_isProper_of_flat_of_forall_exists_isAffineOpen.lean in P2M/Sol	4519	-	202
lean S_AlgebraicGeometry_OModulePresheaf_IterCech_exists_dTot_eq_single_augTot_sub_single_augCech_cup.lean in P2M/Sol	1210	-	202
lean S_QuadraticForm_forall_exists_ternary_pureNrd_eq_of_exists_ne_zero_eq_zero.lean in P2M/Sol	6771	-	200
lean S_NumberField_TateGlobal_zetaIntegral_mul_eulerFactors_eq.lean in P2M/Sol	4687	-	197
lean S_NumberField_LevelArith_exists_continuousH1Sr_sUnitsMaxRep_linearMap_sClassGroupRep_injective_natural.lean in P2M/Sol	2065	-	196
lean S_LanglandsTunnell_RankinSelberg_exists_finTranslate_not_countable_rsFinIntegral_indicator_ne_zero_of_purifier_of_finiteFamily_arch.lean in P2M/Sol	2020	-	195
lean S_LanglandsTunnell_RankinSelberg_rsLocalIntegral_godementWhittaker_iotaGL_eq_sum_rsLocalIntegral_mul_godementZeta.lean in P2M/Sol	613	-	194
lean S_LanglandsTunnell_RankinSelberg_exists_dualTorusPair_eq_archRootNumber_mul_explicit_mul_gammaFactor_of_weightOne_of_minorSection_gaussian3_of_profile.lean in P2M/Sol	1025	-	194
lean S_ModularCurve_PDPairing_pairZFun_heckeT0_comm.lean in P2M/Sol	6437	-	194
lean S_ModularCurve_PDPairing_isFreeGroup_Gamma_four.lean in P2M/Sol	6435	-	193
lean S_ModularCurve_PDPairing_pairZFun_jDeg0_iDeg0.lean in P2M/Sol	6438	-	190
lean S_ModularCurve_PDPairing_index_Gamma_four.lean in P2M/Sol	6434	-	189
lean S_LanglandsTunnell_RankinSelberg_exists_forall_integrable_rsFinCellIntegrand_pureTensorTerm_dual_and_hybrid_of_depth_twisted_torusFinite_central_growth_of_principalLevel_of_gammaHyp.lean in P2M/Sol	1419	-	187
lean S_LanglandsTunnell_RankinSelberg_matFourier22_kirillov_det_mul_coefficient_eq_of_cuspidal.lean in P2M/Sol	3295	-	178
lean S_CerednikDrinfeld_QM_IsFineModuliT_fineFamilyT_apply_eq_apply_of_isPullback_of_frobTwist_eq_of_translate_of_isNoetherianRing_eq.lean in P2M/Sol	597	-	177
lean S_CerednikDrinfeld_QM_IsCoarseModuliT_exists_towerFamily_connected_of_evenRigidifiedPair_of_heckeDictionary_of_isNoetherianRing_heightNormalised_oneLegC5.lean in P2M/Sol	860	-	176

• File size measurements show the distribution of size of files.
• Files are classified in four categories based on their size (lines of code): 1-100 (very small files), 101-200 (small files), 201-500 (medium size files), 501-1000 (long files), 1001+(very long files).
• It is a good practice to keep files small. Long files may become "bloaters", code that have increased to such gargantuan proportions that they are hard to work with.