Top 3 used theorems of each topological ordering level Level 1 rfl Set List Level 2 Eq.symm mul_comm mul_assoc Level 3 Iff.rfl le_rfl funext Level 4 eq_comm Set.ext lt_of_le_of_lt Level 5 Classical.not_not Filter.Eventually.mono ne_of_gt Level 6 not_le le_or_lt Nat.pos_of_ne_zero Level 7 Nat.mul_comm div_pos subsingleton_or_nontrivial Level 8 not_lt norm_smul Finset.induction_on Level 9 Nat.mod_eq_of_lt Finset.mem_image Nat.sub_add_cancel Level 10 List.TFAE.out Nat.mod_lt Finset.coe_image Level 11 isClosed_closure Cardinal.nat_lt_aleph0 MeasureTheory.Measure.restrict_univ Level 12 closure_mono Set.inter_iUnion mem_nhds_iff Level 13 IsOpen.mem_nhds continuous_iff_continuousAt mem_of_mem_nhds Level 14 Finset.mem_range Polynomial.leadingCoeff_eq_zero Int.cast_add Level 15 nhds_prod_eq Polynomial.coeff_map Continuous.continuousOn Level 16 Finset.mem_sdiff MeasureTheory.lintegral_mono MeasureTheory.lintegral_const Level 17 Int.add_assoc Real.rpow_def_of_pos Complex.ofReal_cpow Level 18 Polynomial.eval_map Complex.exp_add Finset.card_sdiff Level 19 MeasureTheory.withDensity_apply Polynomial.monic_X_sub_C MeasureTheory.integrable_const Level 20 Primrec.snd Primrec.fst Real.log_mul Level 21 contDiffWithinAt_localInvariantProp Real.exp_neg Real.mul_rpow Level 22 Real.exp_pos Matrix.det_transpose Real.rpow_neg Level 23 Real.rpow_pos_of_pos Real.rpow_nonneg zpow_add Level 24 MeasureTheory.measure_union_le Real.log_rpow Real.rpow_intCast Level 25 Real.rpow_natCast Matrix.det_mul Real.rpow_neg_one Level 26 EuclideanGeometry.oangle_rotate_sign minpoly.dvd Measurable.stronglyMeasurable Level 27 MvPolynomial.aeval_X MeasureTheory.Measure.restrict_mono Complex.abs_cpow_eq_rpow_re_of_pos Level 28 Real.pi_pos Int.natCast_dvd_natCast MeasureTheory.Measure.restrict_congr_set Level 29 Real.two_pi_pos MvPolynomial.map_injective intervalIntegrable_iff_integrableOn_Ioc_of_le Level 30 MeasureTheory.integrable_indicator_iff Nat.prime_of_mem_primeFactors Real.cos_pos_of_mem_Ioo Level 31 MeasureTheory.ae_restrict_iff' Real.Angle.sign_coe_pi_div_two HasProd.tprod_eq Level 32 MeasureTheory.dominatedFinMeasAdditive_weightedSMul MeasureTheory.ae_restrict_mem MeasureTheory.setLIntegral_congr_fun Level 33 MeasureTheory.integral_congr_ae MeasureTheory.integral_sub MeasureTheory.integral_add Level 34 MeasureTheory.integral_mul_left MeasureTheory.setIntegral_congr_ae Int.not_even_iff_odd Level 35 Real.rpow_mul MeasureTheory.setIntegral_congr_fun Int.modEq_iff_dvd Level 36 NNReal.rpow_mul Complex.cpow_one Complex.isPrimitiveRoot_exp Level 37 ENNReal.rpow_mul NNReal.rpow_self_rpow_inv Complex.arg_real_mul Level 38 ZMod.intCast_zmod_eq_zero_iff_dvd collinear_pair Complex.Gamma_ofReal Level 39 ZMod.natCast_zmod_eq_zero_iff_dvd Rat.normalize_eq Complex.mul_cpow_ofReal_nonneg Level 40 MeasureTheory.memℒp_const jacobiSym.mod_left ZMod.coe_intCast Level 41 Orientation.oangle_rev Real.sqrt_eq_rpow Polynomial.natDegree_eq_card_roots Level 42 Rat.mul_def NumberField.InfinitePlace.not_isReal_iff_isComplex MeasureTheory.indicatorConstLp_coeFn Level 43 Real.hasDerivAt_rpow_const Rat.add_def ProbabilityTheory.Kernel.integrable_density Level 44 Rat.num_divInt_den Rat.divInt_eq_iff Polynomial.natSepDegree_eq_of_isAlgClosed Level 45 Rat.mk'_eq_divInt Rat.divInt_mul_divInt Real.continuousAt_rpow_const Level 46 Polynomial.prod_cyclotomic_eq_X_pow_sub_one Polynomial.cyclotomic.monic Rat.divInt_mul_right Level 47 Polynomial.cyclotomic_ne_zero Polynomial.natDegree_cyclotomic IsGalois.card_aut_eq_finrank Level 48 IsCyclotomicExtension.finrank Rat.inv_divInt' Algebra.norm_eq_prod_embeddings Level 49 LieAlgebra.IsKilling.root_apply_coroot Algebra.isIntegral_trace Polynomial.cyclotomic_prime Level 50 Rat.divInt_eq_div map_wittStructureInt minpoly.isIntegrallyClosed_eq_field_fractions' Level 51 exists_rat_btwn Rat.num_div_den wittStructureInt_vars Level 52 WittVector.zero_coeff NNRat.cast_smul_eq_nnqsmul SimpleGraph.not_isUniform_iff Level 53 IsIntegralClosure.isNoetherian RCLike.wInner_cWeight_eq_expect Rat.inv_natCast_den_of_pos Level 54 MeasureTheory.SimpleFunc.iSup_eapprox_apply IsCyclotomicExtension.discr_prime_pow_ne_two LieAlgebra.IsKilling.chainTopCoeff_zero_right Level 55 Measurable.ennreal_induction WittVector.frobenius_verschiebung MeasureTheory.lintegral_eq_iSup_eapprox_lintegral Level 56 MeasureTheory.lintegral_map MeasureTheory.lintegral_const_mul LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff Level 57 MeasureTheory.lintegral_add_left MeasureTheory.Measure.bind_apply MeasureTheory.withDensity_smul Level 58 MeasureTheory.Measure.prod_apply MeasureTheory.lintegral_add_left' ProbabilityTheory.Kernel.comp_apply' Level 59 MeasureTheory.Measure.prod_prod MeasureTheory.lintegral_add_right' MeasureTheory.Integrable.trim Level 60 Module.Flat.rTensor_preserves_injective_linearMap MeasureTheory.lintegral_eq_zero_iff' MeasureTheory.lintegral_tsum Level 61 MeasureTheory.lintegral_eq_zero_iff Module.Flat.lTensor_preserves_injective_linearMap MeasureTheory.Measure.prod_eq Level 62 Polynomial.cyclotomic.irreducible_rat MeasureTheory.eLpNorm_add_le MeasureTheory.Measure.rnDeriv_eq_zero Level 63 ProbabilityTheory.Kernel.compProd_apply MeasureTheory.Measure.prod_swap MeasureTheory.ae_lt_top Level 64 MeasureTheory.Measure.rnDeriv_lt_top MeasureTheory.Measure.compProd_apply MeasureTheory.Measure.pi_eq Level 65 MeasureTheory.Measure.rnDeriv_pos ProbabilityTheory.Kernel.lintegral_compProd MeasureTheory.Measure.pi_of_empty Level 66 MeasureTheory.Measure.pi_pi MeasureTheory.Measure.rnDeriv_withDensity ProbabilityTheory.Kernel.ae_ae_of_ae_compProd Level 67 MeasureTheory.volume_pi_pi MeasureTheory.quasiMeasurePreserving_inv MeasureTheory.measurePreserving_piCongrLeft Level 68 Real.volume_Icc_pi MeasureTheory.integrableOn_Lp_of_measure_ne_top NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis Level 69 EuclideanSpace.volume_preserving_measurableEquiv MeasureTheory.tendsto_integral_of_dominated_convergence MeasureTheory.lmarginal_union Level 70 MeasureTheory.tendsto_integral_filter_of_dominated_convergence MeasureTheory.lmarginal_insert MeasureTheory.setIntegral_trim Level 71 MeasureTheory.Lp.simpleFunc.denseRange MeasureTheory.continuousAt_of_dominated BoxIntegral.Box.volume_apply Level 72 MeasureTheory.L1.setToL1_eq_setToL1SCLM MeasureTheory.Lp.induction AddCircle.ergodic_zsmul Level 73 MeasureTheory.L1.norm_setToL1_le_mul_norm MeasureTheory.L1.norm_setToL1_le_mul_norm' MeasureTheory.Integrable.induction Level 74 MeasureTheory.integral_eq_lintegral_of_nonneg_ae MeasureTheory.SimpleFunc.integral_eq_integral Real.dimH_of_mem_nhds Level 75 MeasureTheory.integral_nonneg_of_ae MeasureTheory.integral_toReal MeasureTheory.lintegral_coe_eq_integral Level 76 MeasureTheory.integral_nonneg MeasureTheory.setIntegral_mono_set MeasureTheory.integral_mono_ae Level 77 MeasureTheory.integral_const MeasureTheory.ofReal_integral_eq_lintegral_ofReal MeasureTheory.integral_mono_of_nonneg Level 78 MeasureTheory.norm_integral_le_integral_norm MeasureTheory.setIntegral_const MeasureTheory.setIntegral_mono_on Level 79 MeasureTheory.integral_smul_measure MeasureTheory.norm_integral_le_of_norm_le intervalIntegral.integral_mono_on Level 80 MeasureTheory.Measure.addHaar_smul MeasureTheory.average_eq MeasureTheory.setIntegral_union Level 81 MeasureTheory.integral_add_compl MeasureTheory.integrableOn_Ioi_comp_mul_left_iff MeasureTheory.Measure.addHaar_smul_of_nonneg Level 82 MeasureTheory.integral_indicator intervalIntegral.integral_add_adjacent_intervals MeasureTheory.Measure.addHaar_closedBall' Level 83 MeasureTheory.integral_indicator_const MeasureTheory.addHaar_image_le_mul_of_det_lt intervalIntegral.integral_comp_mul_add Level 84 ContinuousLinearMap.integral_comp_comm MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero ProbabilityTheory.isCondKernelCDF_condCDF Level 85 integral_smul_const ContinuousLinearMap.integral_apply MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball Level 86 MeasureTheory.integral_prod integral_withDensity_eq_integral_smul MeasureTheory.measure_le_eq_lt Level 87 ProbabilityTheory.setIntegral_compProd hasFDerivAt_integral_of_dominated_loc_of_lip Real.fourierIntegral_continuousLinearMap_apply' Level 88 hasFDerivAt_integral_of_dominated_of_fderiv_le MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' MeasureTheory.integral_prod_mul Level 89 VectorFourier.hasFDerivAt_fourierIntegral intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right Level 90 intervalIntegral.integral_hasStrictDerivAt_right intervalIntegral.integral_hasDerivWithinAt_right Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable Level 91 MeasureTheory.integral_fintype_prod_eq_pow intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le intervalIntegral.integrableOn_deriv_of_nonneg Level 92 intervalIntegral.intervalIntegrable_rpow' intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le intervalIntegral.integral_eq_sub_of_hasDeriv_right Level 93 intervalIntegral.integral_eq_sub_of_hasDerivAt intervalIntegral.intervalIntegrable_cpow' MeasureTheory.condexpIndL1Fin_ae_eq_condexpIndSMul Level 94 MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto' MeasureTheory.condexpInd_ae_eq_condexpIndSMul integral_cpow Level 95 intervalIntegral.integral_deriv_eq_sub' integrableOn_Ioi_rpow_of_lt MeasureTheory.integral_of_hasDerivAt_of_tendsto Level 96 integral_inv MeasureTheory.integral_image_eq_integral_abs_deriv_smul MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul Level 97 Real.GammaIntegral_convergent intervalIntegral.integral_mul_deriv_eq_deriv_mul MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure Level 98 MeasureTheory.dominatedFinMeasAdditive_condexpInd mellinConvergent_of_isBigO_rpow Complex.GammaIntegral_convergent Level 99 integral_sin_pow MeasureTheory.condexpL1_eq MeasureTheory.condexpL1CLM_indicatorConstLp Level 100 MeasureTheory.condexpL1CLM_indicatorConst mellin_differentiableAt_of_isBigO_rpow Complex.GammaIntegral_add_one Level 101 integral_sin_pow_pos Complex.GammaAux_recurrence1 integrable_rpow_mul_exp_neg_mul_sq Level 102 integrable_exp_neg_mul_sq MeasureTheory.setIntegral_condexpL1CLM MeasureTheory.aestronglyMeasurable'_condexpL1 Level 103 MeasureTheory.condexp_ae_eq_condexpL1 Complex.Gamma_eq_GammaAux ProbabilityTheory.integrable_gaussianPDFReal Level 104 MeasureTheory.setIntegral_condexp MeasureTheory.condexp_congr_ae MeasureTheory.condexp_add Level 105 Real.Gamma_add_one MeasureTheory.ae_eq_condexp_of_forall_setIntegral_eq MeasureTheory.condexp_neg Level 106 Real.Gamma_pos_of_pos MeasureTheory.condexp_sub Real.Gamma_one Level 107 MeasureTheory.condexp_indicator Real.convexOn_log_Gamma ProbabilityTheory.Kernel.martingale_densityProcess Level 108 ProbabilityTheory.condexpKernel_ae_eq_condexp MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on Complex.Gamma_ne_zero Level 109 integral_cexp_quadratic Complex.differentiableOn_compl_singleton_and_continuousAt_iff HurwitzZeta.completedHurwitzZetaOdd_one_sub Level 110 Complex.Gammaℝ_ne_zero_of_re_pos Real.Gamma_one_half_eq Complex.differentiableOn_dslope Level 111 Complex.differentiableOn_update_limUnder_of_isLittleO Complex.tsum_exp_neg_quadratic ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet Level 112 Complex.Gammaℝ_one ProbabilityTheory.Kernel.integral_density jacobiTheta₂_functional_equation Level 113 HurwitzZeta.hasSum_nat_cosZeta Complex.volume_ball HurwitzZeta.differentiableAt_hurwitzZetaEven Level 114 NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd zeta_eq_tsum_one_div_nat_cpow HurwitzZeta.hasSum_nat_sinZeta Level 115 zeta_nat_eq_tsum_of_gt_one ArithmeticFunction.LSeries_zeta_eq_riemannZeta ZMod.differentiableAt_LFunction Level 116 LSeries_one_eq_riemannZeta DirichletCharacter.differentiableAt_LFunction tsum_riemannZetaSummand Level 117 Complex.inv_Gammaℝ_one_sub ZMod.LFunction_dft ProbabilityTheory.Kernel.withDensity_one_sub_rnDerivAux Level 118 DirichletCharacter.LFunction_eq_LSeries ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice HurwitzZeta.hurwitzZetaEven_one_sub Level 119 ProbabilityTheory.Kernel.mutuallySingular_singularPart DirichletCharacter.LFunction_ne_zero_of_one_le_re ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice Level 120 DirichletCharacter.LFunctionTrivChar_residue_one ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_mutuallySingularSetSlice ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero Level 121 ProbabilityTheory.Kernel.rnDeriv_add_singularPart ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux DirichletCharacter.differentiable_LFunctionTrivChar₁ Level 122 ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular Level 123 ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux' ProbabilityTheory.Kernel.rnDeriv_singularPart ProbabilityTheory.Kernel.rnDeriv_add Level 124 ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux Level 125 ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound Level 126 ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div Level 127 Nat.setOf_prime_and_eq_mod_infinite Level 128 Nat.forall_exists_prime_gt_and_eq_mod