inf_lemmas

In [39]: jp_list = ['le_sup_left', 'le_sup_right', 'sup_idem', 'sup_comm']                                                                      

In [40]: jp_list_full = jp_list + [name.replace('le_sup', 'inf_le').replace('sup', 'inf') for name in jp_list]                                  

In [41]: for lemma in jp_list_full: pprint([(name, lib[name].filename, lib[name].line_nb) for name in G.successors(lemma)])                     
[('ideal.map_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  460),
 ('sup_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 123),
 ('le_sup_left_of_le', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 63),
 ('submodule.mul_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/algebra_operations.lean',
  112),
 ('sup_eq_left', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 76),
 ('directed_of_mono', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 107),
 ('filter.mem_at_top_sets',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1930),
 ('monotone.le_map_sup',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  415),
 ('ideal.radical_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  353),
 ('sup_assoc', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 128),
 ('order_dual.semilattice_inf',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  439),
 ('supr_sup_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  488),
 ('continuous_sup_rng_left',
  '/home/pmassot/lean/mathlib/src/topology/order.lean',
  447),
 ('submodule.sup_smul',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  125),
 ('cauchy_seq_finset_iff_vanishing',
  '/home/pmassot/lean/mathlib/src/topology/algebra/infinite_sum.lean',
  672),
 ('dim_sup_add_dim_inf_eq',
  '/home/pmassot/lean/mathlib/src/linear_algebra/dimension.lean',
  275),
 ('linear_map.quotient_inf_equiv_sup_quotient_apply_mk',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  1814),
 ('is_noetherian_iff_well_founded',
  '/home/pmassot/lean/mathlib/src/ring_theory/noetherian.lean',
  283),
 ('emetric.inf_edist_le_Hausdorff_edist_of_mem',
  '/home/pmassot/lean/mathlib/src/topology/metric_space/hausdorff_distance.lean',
  198),
 ('measure_theory.simple_func.integral_sup_le',
  '/home/pmassot/lean/mathlib/src/measure_theory/integration.lean',
  522),
 ('linear_pmap.left_le_sup',
  '/home/pmassot/lean/mathlib/src/linear_algebra/linear_pmap.lean',
  249),
 ('supr_le_supr_of_subset',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  617),
 ('submonoid.prod_bot_sup_bot_prod',
  '/home/pmassot/lean/mathlib/src/group_theory/submonoid.lean',
  1097),
 ('le_inf_sup', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 312),
 ('linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  1819),
 ('submodule.mem_sup',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  696),
 ('emetric.exists_edist_lt_of_Hausdorff_edist_lt',
  '/home/pmassot/lean/mathlib/src/topology/metric_space/hausdorff_distance.lean',
  207),
 ('enat.sup_eq_max', '/home/pmassot/lean/mathlib/src/data/nat/enat.lean', 143),
 ('directed_of_sup', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 162),
 ('inf_sup_self', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 315),
 ('embedding_inl',
  '/home/pmassot/lean/mathlib/src/topology/constructions.lean',
  363),
 ('fixed_points.sup_le_f_of_fixed_points',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  156),
 ('add_submonoid.prod_bot_sup_bot_prod',
  '/home/pmassot/lean/mathlib/src/group_theory/submonoid.lean',
  1097),
 ('sup_lt_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 114),
 ('measure_theory.simple_func.integral_le_integral',
  '/home/pmassot/lean/mathlib/src/measure_theory/integration.lean',
  535),
 ('pnat.factor_multiset_lcm',
  '/home/pmassot/lean/mathlib/src/data/pnat/factors.lean',
  321),
 ('ideal.mem_jacobson_iff',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  566),
 ('forall_le_or_exists_lt_sup',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  142),
 ('filter.map_at_top_eq_of_gc',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  2167),
 ('bdd_above.union', '/home/pmassot/lean/mathlib/src/order/bounds.lean', 186),
 ("filter.at_top_basis'",
  '/home/pmassot/lean/mathlib/src/order/filter/bases.lean',
  256),
 ('supr_bool_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  669),
 ('submodule.smul_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  119),
 ('ideal.is_local.mem_jacobson_or_exists_inv',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  605),
 ('ennreal.supr_add_supr_of_monotone',
  '/home/pmassot/lean/mathlib/src/topology/instances/ennreal.lean',
  354),
 ('sup_le_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 72),
 ('submodule.sup_mul',
  '/home/pmassot/lean/mathlib/src/ring_theory/algebra_operations.lean',
  117),
 ('ideal.radical_eq_Inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  373),
 ('le_of_sup_eq', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 103),
 ('measurable.fst',
  '/home/pmassot/lean/mathlib/src/measure_theory/measurable_space.lean',
  545),
 ('submodule.prod_sup_prod',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  831),
 ("le_sup_left'", '/home/pmassot/lean/mathlib/src/order/lattice.lean', 54),
 ('fixed_points.next_le',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  143)]
[('ideal.map_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  460),
 ('sup_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 123),
 ('linear_pmap.right_le_sup',
  '/home/pmassot/lean/mathlib/src/linear_algebra/linear_pmap.lean',
  259),
 ('submodule.mul_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/algebra_operations.lean',
  112),
 ('continuous_sup_rng_right',
  '/home/pmassot/lean/mathlib/src/topology/order.lean',
  451),
 ('directed_of_mono', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 107),
 ('le_sup_right_of_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  66),
 ('filter.mem_at_top_sets',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1930),
 ('monotone.le_map_sup',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  415),
 ('ideal.radical_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  353),
 ('sup_assoc', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 128),
 ('order_dual.semilattice_inf',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  439),
 ('supr_sup_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  488),
 ('submodule.sup_smul',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  125),
 ('cauchy_seq_finset_iff_vanishing',
  '/home/pmassot/lean/mathlib/src/topology/algebra/infinite_sum.lean',
  672),
 ('dim_sup_add_dim_inf_eq',
  '/home/pmassot/lean/mathlib/src/linear_algebra/dimension.lean',
  275),
 ('is_noetherian_iff_well_founded',
  '/home/pmassot/lean/mathlib/src/ring_theory/noetherian.lean',
  283),
 ('measure_theory.simple_func.integral_sup_le',
  '/home/pmassot/lean/mathlib/src/measure_theory/integration.lean',
  522),
 ('le_of_inf_le_sup_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  366),
 ('submonoid.prod_bot_sup_bot_prod',
  '/home/pmassot/lean/mathlib/src/group_theory/submonoid.lean',
  1097),
 ('embedding_inr',
  '/home/pmassot/lean/mathlib/src/topology/constructions.lean',
  381),
 ('le_inf_sup', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 312),
 ('submodule.mem_sup',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  696),
 ('enat.sup_eq_max', '/home/pmassot/lean/mathlib/src/data/nat/enat.lean', 143),
 ('directed_of_sup', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 162),
 ('fixed_points.sup_le_f_of_fixed_points',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  156),
 ('add_submonoid.prod_bot_sup_bot_prod',
  '/home/pmassot/lean/mathlib/src/group_theory/submonoid.lean',
  1097),
 ('sup_lt_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 114),
 ('pnat.factor_multiset_lcm',
  '/home/pmassot/lean/mathlib/src/data/pnat/factors.lean',
  321),
 ('ideal.mem_jacobson_iff',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  566),
 ('filter.map_at_top_eq_of_gc',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  2167),
 ('bdd_above.union', '/home/pmassot/lean/mathlib/src/order/bounds.lean', 186),
 ("filter.at_top_basis'",
  '/home/pmassot/lean/mathlib/src/order/filter/bases.lean',
  256),
 ('sup_eq_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 85),
 ('supr_bool_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  669),
 ('measurable.snd',
  '/home/pmassot/lean/mathlib/src/measure_theory/measurable_space.lean',
  549),
 ('submodule.smul_sup',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  119),
 ('ideal.is_local.mem_jacobson_or_exists_inv',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  605),
 ('ennreal.supr_add_supr_of_monotone',
  '/home/pmassot/lean/mathlib/src/topology/instances/ennreal.lean',
  354),
 ('sup_le_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 72),
 ("le_sup_right'", '/home/pmassot/lean/mathlib/src/order/lattice.lean', 60),
 ('submodule.sup_mul',
  '/home/pmassot/lean/mathlib/src/ring_theory/algebra_operations.lean',
  117),
 ('ideal.radical_eq_Inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  373),
 ('sup_idem', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 118),
 ('submodule.prod_sup_prod',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  831)]
[('function.support_sup',
  '/home/pmassot/lean/mathlib/src/data/support.lean',
  65),
 ('emetric.Hausdorff_edist_self',
  '/home/pmassot/lean/mathlib/src/topology/metric_space/hausdorff_distance.lean',
  161),
 ('sup_is_idempotent',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  121)]
[('inf_sup_left', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 356),
 ('multiset.union_comm',
  '/home/pmassot/lean/mathlib/src/data/multiset.lean',
  1289),
 ('Inf_sup_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_boolean_algebra.lean',
  35),
 ('is_compl.sup_inf',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  902),
 ('compl_sup_eq_top',
  '/home/pmassot/lean/mathlib/src/order/boolean_algebra.lean',
  39),
 ('submodule.comap_map_mkq',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  1329),
 ('emetric.Hausdorff_edist_comm',
  '/home/pmassot/lean/mathlib/src/topology/metric_space/hausdorff_distance.lean',
  169),
 ('le_of_inf_le_sup_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  366),
 ('submodule.map_mkq_eq_top',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  1332),
 ('sup_left_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 139),
 ('sup_inf_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 353),
 ('is_compl.symm',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  861),
 ('sup_is_commutative',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  126)]
[('forall_le_or_exists_lt_inf',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  268),
 ('infi_inf_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  453),
 ('monotone.map_inf_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  420),
 ('is_min_filter.filter_inf',
  '/home/pmassot/lean/mathlib/src/order/filter/extr.lean',
  183),
 ('filter.comap_ne_bot_of_image_mem',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1303),
 ('linear_independent.image_subtype',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basis.lean',
  578),
 ('cSup_of_cSup_of_monotone_of_continuous',
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  1239),
 ('has_deriv_within_at.continuous_within_at',
  '/home/pmassot/lean/mathlib/src/analysis/calculus/deriv.lean',
  846),
 ('ideal.is_primary_inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  637),
 ('sup_inf_self', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 318),
 ('is_max_filter.filter_inf',
  '/home/pmassot/lean/mathlib/src/order/filter/extr.lean',
  186),
 ('lim_nhds_eq_of_closure',
  '/home/pmassot/lean/mathlib/src/topology/separation.lean',
  144),
 ('le_inf_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 203),
 ('inf_assoc', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 254),
 ('infi_inf',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  471),
 ('inf_eq_left', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 207),
 ('dim_sup_add_dim_inf_eq',
  '/home/pmassot/lean/mathlib/src/linear_algebra/dimension.lean',
  275),
 ('sup_inf_le', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 309),
 ("Inf_of_continuous'",
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  1189),
 ('pnat.factor_multiset_gcd',
  '/home/pmassot/lean/mathlib/src/data/pnat/factors.lean',
  310),
 ('binfi_inf',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  479),
 ('le_of_inf_le_sup_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  366),
 ('continuous_inf_dom_left',
  '/home/pmassot/lean/mathlib/src/topology/order.lean',
  477),
 ('infi_bool_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  674),
 ('ennreal.Sup_add',
  '/home/pmassot/lean/mathlib/src/topology/instances/ennreal.lean',
  323),
 ('image_closure_subset_closure_image',
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  805),
 ('filter.le_of_ultrafilter',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  2278),
 ('linear_pmap.le_of_eq_locus_ge',
  '/home/pmassot/lean/mathlib/src/linear_algebra/linear_pmap.lean',
  192),
 ('infi_le_infi_of_subset',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  609),
 ('cInf_of_cInf_of_monotone_of_continuous',
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  1255),
 ('ideal.radical_inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  359),
 ('dense_inducing.tendsto_extend',
  '/home/pmassot/lean/mathlib/src/topology/dense_embedding.lean',
  176),
 ('continuous.continuous_within_at',
  '/home/pmassot/lean/mathlib/src/topology/continuous_on.lean',
  420),
 ('order_dual.semilattice_sup',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  433),
 ('fixed_points.prev_le',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  132),
 ('ideal.pow_le_pow',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  306),
 ('ennreal.mul_Sup',
  '/home/pmassot/lean/mathlib/src/topology/instances/ennreal.lean',
  376),
 ('submodule.map_inf_eq_map_inf_comap',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  585),
 ('tendsto_inv_at_top_zero',
  '/home/pmassot/lean/mathlib/src/analysis/specific_limits.lean',
  116),
 ('lt_inf_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 240),
 ('inf_le_left_of_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  197),
 ("Sup_of_continuous'",
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  1163),
 ('tendsto_inf_principal_nhds_iff_of_forall_eq',
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  581),
 ('has_fderiv_within_at.continuous_within_at',
  '/home/pmassot/lean/mathlib/src/analysis/calculus/fderiv.lean',
  546),
 ('inf_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 249),
 ('has_fderiv_at.has_fderiv_within_at',
  '/home/pmassot/lean/mathlib/src/analysis/calculus/fderiv.lean',
  327),
 ('t2_iff_ultrafilter',
  '/home/pmassot/lean/mathlib/src/topology/separation.lean',
  117),
 ('fixed_points.f_le_inf_of_fixed_points',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  161),
 ("nhds_within_restrict''",
  '/home/pmassot/lean/mathlib/src/topology/continuous_on.lean',
  83),
 ('compact.adherence_nhdset',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  61),
 ('directed_of_inf', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 290),
 ('is_extr_filter.filter_inf',
  '/home/pmassot/lean/mathlib/src/order/filter/extr.lean',
  189),
 ('tendsto_prod_uniformity_fst',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/basic.lean',
  763),
 ('filter.tendsto_inf_left',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1701),
 ('is_closed_of_is_complete',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/complete_separated.lean',
  20),
 ('ennreal.sub_supr',
  '/home/pmassot/lean/mathlib/src/topology/instances/ennreal.lean',
  413),
 ('is_noetherian_submodule_left',
  '/home/pmassot/lean/mathlib/src/ring_theory/noetherian.lean',
  203),
 ('measurable_inl',
  '/home/pmassot/lean/mathlib/src/measure_theory/measurable_space.lean',
  594),
 ("mem_of_closed_of_tendsto'",
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  568)]
[('forall_le_or_exists_lt_inf',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  268),
 ('inf_le_right_of_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  200),
 ('infi_inf_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  453),
 ('has_fderiv_within_at.iterate',
  '/home/pmassot/lean/mathlib/src/analysis/calculus/fderiv.lean',
  1036),
 ('monotone.map_inf_le',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  420),
 ('is_min_on.localize',
  '/home/pmassot/lean/mathlib/src/topology/local_extr.lean',
  105),
 ('continuous_inf_dom_right',
  '/home/pmassot/lean/mathlib/src/topology/order.lean',
  481),
 ('continuous_within_at.comp',
  '/home/pmassot/lean/mathlib/src/topology/continuous_on.lean',
  391),
 ('inf_eq_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 216),
 ('compact.image_of_continuous_on',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  391),
 ('le_inf_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 203),
 ('inf_assoc', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 254),
 ('infi_inf',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  471),
 ('dim_sup_add_dim_inf_eq',
  '/home/pmassot/lean/mathlib/src/linear_algebra/dimension.lean',
  275),
 ('measurable_inr',
  '/home/pmassot/lean/mathlib/src/measure_theory/measurable_space.lean',
  596),
 ('sup_inf_le', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 309),
 ('le_of_inf_eq', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 234),
 ('pnat.factor_multiset_gcd',
  '/home/pmassot/lean/mathlib/src/data/pnat/factors.lean',
  310),
 ('binfi_inf',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  479),
 ('infi_bool_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  674),
 ('image_closure_subset_closure_image',
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  805),
 ('tendsto_prod_uniformity_snd',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/basic.lean',
  767),
 ('linear_pmap.le_of_eq_locus_ge',
  '/home/pmassot/lean/mathlib/src/linear_algebra/linear_pmap.lean',
  192),
 ('filter.tendsto_inf_right',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1705),
 ('ennreal.infi_ennreal',
  '/home/pmassot/lean/mathlib/src/data/real/ennreal.lean',
  379),
 ('ideal.radical_inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  359),
 ('dense_inducing.tendsto_extend',
  '/home/pmassot/lean/mathlib/src/topology/dense_embedding.lean',
  176),
 ('order_dual.semilattice_sup',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  433),
 ('is_extr_on.localize',
  '/home/pmassot/lean/mathlib/src/topology/local_extr.lean',
  111),
 ('submodule.map_inf_eq_map_inf_comap',
  '/home/pmassot/lean/mathlib/src/linear_algebra/basic.lean',
  585),
 ('lt_inf_iff', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 240),
 ('is_max_on.localize',
  '/home/pmassot/lean/mathlib/src/topology/local_extr.lean',
  108),
 ('inf_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 249),
 ('t2_iff_ultrafilter',
  '/home/pmassot/lean/mathlib/src/topology/separation.lean',
  117),
 ('fixed_points.f_le_inf_of_fixed_points',
  '/home/pmassot/lean/mathlib/src/order/fixed_points.lean',
  161),
 ('compact.elim_finite_subcover',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  92),
 ('compact.adherence_nhdset',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  61),
 ('directed_of_inf', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 290),
 ('inf_eq_bot_iff_le_compl',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  279),
 ('inf_idem', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 244),
 ('is_closed_of_is_complete',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/complete_separated.lean',
  20),
 ('is_noetherian_submodule_right',
  '/home/pmassot/lean/mathlib/src/ring_theory/noetherian.lean',
  208)]
[('inf_is_idempotent',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  247),
 ('disjoint_self',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  835),
 ('nhds_within_inter',
  '/home/pmassot/lean/mathlib/src/topology/continuous_on.lean',
  123),
 ('ideal.is_primary_inf',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  637),
 ('ideal.radical_pow',
  '/home/pmassot/lean/mathlib/src/ring_theory/ideal_operations.lean',
  399),
 ('function.support_inf',
  '/home/pmassot/lean/mathlib/src/data/support.lean',
  69),
 ('nhds_eq_nhds_iff',
  '/home/pmassot/lean/mathlib/src/topology/separation.lean',
  125)]
[('compl_inf_eq_bot',
  '/home/pmassot/lean/mathlib/src/order/boolean_algebra.lean',
  33),
 ('inf_infi',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  476),
 ('mem_closure_iff_ultrafilter',
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  533),
 ('Sup_inf_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_boolean_algebra.lean',
  43),
 ('compact.image_of_continuous_on',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  391),
 ('inf_left_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 265),
 ('multiset.inter_comm',
  '/home/pmassot/lean/mathlib/src/data/multiset.lean',
  1290),
 ('inf_sup_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 363),
 ('inf_is_commutative',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  252),
 ('power_series.order_add_of_order_eq',
  '/home/pmassot/lean/mathlib/src/ring_theory/power_series.lean',
  1369),
 ('is_compl.symm',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  861),
 ('compact_of_finite_subfamily_closed',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  199),
 ("filter.push_pull'",
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1424),
 ('disjoint.comm',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  817),
 ("filter.prod_comm'",
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1836),
 ('inf_eq_bot_iff_le_compl',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  279),
 ('cauchy_prod',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/cauchy.lean',
  202),
 ('nhds_order_unbounded',
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  404),
 ('filter.inf_ne_bot_iff_frequently_right',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  964),
 ('compact.inter_right',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  43)]