max_cauchy set_theory.cardinal set_theory.schroeder_bernstein set_theory.cofinality set_theory.surreal set_theory.ordinal set_theory.pgame set_theory.zfc set_theory.lists set_theory.game set_theory.ordinal_notation linear_algebra.default linear_algebra.finsupp_vector_space linear_algebra.determinant linear_algebra.dimension linear_algebra.finite_dimensional linear_algebra.basis linear_algebra.finsupp linear_algebra.basic linear_algebra.direct_sum_module linear_algebra.sesquilinear_form linear_algebra.dual linear_algebra.tensor_product linear_algebra.matrix linear_algebra.bilinear_form analysis.asymptotics analysis.convex analysis.specific_limits analysis.calculus.deriv analysis.calculus.times_cont_diff analysis.calculus.mean_value analysis.calculus.tangent_cone analysis.complex.exponential analysis.complex.polynomial analysis.normed_space.real_inner_product analysis.normed_space.basic analysis.normed_space.banach analysis.normed_space.bounded_linear_maps analysis.normed_space.operator_norm order.default order.conditionally_complete_lattice order.galois_connection order.lexicographic order.lattice order.zorn order.complete_lattice order.bounds order.bounded_lattice order.basic order.pilex order.order_iso order.complete_boolean_algebra order.liminf_limsup order.boolean_algebra order.fixed_points order.filter.partial order.filter.default order.filter.basic order.filter.filter_product order.filter.pointwise order.filter.lift algebraic_geometry.presheafed_space algebraic_geometry.stalks measure_theory.decomposition measure_theory.measurable_space measure_theory.bochner_integration measure_theory.simple_func_dense measure_theory.integration measure_theory.giry_monad measure_theory.measure_space measure_theory.outer_measure measure_theory.borel_space measure_theory.l1_space measure_theory.probability_mass_function measure_theory.ae_eq_fun measure_theory.lebesgue_measure measure_theory.category.Meas geometry.manifold.manifold logic.embedding logic.unique logic.relator logic.function logic.basic logic.relation computability.turing_machine computability.halting computability.partrec_code computability.partrec computability.primrec data.pequiv data.mv_polynomial data.vector2 data.fin data.mllist data.pfun data.prod data.rel data.finset data.semiquot data.opposite data.finmap data.string data.erased data.multiset data.finsupp data.setoid data.quot data.sum data.hash_map data.ulift data.lazy_list2 data.char data.tree data.bool data.dfinsupp data.fintype data.polynomial data.subtype data.holor data.matrix.pequiv data.matrix.basic data.buffer.basic data.analysis.topology data.analysis.filter data.fp.basic data.num.bitwise data.num.lemmas data.num.basic data.string.defs data.complex.exponential data.complex.basic data.sigma.default data.sigma.basic data.int.parity data.int.gcd data.int.basic data.int.modeq data.int.sqrt data.dlist.basic data.dlist.instances data.stream.basic data.padics.default data.padics.hensel data.padics.padic_norm data.padics.padic_numbers data.padics.padic_integers data.zsqrtd.basic data.zsqrtd.gaussian_int data.equiv.fin data.equiv.denumerable data.equiv.encodable data.equiv.local_equiv data.equiv.algebra data.equiv.basic data.equiv.functor data.equiv.nat data.equiv.list data.zmod.basic data.zmod.quadratic_reciprocity data.list.default data.list.perm data.list.defs data.list.basic data.list.min_max data.list.sort data.list.sigma data.list.alist data.set.default data.set.intervals data.set.lattice data.set.countable data.set.function data.set.basic data.set.finite data.set.disjointed data.set.enumerate data.array.lemmas data.rat.default data.rat.denumerable data.rat.order data.rat.floor data.rat.cast data.rat.basic data.seq.seq data.seq.parallel data.seq.wseq data.seq.computation data.nat.parity data.nat.prime data.nat.enat data.nat.gcd data.nat.cast data.nat.basic data.nat.modeq data.nat.dist data.nat.choose data.nat.pairing data.nat.sqrt data.nat.fib data.nat.totient data.real.cardinality data.real.pi data.real.cau_seq_completion data.real.cau_seq data.real.nnreal data.real.irrational data.real.basic data.real.hyperreal data.real.ennreal data.option.defs data.option.basic data.pnat.factors data.pnat.basic data.pnat.xgcd algebra.field_power algebra.ordered_field algebra.default algebra.ordered_ring algebra.quadratic_discriminant algebra.gcd_domain algebra.order_functions algebra.pi_instances algebra.punit_instances algebra.free algebra.field algebra.opposites algebra.module algebra.order algebra.big_operators algebra.euclidean_domain algebra.char_p algebra.floor algebra.associated algebra.archimedean algebra.group_power algebra.direct_limit algebra.pointwise algebra.ordered_group algebra.direct_sum algebra.ring algebra.char_zero algebra.continued_fractions.default algebra.continued_fractions.continuants_recurrence algebra.continued_fractions.basic algebra.continued_fractions.translations algebra.group.default algebra.group.units algebra.group.to_additive algebra.group.basic algebra.group.hom algebra.group.type_tags algebra.group.with_one algebra.group.anti_hom algebra.group.units_hom algebra.group.conj algebra.group.free_monoid algebra.category.Group algebra.category.Mon.default algebra.category.Mon.basic algebra.category.Mon.colimits algebra.category.CommRing.default algebra.category.CommRing.limits algebra.category.CommRing.adjunctions algebra.category.CommRing.basic algebra.category.CommRing.colimits topology.sequences topology.maps topology.order topology.constructions topology.compact_open topology.basic topology.opens topology.bases topology.bounded_continuous_function topology.separation topology.stone_cech topology.local_homeomorph topology.subset_properties topology.uniform_space.pi topology.uniform_space.uniform_embedding topology.uniform_space.complete_separated topology.uniform_space.cauchy topology.uniform_space.basic topology.uniform_space.separation topology.uniform_space.compare_reals topology.uniform_space.completion topology.uniform_space.abstract_completion topology.uniform_space.absolute_value topology.algebra.uniform_group topology.algebra.group_completion topology.algebra.monoid topology.algebra.module topology.algebra.uniform_ring topology.algebra.group topology.algebra.open_subgroup topology.algebra.continuous_functions topology.algebra.ring topology.algebra.infinite_sum topology.algebra.ordered topology.metric_space.lipschitz topology.metric_space.closeds topology.metric_space.emetric_space topology.metric_space.gromov_hausdorff topology.metric_space.gluing topology.metric_space.cau_seq_filter topology.metric_space.premetric_space topology.metric_space.gromov_hausdorff_realized topology.metric_space.baire topology.metric_space.basic topology.metric_space.hausdorff_distance topology.metric_space.completion topology.metric_space.isometry topology.sheaves.presheaf topology.sheaves.presheaf_of_functions topology.sheaves.stalks topology.category.UniformSpace topology.category.TopCommRing topology.category.Top.default topology.category.Top.limits topology.category.Top.epi_mono topology.category.Top.adjunctions topology.category.Top.basic topology.category.Top.opens topology.category.Top.open_nhds topology.instances.complex topology.instances.nnreal topology.instances.real topology.instances.polynomial topology.instances.ennreal ring_theory.maps ring_theory.algebra_operations ring_theory.subring ring_theory.adjoin_root ring_theory.integral_closure ring_theory.ideal_operations ring_theory.euclidean_domain ring_theory.algebra ring_theory.adjoin ring_theory.principal_ideal_domain ring_theory.free_ring ring_theory.multiplicity ring_theory.noetherian ring_theory.free_comm_ring ring_theory.polynomial ring_theory.unique_factorization_domain ring_theory.ideals ring_theory.localization ring_theory.power_series group_theory.free_abelian_group group_theory.submonoid group_theory.eckmann_hilton group_theory.group_action group_theory.sylow group_theory.abelianization group_theory.order_of_element group_theory.presented_group group_theory.quotient_group group_theory.coset group_theory.subgroup group_theory.free_group group_theory.perm.sign group_theory.perm.cycles number_theory.pell number_theory.sum_two_squares number_theory.dioph category.bifunctor category.basic category.functor category.applicative category.fold category.bitraversable.lemmas category.bitraversable.basic category.bitraversable.instances category.monad.writer category.monad.basic category.monad.cont category.traversable.default category.traversable.lemmas category.traversable.equiv category.traversable.basic category.traversable.derive category.traversable.instances meta.expr meta.coinductive_predicates meta.rb_map category_theory.yoneda category_theory.sparse category_theory.discrete_category category_theory.natural_isomorphism category_theory.natural_transformation category_theory.endomorphism category_theory.fully_faithful category_theory.full_subcategory category_theory.isomorphism category_theory.opposites category_theory.epi_mono category_theory.equivalence category_theory.pempty category_theory.groupoid category_theory.whiskering category_theory.single_obj category_theory.const category_theory.core category_theory.elements category_theory.functor category_theory.types category_theory.punit category_theory.comma category_theory.currying category_theory.conj category_theory.hom_functor category_theory.functor_category category_theory.eq_to_hom category_theory.products.default category_theory.products.bifunctor category_theory.products.basic category_theory.products.associator category_theory.adjunction.default category_theory.adjunction.limits category_theory.adjunction.fully_faithful category_theory.adjunction.basic category_theory.sums.default category_theory.sums.basic category_theory.sums.associator category_theory.monoidal.functor category_theory.monoidal.of_has_finite_products category_theory.monoidal.types category_theory.monoidal.category category_theory.limits.limits category_theory.limits.lattice category_theory.limits.opposites category_theory.limits.over category_theory.limits.types category_theory.limits.preserves category_theory.limits.cones category_theory.limits.functor_category category_theory.limits.shapes.default category_theory.limits.shapes.binary_products category_theory.limits.shapes.equalizers category_theory.limits.shapes.terminal category_theory.limits.shapes.finite_limits category_theory.limits.shapes.products category_theory.limits.shapes.pullbacks category_theory.limits.shapes.finite_products category_theory.limits.shapes.constructions.limits category_theory.limits.shapes.constructions.pullbacks category_theory.limits.shapes.constructions.finite_products category_theory.limits.shapes.constructions.limits_of_products_and_equalizers category_theory.limits.shapes.constructions.sums category_theory.monad.default category_theory.monad.limits category_theory.monad.algebra category_theory.monad.basic category_theory.monad.types category_theory.monad.adjunction category_theory.concrete_category.default category_theory.concrete_category.bundled_hom category_theory.concrete_category.basic category_theory.concrete_category.unbundled_hom category_theory.concrete_category.bundled category_theory.category.default category_theory.category.Kleisli category_theory.category.Cat category_theory.category.Groupoid category_theory.category.Rel field_theory.minimal_polynomial field_theory.mv_polynomial field_theory.splitting_field field_theory.finite field_theory.perfect_closure field_theory.finite_card field_theory.subfield tactic.default tactic.transport tactic.find tactic.cache tactic.rcases tactic.ring2 tactic.pi_instances tactic.local_cache tactic.sanity_check tactic.split_ifs tactic.linarith tactic.ext tactic.transfer tactic.push_neg tactic.reassoc_axiom tactic.generalize_proofs tactic.elide tactic.slice tactic.tidy tactic.abel tactic.wlog tactic.scc tactic.explode tactic.where tactic.replacer tactic.mk_iff_of_inductive_prop tactic.algebra tactic.simps tactic.core tactic.finish tactic.basic tactic.apply tactic.well_founded_tactics tactic.interactive tactic.fin_cases tactic.apply_fun tactic.tfae tactic.auto_cases tactic.norm_cast tactic.library_search tactic.rewrite tactic.squeeze tactic.lift tactic.doc_blame tactic.subtype_instance tactic.norm_num tactic.ring tactic.solve_by_elim tactic.simpa tactic.chain tactic.restate_axiom tactic.alias tactic.tauto tactic.localized tactic.monotonicity.default tactic.monotonicity.lemmas tactic.monotonicity.basic tactic.monotonicity.interactive tactic.rewrite_all.default tactic.rewrite_all.basic tactic.rewrite_all.congr tactic.converter.interactive tactic.converter.binders tactic.converter.old_conv tactic.omega.coeffs tactic.omega.default tactic.omega.main tactic.omega.lin_comb tactic.omega.prove_unsats tactic.omega.misc tactic.omega.find_ees tactic.omega.eq_elim tactic.omega.clause tactic.omega.term tactic.omega.find_scalars tactic.omega.int.main tactic.omega.int.preterm tactic.omega.int.dnf tactic.omega.int.form tactic.omega.nat.main tactic.omega.nat.preterm tactic.omega.nat.neg_elim tactic.omega.nat.dnf tactic.omega.nat.sub_elim tactic.omega.nat.form