Mathlib Privatization Candidate Dashboard

Last updated: 2026-05-12 03:04 UTC
How to read this dashboard: what the tiers mean and where to look

Candidates are split into three tiers by reference shape. The tabs match the tiers.

TierWhat it groupsCountWhere it shows
Tier 1 One row = one decl. 0 external users, 0 intra-module refs, policy-clean. Applied as a single private edit. 8,124 Rolled up into Tier-2 bundles. Each bundle's decls column lists its tier-1 members.
Tier 2 One row = one module. Modules with ≥ 3 tier-1 decls. One PR per module privatizes its tier-1 set in one commit. Score: blast-cone CP × T30 multiplier (3× if top-30 by leverage) × log(1+edits). 718 Top-25 on Summary; full list under Tier 2 — Module bundles.
Tier 3 One row = one decl. A def, abbrev, or structure constructor whose type is referenced by ≥ 2 decls in the same module, with ≤ 30 external users. Action: move the hub and its dependents into a sub-module that the parent imports privately. 21,988 Tier 3 — Encapsulation candidates tab.

T30: the 30 mathlib modules with the highest leverage (edits × cascade-cost) over the last 1,500 master commits. Acts as a 3× multiplier on the Tier-2 score. Full formula and selection rules under Methodology.

Other tabs. Methodology: how candidates are selected, bundled, and scored. Why some decls are excluded: per-decl reasoning for non-candidates (blocked attribute, forbidden name pattern, registered in an extension's by-name registry, etc.). Run history: per-run tier counts and transitions (new / merged / dropped).

Mathlib decls scanned
349,712
+0 since last run
Tier-1 candidates
8,124
+0 since last run
Tier-2 bundles
718
+0 since last run
Tier-3 encap hubs
21,988
-3430 since last run
New since last run
0
Merged (now private)
0

Top 25 module bundles by impact

Modules with mechanically-safe privatization available. Each row groups all tier-1 candidates in that module. Score combines blast-cone CP × top-30 multiplier × log(1+edits).

Score N decls Top-30 Edits Module / Decls Action
144.0 146
Mathlib.AlgebraicTopology.SimplicialObject.Basic
  • CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj candidate
  • CategoryTheory.CosimplicialObject.comp_left candidate
  • CategoryTheory.SimplicialObject.Augmented.const_obj_hom candidate
  • CategoryTheory.CosimplicialObject.Augmented.leftOp_right candidate
  • CategoryTheory.CosimplicialObject.id_right_app candidate
  • CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj candidate
  • CategoryTheory.CosimplicialObject.Augmented.const_map_left candidate
  • CategoryTheory.CosimplicialObject.Augmented.const_obj_left candidate
  • CategoryTheory.CosimplicialObject.instHasLimits candidate
  • CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc candidate
  • CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc candidate
  • CategoryTheory.SimplicialObject.Augmented.w_app_assoc candidate
  • CategoryTheory.CosimplicialObject.Augmented.whiskering_obj candidate
  • CategoryTheory.CosimplicialObject.comp_right_app candidate
  • CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map candidate
  • CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation candidate
  • CategoryTheory.CosimplicialObject.δ_comp_δ' candidate
  • CategoryTheory.CosimplicialObject.augmentOfIsInitial_hom_app candidate
  • CategoryTheory.SimplicialObject.Augmented.whiskeringObj.eq_1 candidate
  • CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app candidate
  • CategoryTheory.CosimplicialObject.Augmented.const_obj_right candidate
  • CategoryTheory.SimplicialObject.Augmented.hom_ext_iff candidate
  • CategoryTheory.CosimplicialObject.σ_naturality_assoc candidate
  • SimplexCategory.Truncated.incl.congr_simp candidate
  • CategoryTheory.CosimplicialObject.augment_left candidate
  • … and 55 more
ready to PR
120.0 120
Mathlib.MeasureTheory.Function.SimpleFunc
  • MeasureTheory.SimpleFunc.restrict.eq_1 candidate
  • MeasureTheory.SimpleFunc.ext_iff candidate
  • MeasureTheory.SimpleFunc.neg_apply candidate
  • MeasureTheory.SimpleFunc.approx_comp candidate
  • MeasureTheory.SimpleFunc.instSMulCommClass candidate
  • MeasureTheory.SimpleFunc.restrict_preimage candidate
  • MeasureTheory.SimpleFunc.ennrealRatEmbed.eq_1 candidate
  • MeasureTheory.SimpleFunc.coe_mk candidate
  • MeasureTheory.SimpleFunc.sup_eq_map₂ candidate
  • MeasureTheory.SimpleFunc.inv_apply candidate
  • MeasureTheory.SimpleFunc.instZero.eq_1 candidate
  • MeasureTheory.SimpleFunc.const_algebraMap candidate
  • MeasureTheory.SimpleFunc.map_coe_nnreal_restrict candidate
  • MeasureTheory.SimpleFunc.le_sup_lintegral candidate
  • MeasureTheory.SimpleFunc.aemeasurable candidate
  • MeasureTheory.SimpleFunc.zero_lintegral candidate
  • MeasureTheory.SimpleFunc.seq_apply candidate
  • MeasureTheory.SimpleFunc.map_restrict_of_zero candidate
  • MeasureTheory.SimpleFunc.approx_apply candidate
  • MeasureTheory.SimpleFunc.instSub.eq_1 candidate
  • MeasureTheory.SimpleFunc.eapprox_lt_top candidate
  • MeasureTheory.SimpleFunc.comp.congr_simp candidate
  • MeasureTheory.SimpleFunc.mem_restrict_range candidate
  • MeasureTheory.SimpleFunc.instSMul.eq_1 candidate
  • MeasureTheory.SimpleFunc.pair_preimage candidate
  • … and 55 more
ready to PR
109.6 143
Mathlib.Combinatorics.SimpleGraph.Subgraph
  • SimpleGraph.Subgraph.spanningCoe_bot candidate
  • SimpleGraph.Subgraph.degree_of_notMem_verts candidate
  • SimpleGraph.Subgraph.deleteVerts_le candidate
  • SimpleGraph.degree_toSubgraph candidate
  • SimpleGraph.Subgraph.induce_self_verts candidate
  • SimpleGraph.Subgraph.spanningCoe_top candidate
  • SimpleGraph.Subgraph.Adj.adj_sub' candidate
  • SimpleGraph.Subgraph.restrict_coeSubgraph candidate
  • SimpleGraph.Subgraph.deleteEdges_verts candidate
  • SimpleGraph.Subgraph.edgeSet_inf candidate
  • SimpleGraph.Subgraph.coeDeleteVertsIso candidate
  • SimpleGraph.Subgraph.incidenceSet_subset candidate
  • SimpleGraph.toSubgraph_verts candidate
  • SimpleGraph.Subgraph.coe_deleteEdges_eq candidate
  • SimpleGraph.Subgraph.spanningCoe_coe candidate
  • SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree candidate
  • SimpleGraph.Subgraph.Adj.of_spanningCoe candidate
  • SimpleGraph.Subgraph.spanningHom_injective candidate
  • SimpleGraph.Subgraph.coe_deleteEdges_le candidate
  • SimpleGraph.Subgraph.neighborSet_sInf candidate
  • SimpleGraph.Subgraph.deleteVerts_mono candidate
  • SimpleGraph.Subgraph.verts_sInf candidate
  • SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq candidate
  • SimpleGraph.Subgraph.induce_mono candidate
  • SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet candidate
  • … and 55 more
ready to PR
81.0 105
Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  • SimpleGraph.Walk.take.eq_1 candidate
  • SimpleGraph.Walk.reverseAux_append candidate
  • SimpleGraph.Walk.mem_support_of_mem_edges candidate
  • SimpleGraph.Walk.dropLast_cons_nil candidate
  • SimpleGraph.Walk.support_concat candidate
  • SimpleGraph.Walk.dropLast_nil candidate
  • SimpleGraph.Walk.reverse_injective candidate
  • SimpleGraph.Walk.concatRec_nil candidate
  • SimpleGraph.Walk.concatRecAux.eq_def candidate
  • SimpleGraph.Walk.Nil.eq_copy_nil candidate
  • SimpleGraph.Walk.copy_cons candidate
  • SimpleGraph.Walk.length_dropLast_add_one candidate
  • SimpleGraph.Walk.dropLast_concat candidate
  • SimpleGraph.Walk.concatRec.eq_1 candidate
  • SimpleGraph.Walk.take.eq_def candidate
  • SimpleGraph.Walk.concat_dropLast candidate
  • SimpleGraph.Walk.drop.eq_3 candidate
  • SimpleGraph.Walk.Nil.append candidate
  • SimpleGraph.Walk.copy.eq_1 candidate
  • SimpleGraph.Walk.drop_add_eq candidate
  • SimpleGraph.Walk.darts_copy candidate
  • SimpleGraph.Walk.reverse_copy candidate
  • SimpleGraph.Walk.cons_reverseAux candidate
  • SimpleGraph.Walk.concat_inj candidate
  • SimpleGraph.Walk.append_copy_copy candidate
  • … and 55 more
ready to PR
73.0 87
Mathlib.Combinatorics.SimpleGraph.Maps
  • SimpleGraph.Iso.comap_symm_apply candidate
  • SimpleGraph.Embedding.preimage_neighborSet candidate
  • SimpleGraph.«term_→g_» candidate
  • SimpleGraph.Iso.mapNeighborSet_apply_coe candidate
  • SimpleGraph.Hom.mapNeighborSet_coe candidate
  • SimpleGraph.neighborSet_mono candidate
  • SimpleGraph.comap_comap candidate
  • SimpleGraph.Iso.mapEdgeSet_symm_apply candidate
  • SimpleGraph.map_le_iff_le_comap candidate
  • SimpleGraph.induce_top candidate
  • SimpleGraph.neighborSet_map_equiv candidate
  • SimpleGraph.«term_↪g_» candidate
  • SimpleGraph.Embedding.map_mem_edgeSet_iff candidate
  • SimpleGraph.Hom.instFinite candidate
  • SimpleGraph.Hom.ofLE_apply candidate
  • SimpleGraph.map_comap_le candidate
  • SimpleGraph.support_spanningCoe candidate
  • SimpleGraph.induce_spanningCoe candidate
  • SimpleGraph.Iso.coe_comp candidate
  • SimpleGraph.Hom.coe_id candidate
  • SimpleGraph.Embedding.preimage_edgeSet candidate
  • SimpleGraph.Embedding.coe_toHom candidate
  • SimpleGraph.map_adj' candidate
  • SimpleGraph.Hom.comp_comap_ofLE candidate
  • SimpleGraph.induceUnivIso_symm_apply_coe candidate
  • … and 55 more
ready to PR
57.8 78
Mathlib.Combinatorics.SimpleGraph.Paths
  • SimpleGraph.Walk.mapLe_isCycle candidate
  • SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset candidate
  • SimpleGraph.Path.count_support_eq_one candidate
  • SimpleGraph.Walk.IsPath.take candidate
  • SimpleGraph.Walk.map_isTrail_iff_of_injective candidate
  • SimpleGraph.Path.map_injective candidate
  • SimpleGraph.Walk.IsTrail.of_append_right candidate
  • SimpleGraph.Path.map_coe candidate
  • SimpleGraph.Walk.isCircuit_rotate candidate
  • SimpleGraph.Path.mapEmbedding_coe candidate
  • SimpleGraph.Walk.IsTrail.reverse candidate
  • SimpleGraph.Walk.IsPath.drop candidate
  • SimpleGraph.Path.singleton_coe candidate
  • SimpleGraph.Walk.bypass.eq_def candidate
  • SimpleGraph.Walk.IsTrail.of_cons candidate
  • SimpleGraph.Walk.isTrail_of_isSubwalk candidate
  • SimpleGraph.Path.nil_coe candidate
  • SimpleGraph.Walk.not_nil_of_isCycle_cons candidate
  • SimpleGraph.Walk.isCycle_copy candidate
  • SimpleGraph.Walk.support_toPath_subset candidate
  • SimpleGraph.Walk.IsCycle.isPath_of_append_left candidate
  • SimpleGraph.Walk.reverse_isTrail_iff candidate
  • SimpleGraph.Walk.isCircuit_def candidate
  • SimpleGraph.Walk.IsTrail.dropUntil candidate
  • SimpleGraph.Walk.IsCycle.isPath_of_append_right candidate
  • … and 53 more
ready to PR
57.0 57
Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
  • Affine.Simplex.faceOpposite_point_eq_point_one candidate
  • Affine.Simplex.interior_restrict candidate
  • Affine.Simplex.map_subtype_restrict candidate
  • Affine.Simplex.map_id candidate
  • Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc candidate
  • Affine.Simplex.reindex_map candidate
  • Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg candidate
  • Affine.Simplex.map_comp candidate
  • Affine.Simplex.closedInterior_reindex candidate
  • Affine.Simplex.affineCombination_mem_setInterior_iff candidate
  • Affine.Simplex.faceOpposite_point_eq_point_zero candidate
  • Affine.Simplex.faceOpposite_map candidate
  • Affine.Simplex.face.eq_1 candidate
  • Affine.Simplex.closedInterior_faceOpposite_subset_closedInterior candidate
  • Affine.Simplex.map.congr_simp candidate
  • Affine.Simplex.mk.congr_simp candidate
  • Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo candidate
  • Affine.Simplex.map_mkOfPoint candidate
  • Affine.Simplex.interior_map candidate
  • Affine.Simplex.setInterior.eq_1 candidate
  • Affine.Simplex.interior.eq_1 candidate
  • Affine.Simplex.faceOpposite.congr_simp candidate
  • Affine.Simplex.point_mem_closedInterior_faceOpposite_iff candidate
  • Affine.Simplex.mk.inj candidate
  • Affine.Simplex.closedInterior.eq_1 candidate
  • … and 32 more
ready to PR
56.7 95
Mathlib.Combinatorics.SimpleGraph.Clique
  • SimpleGraph.IsContained.not_cliqueFree_card candidate
  • SimpleGraph.isClique_insert candidate
  • SimpleGraph.isClique_empty candidate
  • SimpleGraph.isClique_iff_isChain_adj candidate
  • SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCard candidate
  • SimpleGraph.IsMaximumIndepSet.isIndepSet candidate
  • SimpleGraph.cliqueSet_zero candidate
  • SimpleGraph.isMaximalIndepSet_compl candidate
  • SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet candidate
  • SimpleGraph.cliqueSet_mono' candidate
  • SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique candidate
  • SimpleGraph.isNClique_one candidate
  • SimpleGraph.cliqueNum.eq_1 candidate
  • SimpleGraph.indepNum.eq_1 candidate
  • SimpleGraph.cliqueFree_two candidate
  • SimpleGraph.IsNClique.erase_of_sup_edge_of_mem candidate
  • SimpleGraph.maximumClique_exists candidate
  • SimpleGraph.IsMaximumClique.isMaximalClique candidate
  • SimpleGraph.maximumIndepSet_card_eq_indepNum candidate
  • SimpleGraph.cliqueFree_map_iff candidate
  • SimpleGraph.IsClique.insert candidate
  • SimpleGraph.CliqueFreeOn.mono candidate
  • SimpleGraph.IsClique.sdiff_of_sup_edge candidate
  • SimpleGraph.cliqueFreeOn_singleton candidate
  • SimpleGraph.IsContained.not_cliqueFree candidate
  • … and 55 more
ready to PR
54.5 55
Mathlib.AlgebraicTopology.SimplexCategory.Basic
  • SimplexCategory.δ_comp_σ_self' candidate
  • SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor candidate
  • SimplexCategory.toCat_obj candidate
  • SimplexCategory.SkeletalFunctor.isEquivalence candidate
  • SimplexCategory.intervalEdge.congr_simp candidate
  • SimplexCategory.skeletalEquivalence candidate
  • SimplexCategory.isIso_of_bijective candidate
  • SimplexCategory.δ_comp_σ_of_gt'_assoc candidate
  • SimplexCategory.skeletalFunctor_map candidate
  • SimplexCategory.skeletalFunctor.coe_map candidate
  • SimplexCategory.instBalanced candidate
  • SimplexCategory.instHasStrongEpiImages candidate
  • SimplexCategory.skeletalFunctor_obj candidate
  • SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor candidate
  • SimplexCategory.factor_δ_spec candidate
  • SimplexCategory.mkOfSucc_homToOrderHom_one candidate
  • SimplexCategory.skeletal candidate
  • SimplexCategory.eq_of_one_to_one candidate
  • SimplexCategory.δ_comp_σ_self'_assoc candidate
  • SimplexCategory.eq_comp_δ_of_not_surjective' candidate
  • SimplexCategory.exists_eq_const_of_zero candidate
  • SimplexCategory.σ.eq_1 candidate
  • SimplexCategory.const_fac_thru_zero candidate
  • SimplexCategory.isIso_iff_of_mono candidate
  • SimplexCategory.concreteCategoryHom_id candidate
  • … and 30 more
ready to PR
48.2 52
Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
  • SSet.stdSimplex.objMk_bijective candidate
  • SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred candidate
  • SSet.stdSimplex.nonDegenerateEquiv'_symm_apply_mem candidate
  • SSet.stdSimplex.faceSingletonComplIso_hom_ι candidate
  • SSet.stdSimplex.finSuccAboveOrderIsoFinset candidate
  • SSet.stdSimplex.coe_triangle_down_toOrderHom candidate
  • SSet.stdSimplex.const_down_toOrderHom candidate
  • SSet.stdSimplex.map_objEquiv_symm candidate
  • SSet.stdSimplex.orderIsoOfNonDegenerate candidate
  • SSet.stdSimplex.facePairComplIso_hom_ι_assoc candidate
  • SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_pred candidate
  • SSet.stdSimplex.objEquiv_yonedaEquiv_id candidate
  • SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply candidate
  • SSet.stdSimplex.face_obj candidate
  • SSet.stdSimplex.coe_edge_down_toOrderHom candidate
  • SSet.stdSimplex.nonDegenerateEquiv_apply_apply candidate
  • SSet.stdSimplex.objEquiv_toOrderHom_apply candidate
  • SSet.stdSimplex.obj₀Equiv_symm_apply candidate
  • SSet.stdSimplex.facePairComplIso.congr_simp candidate
  • SSet.stdSimplex.monotone_apply candidate
  • SSet.S1 candidate
  • SSet.stdSimplex.instFiniteToSSetOfSimplex candidate
  • SSet.stdSimplex.opObjEquiv_apply candidate
  • SSet.stdSimplex.objEquiv_symm_id_mem_nonDegenerate candidate
  • SSet.stdSimplex.isoNerve_hom_app_apply candidate
  • … and 27 more
ready to PR
47.1 52
Mathlib.Combinatorics.SimpleGraph.Basic
  • SimpleGraph.edgeSet_inj candidate
  • SimpleGraph.incidence_other_neighbor_edge candidate
  • SimpleGraph.incidenceSetEquivNeighborSet_apply_coe candidate
  • SimpleGraph.mk'_apply_adj candidate
  • SimpleGraph.default_def candidate
  • SimpleGraph.mem_incidenceSet candidate
  • SimpleGraph.mk.inj candidate
  • SimpleGraph.fromEdgeSet_disjoint candidate
  • aesop_graph candidate
  • SimpleGraph.completeGraph_eq_top candidate
  • SimpleGraph.notMem_neighborSet_self candidate
  • SimpleGraph.instNontrivial candidate
  • SimpleGraph.notMem_commonNeighbors_left candidate
  • SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe candidate
  • SimpleGraph.not_mem_edgeSet_of_isDiag candidate
  • SimpleGraph.IsIsolated.eq_1 candidate
  • SimpleGraph.neighborSet_eq_empty candidate
  • SimpleGraph.iInf_adj_of_nonempty candidate
  • SimpleGraph.support_mono candidate
  • SimpleGraph.le_fromEdgeSet_iff candidate
  • SimpleGraph.otherVertexOfIncident.congr_simp candidate
  • SimpleGraph.incidenceSet_inter_incidenceSet_subset candidate
  • SimpleGraph.inf_adj candidate
  • SimpleGraph.adj_incidenceSet_inter candidate
  • SimpleGraph.ne_of_adj_of_not_adj candidate
  • … and 27 more
ready to PR
44.0 44
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
  • MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc candidate
  • MeasureTheory.SimpleFunc.norm_approxOn_y₀_le candidate
  • MeasureTheory.Lp.simpleFunc.toLp.congr_simp candidate
  • MeasureTheory.Lp.simpleFunc.toLp_eq_toLp candidate
  • MeasureTheory.Lp.simpleFunc.coe_smul candidate
  • MeasureTheory.Lp.simpleFunc.toLp_zero candidate
  • MeasureTheory.Lp.simpleFunc.norm_toLp candidate
  • MeasureTheory.Lp.simpleFunc.aemeasurable candidate
  • MeasureTheory.SimpleFunc.memLp_iff_integrable candidate
  • MeasureTheory.SimpleFunc.memLp_iff_finMeasSupp candidate
  • MeasureTheory.Lp.simpleFunc.toLp_smul candidate
  • MeasureTheory.SimpleFunc.eLpNorm'_eq candidate
  • MeasureTheory.SimpleFunc.memLp_top candidate
  • MeasureTheory.Lp.simpleFunc.indicatorConst.congr_simp candidate
  • MeasureTheory.SimpleFunc.nnnorm_approxOn_le candidate
  • MeasureTheory.SimpleFunc.memLp_iff candidate
  • MeasureTheory.SimpleFunc.memLp_approxOn candidate
  • MeasureTheory.Lp.simpleFunc.stronglyMeasurable candidate
  • MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable candidate
  • MeasureTheory.Lp.simpleFunc.eq' candidate
  • MeasureTheory.Lp.simpleFunc.coeFn_zero candidate
  • MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator candidate
  • MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc candidate
  • MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm candidate
  • MeasureTheory.Lp.simpleFunc.coeFn_le candidate
  • … and 19 more
ready to PR
43.9 74
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  • SimpleGraph.ConnectedComponent.maximal_connected_induce_iff candidate
  • SimpleGraph.ConnectedComponent.instSubsingleton candidate
  • SimpleGraph.Preconnected.eq_1 candidate
  • SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen candidate
  • SimpleGraph.reachable_eq_reflTransGen candidate
  • SimpleGraph.reachable_comm candidate
  • SimpleGraph.ConnectedComponent.top_supp_eq_univ candidate
  • SimpleGraph.not_reachable_of_neighborSet_left_eq_empty candidate
  • SimpleGraph.reachable_or_compl_adj candidate
  • SimpleGraph.Reachable.nonempty_neighborSet_left candidate
  • SimpleGraph.ConnectedComponent.toSimpleGraph_adj candidate
  • SimpleGraph.reachable_deleteEdges_iff_exists_walk candidate
  • SimpleGraph.Iso.connectedComponentEquiv_refl candidate
  • SimpleGraph.ConnectedComponent.inhabited_default candidate
  • SimpleGraph.IsBridge.eq_1 candidate
  • SimpleGraph.Iso.reachable_iff candidate
  • SimpleGraph.ConnectedComponent.map_mk candidate
  • SimpleGraph.Preconnected.map candidate
  • SimpleGraph.Iso.connectedComponentEquiv_symm candidate
  • SimpleGraph.connected_bot_iff candidate
  • SimpleGraph.ConnectedComponent.isoEquivSupp candidate
  • SimpleGraph.preconnected_top candidate
  • SimpleGraph.Iso.connectedComponentEquiv_symm_apply candidate
  • SimpleGraph.ConnectedComponent.maximal_connected_induce_supp candidate
  • SimpleGraph.reachable_is_equivalence candidate
  • … and 49 more
ready to PR
42.8 66
Mathlib.Combinatorics.SimpleGraph.Copy
  • SimpleGraph.killCopies_def candidate
  • SimpleGraph.Hom.minDegree_le candidate
  • SimpleGraph.Copy.ofLE_comp candidate
  • SimpleGraph.isContained_iff_exists_le_comap candidate
  • SimpleGraph.Free.eq_1 candidate
  • SimpleGraph.compl_isIndContained_compl candidate
  • SimpleGraph.instIsPreorderIsContained candidate
  • SimpleGraph.isContained_congr_right candidate
  • SimpleGraph.labelledCopyCount_pos candidate
  • SimpleGraph.maxDegree_mono candidate
  • SimpleGraph.labelledCopyCount_eq_zero candidate
  • SimpleGraph.IsContained.mono_left candidate
  • SimpleGraph.Copy.comp_apply candidate
  • SimpleGraph.Copy.coe_ofLE candidate
  • SimpleGraph.copyCount_eq_card_image_copyToSubgraph candidate
  • SimpleGraph.Copy.isContained candidate
  • SimpleGraph.IsIndContained.of_isEmpty candidate
  • SimpleGraph.Subgraph.IsInduced.eq_1 candidate
  • SimpleGraph.«term_⊑_» candidate
  • SimpleGraph.Copy.toSubgraph_surjOn candidate
  • SimpleGraph.copyCount.eq_1 candidate
  • SimpleGraph.IsIndContained.rfl candidate
  • SimpleGraph.IsIndContained.isContained candidate
  • SimpleGraph.labelledCopyCount.eq_1 candidate
  • SimpleGraph.Copy.coe_comp candidate
  • … and 41 more
ready to PR
39.2 47
Mathlib.Combinatorics.SimpleGraph.Finite
  • SimpleGraph.edgeFinset_ssubset_edgeFinset candidate
  • SimpleGraph.neighborFinset_nonempty candidate
  • SimpleGraph.minDegree.eq_1 candidate
  • SimpleGraph.edgeFinset_subset_sym2_of_support_subset candidate
  • SimpleGraph.degree_lt_card_verts candidate
  • SimpleGraph.minDegree_le_maxDegree candidate
  • SimpleGraph.Iso.maxDegree_eq candidate
  • SimpleGraph.card_commonNeighbors_le_degree_right candidate
  • SimpleGraph.edgeSet_univ_card candidate
  • SimpleGraph.card_edgeFinset_map candidate
  • SimpleGraph.Iso.degree_eq candidate
  • SimpleGraph.Adj.degree_pos_left candidate
  • SimpleGraph.Iso.minDegree_eq candidate
  • SimpleGraph.IsRegularOfDegree.eq_1 candidate
  • SimpleGraph.maxDegree.congr_simp candidate
  • SimpleGraph.degree_eq_zero candidate
  • SimpleGraph.card_commonNeighbors_lt_card_verts candidate
  • SimpleGraph.maxDegree.eq_1 candidate
  • SimpleGraph.minDegree_top candidate
  • SimpleGraph.card_edgeFinset_induce_support candidate
  • SimpleGraph.degree_compl candidate
  • SimpleGraph.neighborFinset.eq_1 candidate
  • SimpleGraph.not_isDiag_of_mem_edgeFinset candidate
  • SimpleGraph.edgeFinset_sdiff candidate
  • SimpleGraph.nontrivial_of_degree_ne_zero candidate
  • … and 22 more
ready to PR
39.0 39
Mathlib.MeasureTheory.Integral.SetToL1
  • MeasureTheory.L1.SimpleFunc.setToL1S_smul_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_zero_left candidate
  • MeasureTheory.L1.SimpleFunc.norm_setToL1S_le candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_nonneg candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_mono_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_congr candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_smul_real candidate
  • MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_zero_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_sub candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S.eq_1 candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_add_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_neg candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_mono_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_const candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left' candidate
  • MeasureTheory.L1.SimpleFunc.setToL1S_add_left candidate
  • MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg candidate
  • … and 14 more
ready to PR
35.6 7 T30 7
Mathlib.Algebra.MonoidAlgebra.Defs
  • MonoidAlgebra.single_mul_apply_aux candidate
  • AddMonoidAlgebra.unexpander candidate
  • MonoidAlgebra.«term__[_]» candidate
  • MonoidAlgebra.mul_single_apply_aux candidate
  • AddMonoidAlgebra.«term__[_]» candidate
  • MonoidAlgebra.mul' candidate
  • MonoidAlgebra.unexpander candidate
ready to PR
33.8 43
Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  • SimpleGraph.Walk.edges_eq_zipWith_support candidate
  • SimpleGraph.Walk.ofDarts.congr_simp candidate
  • SimpleGraph.Walk.not_nil_iff candidate
  • SimpleGraph.Walk.length_ofSupport candidate
  • SimpleGraph.Walk.coe_edges_toFinset candidate
  • SimpleGraph.Walk.mem_darts_iff_fst_snd_infix_support candidate
  • SimpleGraph.Walk.mem_support_iff_exists_mem_edges candidate
  • SimpleGraph.Walk.isChain_dartAdj_cons_darts candidate
  • SimpleGraph.Walk.ofDarts_singleton candidate
  • SimpleGraph.Walk.cons.sizeOf_spec candidate
  • SimpleGraph.Walk.isChain_adj_cons_support candidate
  • SimpleGraph.Walk.ofSupport.congr_simp candidate
  • SimpleGraph.Walk.mem_darts_iff_infix_support candidate
  • SimpleGraph.Walk.cons'.congr_simp candidate
  • SimpleGraph.Walk.support_getElem_zero candidate
  • SimpleGraph.Walk.edgeSet_cons candidate
  • SimpleGraph.Walk.darts_ofDarts candidate
  • SimpleGraph.Walk.edgeSet.eq_1 candidate
  • SimpleGraph.Walk.support_getElem_length candidate
  • SimpleGraph.Walk.ofSupport_singleton candidate
  • SimpleGraph.Walk.end_mem_tail_support_of_ne candidate
  • SimpleGraph.Walk.support_nonempty candidate
  • SimpleGraph.Walk.map_fst_darts_append candidate
  • SimpleGraph.Walk.notNilRec_cons candidate
  • SimpleGraph.Walk.ofDarts_cons_cons candidate
  • … and 18 more
ready to PR
30.5 6 T30 7
Mathlib.Logic.Basic
  • LibraryNote.«fact_non-instances» candidate
  • Exists.classicalRecOn candidate
  • Classical.byContradiction' candidate
  • Classical.existsCases candidate
  • LibraryNote.decidable_namespace candidate
  • LibraryNote.decidable_arguments candidate
ready to PR
30.0 30
Mathlib.MeasureTheory.Integral.Bochner.L1
  • MeasureTheory.SimpleFunc.integral_mono candidate
  • MeasureTheory.L1.SimpleFunc.integral_eq_setToL1S candidate
  • MeasureTheory.L1.SimpleFunc.negPart.eq_1 candidate
  • MeasureTheory.L1.SimpleFunc.norm_eq_integral candidate
  • MeasureTheory.SimpleFunc.integral_nonneg candidate
  • MeasureTheory.L1.SimpleFunc.norm_Integral_le_one candidate
  • MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc candidate
  • MeasureTheory.SimpleFunc.negPart.eq_1 candidate
  • MeasureTheory.L1.SimpleFunc.integral_eq_lintegral candidate
  • MeasureTheory.SimpleFunc.integral_eq_sum_filter candidate
  • MeasureTheory.L1.SimpleFunc.integral.eq_1 candidate
  • MeasureTheory.L1.SimpleFunc.integralCLM' candidate
  • MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm candidate
  • MeasureTheory.L1.SimpleFunc.norm_integral_le_norm candidate
  • MeasureTheory.L1.SimpleFunc.integral_congr candidate
  • MeasureTheory.SimpleFunc.posPart_map_norm candidate
  • MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub candidate
  • MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral candidate
  • MeasureTheory.SimpleFunc.integral_def candidate
  • MeasureTheory.SimpleFunc.posPart.eq_1 candidate
  • MeasureTheory.SimpleFunc.posPart_sub_negPart candidate
  • MeasureTheory.SimpleFunc.negPart_map_norm candidate
  • MeasureTheory.L1.SimpleFunc.coe_negPart candidate
  • MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc candidate
  • MeasureTheory.SimpleFunc.integral_add_measure candidate
  • … and 5 more
ready to PR
29.0 29
Mathlib.Data.List.Permutation
  • List.permutationsAux_cons candidate
  • List.getElem_permutations'Aux candidate
  • List.nodup_permutations'Aux_of_notMem candidate
  • List.injective_permutations'Aux candidate
  • List.permutationsAux_append candidate
  • List.mem_permutationsAux2 candidate
  • List.perm_of_mem_permutationsAux candidate
  • List.length_foldr_permutationsAux2 candidate
  • List.length_permutationsAux candidate
  • List.length_foldr_permutationsAux2' candidate
  • List.perm_permutations'Aux_comm candidate
  • List.permutationsAux_nil candidate
  • List.permutationsAux2_snd_nil candidate
  • List.map_map_permutations'Aux candidate
  • List.permutations'Aux_eq_permutationsAux2 candidate
  • List.permutationsAux2_snd_cons candidate
  • List.mem_permutationsAux2' candidate
  • List.permutationsAux2_fst candidate
  • List.map_map_permutationsAux2 candidate
  • List.mem_permutationsAux_of_perm candidate
  • List.length_permutations'Aux candidate
  • List.get_permutations'Aux candidate
  • List.map_permutationsAux2' candidate
  • List.length_permutationsAux2 candidate
  • List.nodup_permutations'Aux_iff candidate
  • … and 4 more
ready to PR
28.6 38
Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  • SimpleGraph.Walk.dropUntil.eq_2 candidate
  • SimpleGraph.Walk.support.eq_1 candidate
  • SimpleGraph.Walk.takeUntil_append_of_mem_left candidate
  • SimpleGraph.Walk.edges_dropUntil_subset candidate
  • SimpleGraph.Walk.length_takeUntil candidate
  • SimpleGraph.Walk.drop.hcongr_6 candidate
  • SimpleGraph.Walk.isSubwalk_takeUntil candidate
  • SimpleGraph.Walk.getVert_length_takeUntil candidate
  • SimpleGraph.Walk.support.hcongr_5 candidate
  • SimpleGraph.Walk.getVert_le_length_takeUntil_eq_iff candidate
  • SimpleGraph.Walk.takeUntil_nil candidate
  • SimpleGraph.Walk.count_support_takeUntil_eq_one candidate
  • SimpleGraph.Walk.rotate.congr_simp candidate
  • SimpleGraph.Walk.getVert_lt_length_takeUntil_ne candidate
  • SimpleGraph.Walk.rotate_eq_nil candidate
  • SimpleGraph.Walk.dropUntil.eq_def candidate
  • SimpleGraph.Walk.takeUntil_eq_take candidate
  • SimpleGraph.Walk.takeUntil.eq_2 candidate
  • SimpleGraph.Walk.takeUntil.hcongr_8 candidate
  • SimpleGraph.Walk.isSubwalk_dropUntil candidate
  • SimpleGraph.Walk.dropUntil_eq_drop candidate
  • SimpleGraph.Walk.dropUntil.congr_simp candidate
  • SimpleGraph.Walk.support.eq_def candidate
  • SimpleGraph.Walk.takeUntil_cons candidate
  • SimpleGraph.Walk.takeUntil.eq_def candidate
  • … and 13 more
ready to PR
26.5 5 T30 9
Mathlib.Data.NNReal.Defs
  • NNReal.«termℝ≥0» candidate
  • Mathlib.Meta.Positivity.evalNNRealtoReal candidate
  • Mathlib.Meta.Positivity.evalRealNNAbs candidate
  • NNReal.gi candidate
  • Mathlib.Meta.Positivity.evalRealToNNReal candidate
ready to PR
25.0 67
Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  • SimpleGraph.Subgraph.Preconnected.coeSubgraph candidate
  • SimpleGraph.Subgraph.Connected.coeSubgraph candidate
  • SimpleGraph.Walk.connected_induce_support candidate
  • SimpleGraph.Subgraph.Connected.mono candidate
  • SimpleGraph.Walk.mapToSubgraph.eq_def candidate
  • SimpleGraph.Walk.toSubgraph.eq_2 candidate
  • SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj candidate
  • SimpleGraph.extend_finset_to_connected candidate
  • SimpleGraph.ConnectedComponent.spanningCoe_toSubgraph candidate
  • SimpleGraph.Reachable.coe_coeSubgraph candidate
  • SimpleGraph.Walk.toSubgraph.eq_def candidate
  • SimpleGraph.induce_pair_connected_of_adj candidate
  • SimpleGraph.Subgraph.connected_iff' candidate
  • SimpleGraph.connected_induce_union candidate
  • SimpleGraph.Walk.map.eq_2 candidate
  • SimpleGraph.Subgraph.Preconnected.degree_zero_iff candidate
  • SimpleGraph.Walk.map.eq_def candidate
  • SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint candidate
  • SimpleGraph.Subgraph.Connected.nonempty candidate
  • SimpleGraph.Walk.toSubgraph_append candidate
  • SimpleGraph.Subgraph.Connected.map candidate
  • SimpleGraph.Subgraph.top_induce_pair_connected_of_adj candidate
  • SimpleGraph.Walk.mapToSubgraph.eq_2 candidate
  • SimpleGraph.connected_induce_iff candidate
  • SimpleGraph.Subgraph.induce_union_connected candidate
  • … and 42 more
ready to PR
24.8 25
Mathlib.Geometry.Manifold.Notation
  • Manifold.Elab.findModels candidate
  • delabMDifferentiableOn candidate
  • Manifold.Elab.instInhabitedFindModelResult.default candidate
  • Manifold.«termMfderiv%__» candidate
  • Manifold.«termCMDiff[_]____» candidate
  • delabMDifferentiableAt candidate
  • Manifold.Elab.findModel candidate
  • Manifold.«termT%_» candidate
  • Manifold.Elab.instInhabitedNormedSpaceInfo.default candidate
  • Manifold.«termHasMFDerivAt[_]______» candidate
  • delabMDifferentiableWithinAt candidate
  • Manifold.termMDiff__ candidate
  • delabTotalSpace_mk candidate
  • Manifold.«termCMDiffAt[_]____» candidate
  • Manifold.Elab.findModelInner candidate
  • Manifold.«termMfderiv[_]__» candidate
  • Manifold.«termMDiffAt[_]__» candidate
  • Manifold.termMDiffAt__ candidate
  • Manifold.termCMDiff____ candidate
  • Manifold.termCMDiffAt____ candidate
  • delabTotalSpace_mk' candidate
  • delab_mfderiv candidate
  • delabMDifferentiable candidate
  • Manifold.«termHasMFDerivAt%______» candidate
  • Manifold.«termMDiff[_]__» candidate
ready to PR