/- All declarations in mathlib that
  * are a lemma/theorem but construct data
  * are a definition, but define an element of a proposition

  All automatically generated definitions and all instances are filtered out.
-/

-- topology\uniform_space\uniform_embedding.lean
#print uniform_inducing.mk' -- is a def, should be a lemma/theorem

-- topology\order.lean
#print continuous_iff_continuous_on_univ -- is a def, should be a lemma/theorem

-- topology\opens.lean
#print topological_space.opens.gc -- is a def, should be a lemma/theorem

-- topology\metric_space\isometry.lean
#print isometry.isometric_on_range -- is a lemma/theorem, should be a def

-- topology\maps.lean
#print embedding.mk' -- is a def, should be a lemma/theorem
#print dense_range.inhabited -- is a lemma/theorem, should be a def

-- topology\constructions.lean
#print homeomorph.continuous -- is a def, should be a lemma/theorem
#print dense_embedding.prod -- is a def, should be a lemma/theorem
#print dense_embedding.subtype -- is a def, should be a lemma/theorem
#print dense_inducing.prod -- is a def, should be a lemma/theorem

-- topology\algebra\group.lean
#print nhds_is_add_hom -- is a def, should be a lemma/theorem
#print nhds_is_mul_hom -- is a def, should be a lemma/theorem

-- tactic\omega\nat\preterm.lean
#print omega.nat.preterm.val_constant -- is a def, should be a lemma/theorem

-- tactic\omega\nat\form.lean
#print omega.nat.form.holds_constant -- is a def, should be a lemma/theorem

-- tactic\omega\coeffs.lean
#print omega.coeffs.val_set -- is a def, should be a lemma/theorem
#print omega.coeffs.val_except_add_eq -- is a def, should be a lemma/theorem
#print omega.coeffs.val_between_set -- is a def, should be a lemma/theorem

-- tactic\omega\clause.lean
#print omega.clause.holds_append -- is a def, should be a lemma/theorem

-- tactic\monotonicity\interactive.lean
#print tactic.interactive.apply_rel -- is a lemma/theorem, should be a def

-- tactic\interactive.lean
#print tactic.interactive.generalize_a_aux -- is a lemma/theorem, should be a def

-- tactic\chain.lean
#print tactic.tactic_script.base.inj_eq -- is a def, should be a lemma/theorem
#print tactic.tactic_script.pack_1_2.inj -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.pack_unpack -- is a def, should be a lemma/theorem
#print tactic.tactic_script.work.sizeof_spec -- is a def, should be a lemma/theorem
#print tactic.tactic_script.unpack_pack_1_2 -- is a def, should be a lemma/theorem
#print tactic.tactic_script.work.inj_eq -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.pack.list.nil.spec -- is a def, should be a lemma/theorem
#print tactic.tactic_script.sizeof_pack_1_2 -- is a def, should be a lemma/theorem
#print tactic.tactic_script.base.inj -- is a def, should be a lemma/theorem
#print tactic.tactic_script.base.sizeof_spec -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.pack.list.cons.spec -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.pack.inj -- is a def, should be a lemma/theorem
#print tactic.tactic_script.pack_unpack_1_2 -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.unpack_pack -- is a def, should be a lemma/theorem
#print tactic.tactic_script.primitive.sizeof_pack -- is a def, should be a lemma/theorem
#print tactic.tactic_script.work.inj -- is a def, should be a lemma/theorem

-- set_theory\zfc.lean
#print classical.all_definable -- is a lemma/theorem, should be a def

-- set_theory\ordinal.lean
#print cardinal.ord_eq_min -- is a def, should be a lemma/theorem
#print embedding_to_cardinal -- is a lemma/theorem, should be a def
#print ordinal.div_def -- is a def, should be a lemma/theorem

-- set_theory\lists.lean
#print lists'.subset.nil -- is a def, should be a lemma/theorem
#print lists'.subset.cons -- is a def, should be a lemma/theorem
#print lists'.subset.rec -- is a def, should be a lemma/theorem
#print lists'.subset.cases_on -- is a def, should be a lemma/theorem
#print lists.equiv.antisymm -- is a def, should be a lemma/theorem
#print lists.equiv.refl -- is a def, should be a lemma/theorem
#print lists.equiv.rec -- is a def, should be a lemma/theorem
#print lists.equiv.cases_on -- is a def, should be a lemma/theorem

-- ring_theory\power_series.lean
#print mv_power_series.is_local_ring -- is a def, should be a lemma/theorem

-- ring_theory\ideals.lean
#print ideal.zero_ne_one_of_proper -- is a def, should be a lemma/theorem

-- ring_theory\algebra.lean
#print algebra.gc -- is a def, should be a lemma/theorem

-- order\order_iso.lean
#print order_iso.prod_lex_congr -- is a lemma/theorem, should be a def
#print order_iso.sum_lex_congr -- is a lemma/theorem, should be a def
#print order_embedding.nat_lt -- is a lemma/theorem, should be a def
#print order_embedding.nat_gt -- is a lemma/theorem, should be a def

-- order\filter\pointwise.lean
#print filter.pointwise_mul_map_is_monoid_hom -- is a def, should be a lemma/theorem
#print filter.pointwise_add_map_is_add_monoid_hom -- is a def, should be a lemma/theorem

-- order\filter\partial.lean
#print filter.mem_pmap -- is a def, should be a lemma/theorem
#print filter.mem_rcomap' -- is a def, should be a lemma/theorem

-- order\filter\basic.lean
#print filter.is_lawful_monad -- is a def, should be a lemma/theorem

-- order\complete_lattice.lean
#print lattice.has_Inf_to_nonempty -- is a def, should be a lemma/theorem
#print lattice.has_Sup_to_nonempty -- is a def, should be a lemma/theorem

-- order\basic.lean
#print antisymm_of_asymm -- is a def, should be a lemma/theorem
#print well_founded.lt_sup -- is a def, should be a lemma/theorem

-- number_theory\dioph.lean
#print poly.ext -- is a def, should be a lemma/theorem
#print poly.isp -- is a def, should be a lemma/theorem
#print poly.induction -- is a def, should be a lemma/theorem

-- measure_theory\ae_eq_fun.lean
#print measure_theory.ae_eq_fun.lift_rel_mk_mk -- is a def, should be a lemma/theorem

-- logic\basic.lean
#print imp_intro -- is a lemma/theorem, should be a def
#print not.elim -- is a lemma/theorem, should be a def
#print Exists.imp -- is a def, should be a lemma/theorem
#print classical.dec_rel -- is a lemma/theorem, should be a def
#print classical.dec_eq -- is a lemma/theorem, should be a def
#print classical.dec_pred -- is a lemma/theorem, should be a def
#print classical.dec -- is a lemma/theorem, should be a def

-- linear_algebra\finsupp_vector_space.lean
#print fin_dim_vectorspace_equiv -- is a lemma/theorem, should be a def

-- group_theory\sylow.lean
#print sylow.fixed_points_mul_left_cosets_equiv_quotient -- is a lemma/theorem, should be a def

-- group_theory\free_group.lean
#print free_group.to_word.inj -- is a def, should be a lemma/theorem
#print free_group.to_word.mk -- is a def, should be a lemma/theorem

-- data\seq\computation.lean
#print computation.lift_rel_aux.ret_left -- is a def, should be a lemma/theorem
#print computation.corec_eq -- is a def, should be a lemma/theorem
#print computation.lift_rel_aux.ret_right -- is a def, should be a lemma/theorem

-- data\rat\order.lean
#print rat.nonneg_antisymm -- is a def, should be a lemma/theorem
#print rat.nonneg_add -- is a def, should be a lemma/theorem
#print rat.nonneg_total -- is a def, should be a lemma/theorem
#print rat.nonneg_mul -- is a def, should be a lemma/theorem

-- data\rat\basic.lean
#print rat.num_denom_cases_on -- is a lemma/theorem, should be a def
#print rat.num_denom_cases_on' -- is a lemma/theorem, should be a def

-- data\polynomial.lean
#print polynomial.degree_lt_wf -- is a def, should be a lemma/theorem

-- data\pfun.lean
#print pfun.fix_induction -- is a lemma/theorem, should be a def
#print roption.ext -- is a def, should be a lemma/theorem
#print pfun.ext -- is a def, should be a lemma/theorem
#print pfun.ext' -- is a def, should be a lemma/theorem
#print roption.ext' -- is a def, should be a lemma/theorem
#print pfun.mem_preimage -- is a def, should be a lemma/theorem

-- data\matrix\basic.lean
#print matrix.is_add_monoid_hom_mul_right -- is a def, should be a lemma/theorem

-- data\list\min_max.lean
#print list.minimum_singleton -- is a def, should be a lemma/theorem
#print list.minimum_aux_cons -- is a def, should be a lemma/theorem
#print list.maximum_cons -- is a def, should be a lemma/theorem
#print list.maximum_singleton -- is a def, should be a lemma/theorem
#print list.minimum_cons -- is a def, should be a lemma/theorem
#print list.maximum_aux_cons -- is a def, should be a lemma/theorem

-- data\finsupp.lean
#print finsupp.lt_wf -- is a def, should be a lemma/theorem

-- data\finset.lean
#print finset.strong_induction_on -- is a lemma/theorem, should be a def

-- data\fin.lean
#print fin.mk_val -- is a def, should be a lemma/theorem

-- data\equiv\basic.lean
#print equiv.subtype_quotient_equiv_quotient_subtype -- is a lemma/theorem, should be a def

-- data\equiv\algebra.lean
#print mul_equiv.apply_symm_apply -- is a def, should be a lemma/theorem
#print add_equiv.map_zero -- is a def, should be a lemma/theorem
#print add_equiv.map_add -- is a def, should be a lemma/theorem
#print mul_equiv.symm_apply_apply -- is a def, should be a lemma/theorem
#print mul_equiv.map_one -- is a def, should be a lemma/theorem
#print add_equiv.apply_symm_apply -- is a def, should be a lemma/theorem
#print add_equiv.symm_apply_apply -- is a def, should be a lemma/theorem
#print mul_equiv.map_mul -- is a def, should be a lemma/theorem

-- computability\turing_machine.lean
#print turing.TM2to1.stmt_st_rec -- is a lemma/theorem, should be a def

-- category_theory\natural_transformation.lean
#print category_theory.nat_trans.naturality -- is a def, should be a lemma/theorem

-- category_theory\natural_isomorphism.lean
#print category_theory.nat_iso.of_components.inv_app -- is a def, should be a lemma/theorem
#print category_theory.nat_iso.of_components.hom_app -- is a def, should be a lemma/theorem
#print category_theory.nat_iso.of_components.app -- is a def, should be a lemma/theorem

-- category_theory\monoidal\functor.lean
#print category_theory.lax_monoidal_functor.left_unitality -- is a def, should be a lemma/theorem
#print category_theory.lax_monoidal_functor.right_unitality -- is a def, should be a lemma/theorem
#print category_theory.lax_monoidal_functor.associativity -- is a def, should be a lemma/theorem
#print category_theory.lax_monoidal_functor.μ_natural -- is a def, should be a lemma/theorem

-- category_theory\monoidal\category.lean
#print category_theory.monoidal_category.triangle -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.tensor_id -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.right_unitor_naturality -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.left_unitor_naturality -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.pentagon -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.associator_naturality -- is a def, should be a lemma/theorem
#print category_theory.monoidal_category.tensor_comp -- is a def, should be a lemma/theorem

-- category_theory\monad\basic.lean
#print category_theory.monad.assoc -- is a def, should be a lemma/theorem
#print category_theory.monad.right_unit -- is a def, should be a lemma/theorem
#print category_theory.monad.left_unit -- is a def, should be a lemma/theorem

-- category_theory\monad\algebra.lean
#print category_theory.monad.algebra.hom.h -- is a def, should be a lemma/theorem
#print category_theory.monad.algebra.assoc -- is a def, should be a lemma/theorem
#print category_theory.monad.algebra.unit -- is a def, should be a lemma/theorem

-- category_theory\limits\shapes\equalizers.lean
#print category_theory.limits.fork.condition -- is a def, should be a lemma/theorem
#print category_theory.limits.cofork.condition -- is a def, should be a lemma/theorem

-- category_theory\limits\limits.lean
#print category_theory.limits.is_limit.uniq -- is a def, should be a lemma/theorem
#print category_theory.limits.is_colimit.uniq -- is a def, should be a lemma/theorem
#print category_theory.limits.is_colimit.fac -- is a def, should be a lemma/theorem
#print category_theory.limits.is_limit.fac -- is a def, should be a lemma/theorem

-- category_theory\limits\cones.lean
#print category_theory.limits.cocone_morphism.w -- is a def, should be a lemma/theorem
#print category_theory.limits.cone_morphism.w -- is a def, should be a lemma/theorem

-- category_theory\isomorphism.lean
#print category_theory.iso.hom_inv_id -- is a def, should be a lemma/theorem
#print category_theory.iso.inv_hom_id -- is a def, should be a lemma/theorem

-- category_theory\groupoid.lean
#print category_theory.groupoid.inv_comp -- is a def, should be a lemma/theorem
#print category_theory.groupoid.comp_inv -- is a def, should be a lemma/theorem

-- category_theory\functor.lean
#print category_theory.functor.map_comp -- is a def, should be a lemma/theorem
#print category_theory.functor.map_id -- is a def, should be a lemma/theorem

-- category_theory\fully_faithful.lean
#print category_theory.faithful.injectivity -- is a def, should be a lemma/theorem
#print category_theory.functor.injectivity -- is a def, should be a lemma/theorem
#print category_theory.full.witness -- is a def, should be a lemma/theorem

-- category_theory\equivalence.lean
#print category_theory.is_equivalence.functor_unit_iso_comp -- is a def, should be a lemma/theorem
#print category_theory.equivalence.functor_unit_iso_comp -- is a def, should be a lemma/theorem

-- category_theory\comma.lean
#print category_theory.comma_morphism.w -- is a def, should be a lemma/theorem

-- category_theory\category.lean
#print category_theory.category.comp_id -- is a def, should be a lemma/theorem
#print category_theory.category.id_comp -- is a def, should be a lemma/theorem
#print category_theory.category.assoc -- is a def, should be a lemma/theorem

-- category_theory\adjunction\basic.lean
#print category_theory.adjunction.core_unit_counit.left_triangle -- is a def, should be a lemma/theorem
#print category_theory.adjunction.core_unit_counit.right_triangle -- is a def, should be a lemma/theorem
#print category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right -- is a def, should be a lemma/theorem
#print category_theory.adjunction.hom_equiv_unit -- is a def, should be a lemma/theorem
#print category_theory.adjunction.hom_equiv_counit -- is a def, should be a lemma/theorem
#print category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm -- is a def, should be a lemma/theorem

-- category\traversable\equiv.lean
#print equiv.is_lawful_functor' -- is a def, should be a lemma/theorem
#print equiv.is_lawful_functor -- is a def, should be a lemma/theorem

-- algebra\ring.lean
#print is_ring_hom.of_semiring -- is a def, should be a lemma/theorem

-- algebra\pointwise.lean
#print set.singleton.is_monoid_hom -- is a def, should be a lemma/theorem
#print set.singleton.is_add_monoid_hom -- is a def, should be a lemma/theorem
#print set.singleton.is_mul_hom -- is a def, should be a lemma/theorem
#print set.singleton.is_add_hom -- is a def, should be a lemma/theorem
#print set.pointwise_mul_image_is_semiring_hom -- is a def, should be a lemma/theorem

-- algebra\ordered_field.lean
#print div_nonneg -- is a def, should be a lemma/theorem
#print div_pos -- is a def, should be a lemma/theorem
#print half_lt_self -- is a def, should be a lemma/theorem

-- algebra\order_functions.lean
#print abs_add -- is a def, should be a lemma/theorem
#print sub_abs_le_abs_sub -- is a def, should be a lemma/theorem

-- algebra\group\hom.lean
#print monoid_hom.ext -- is a def, should be a lemma/theorem
#print add_monoid_hom.map_add -- is a def, should be a lemma/theorem
#print add_monoid_hom.ext -- is a def, should be a lemma/theorem
#print add_monoid_hom.map_zero -- is a def, should be a lemma/theorem

-- algebra\group\basic.lean
#print sub_sub_cancel -- is a def, should be a lemma/theorem

-- algebra\direct_limit.lean
#print add_comm_group.direct_limit.directed_system -- is a def, should be a lemma/theorem