gistfile1.txt

/- The `generalisation_linter` linter reports: -/
/- typeclass generalisations may be possible -/
-- algebra/algebra/basic.lean
#check @algebra.id.smul_eq_mul /- _inst_1: comm_semiring ↝ has_mul -/
#check @algebra.mem_algebra_map_submonoid_of_mem /- _inst_2: comm_semiring ↝ semiring -/
#check @algebra.mul_sub_algebra_map_commutes /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_hom.map_inv /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_hom.map_div /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_equiv.map_neg /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_equiv.map_sub /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ring_hom.map_rat_algebra_map /- _inst_1: ring ↝ semiring -/
#check @ring_hom.map_rat_algebra_map /- _inst_2: ring ↝ semiring -/
#check @algebra_compatible_smul /- _inst_6: module ↝ has_scalar -/
#check @is_scalar_tower.to_smul_comm_class' /- _inst_7: is_scalar_tower ↝ smul_comm_class -/
#check @smul_algebra_smul_comm /- _inst_7: is_scalar_tower ↝ smul_comm_class -/
#check @linear_map.coe_is_scalar_tower /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @linear_map.coe_is_scalar_tower /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @linear_map.coe_restrict_scalars_eq_coe /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @linear_map.coe_restrict_scalars_eq_coe /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @linear_map.ker_restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/

-- algebra/algebra/operations.lean
#check @submodule.mem_span_mul_finite_of_mem_span_mul /- _inst_3: algebra ↝ module -/

-- algebra/algebra/spectrum.lean
#check @spectrum.mem_iff /- _inst_1: comm_ring ↝ comm_semiring -/
#check @spectrum.mem_resolvent_set_of_left_right_inverse /- _inst_1: comm_ring ↝ comm_semiring -/
#check @spectrum.mem_resolvent_set_iff /- _inst_1: comm_ring ↝ comm_semiring -/
#check @spectrum.resolvent_eq /- _inst_1: comm_ring ↝ comm_semiring -/
#check @spectrum.is_unit_resolvent /- _inst_1: comm_ring ↝ comm_semiring -/
#check @spectrum.star_mem_resolvent_set_iff /- _inst_4: star_add_monoid ↝ has_involutive_star
#check @alg_hom.mem_resolvent_set_apply /- _inst_1: comm_ring ↝ comm_semiring -/

-- algebra/algebra/subalgebra/basic.lean
#check @subalgebra.no_zero_divisors /- _inst_8: comm_ring ↝ comm_semiring -/

-- algebra/algebra/tower.lean
#check @is_scalar_tower.algebra_map_smul /- _inst_5: module ↝ has_scalar
#check @submodule.span_algebra_map_image_of_tower /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @submodule.span_algebra_map_image_of_tower /- _inst_14: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @algebra.lsmul_injective /- _inst_2: ring ↝ semiring -/

-- algebra/algebra/unitization.lean
#check @unitization.snd_coe /- _inst_1: has_zero ↝ has_coe_t -/
#check @unitization.fst_smul /- _inst_2: has_scalar ↝ has_scalar -/
#check @unitization.snd_smul /- _inst_1: has_scalar ↝ has_scalar -/
#check @unitization.coe_add /- _inst_2: add_zero_class ↝ has_add -/
#check @unitization.star_module /- _inst_4: star_add_monoid ↝ has_star -/
#check @unitization.star_module /- _inst_5: module ↝ has_scalar -/
#check @unitization.alg_hom_ext /- _inst_7: ring ↝ semiring

-- algebra/associated.lean
#check @prime /- _inst_1: comm_monoid_with_zero ↝ monoid_with_zero -/
#check @associates.bot_eq_one /- _inst_1: comm_monoid ↝ monoid -/
#check @associates.mk_one /- _inst_1: comm_monoid ↝ monoid -/
#check @associates.mk_injective /- _inst_1: comm_monoid ↝ monoid -/
#check @associates.mk_eq_zero /- _inst_1: comm_monoid_with_zero ↝ monoid_with_zero -/
#check @associates.nontrivial /- _inst_1: comm_monoid_with_zero ↝ monoid_with_zero -/
#check @associates.exists_non_zero_rep /- _inst_1: comm_monoid_with_zero ↝ monoid_with_zero -/
#check @associates.dvd_of_mk_le_mk /- _inst_1: comm_monoid_with_zero ↝ comm_monoid -/
#check @associates.mk_le_mk_of_dvd /- _inst_1: comm_monoid_with_zero ↝ comm_monoid -/
#check @associates.irreducible_iff_prime_iff /- _inst_1: cancel_comm_monoid_with_zero ↝ comm_monoid_with_zero -/
#check @dvd_not_unit.is_unit_of_irreducible_right /- _inst_1: cancel_comm_monoid_with_zero ↝ comm_monoid_with_zero -/
#check @dvd_not_unit.not_unit /- _inst_1: cancel_comm_monoid_with_zero ↝ comm_monoid_with_zero -/

-- algebra/big_operators/associated.lean
#check @associates.rel_associated_iff_map_eq_map /- _inst_1: comm_monoid ↝ monoid -/
#check @associates.exists_mem_multiset_le_of_prime /- _inst_1: cancel_comm_monoid_with_zero ↝ comm_monoid_with_zero -/
#check @prime.dvd_finsupp_prod_iff /- _inst_1: comm_monoid_with_zero ↝ has_zero -/

-- algebra/big_operators/finprod.lean
#check @mul_finsum /- _inst_3: semiring ↝ non_unital_non_assoc_semiring -/
#check @finsum_mul /- _inst_3: semiring ↝ non_unital_non_assoc_semiring -/

-- algebra/big_operators/finsupp.lean
#check @finsupp.sum_apply' /- _inst_1: add_comm_monoid ↝ has_zero -/
#check @finsupp.sum_mul /- _inst_4: non_unital_non_assoc_semiring ↝ has_zero -/
#check @finsupp.mul_sum /- _inst_4: non_unital_non_assoc_semiring ↝ has_zero -/

-- algebra/big_operators/multiset.lean
#check @multiset.dvd_sum /- _inst_1: comm_semiring ↝ non_unital_semiring -/

-- algebra/big_operators/order.lean
#check @finset.exists_lt_of_prod_lt' /- _inst_1: linear_ordered_cancel_comm_monoid ↝ canonically_linear_ordered_monoid -/
#check @finset.exists_lt_of_sum_lt /- _inst_1: linear_ordered_cancel_add_comm_monoid ↝ linear_ordered_add_comm_monoid -/

-- algebra/big_operators/pi.lean
#check @ring_hom.functions_ext /- _inst_4: semiring ↝ non_assoc_semiring -/

-- algebra/big_operators/ring.lean
#check @finset.prod_pow_eq_pow_sum /- _inst_1: comm_semiring ↝ comm_monoid -/

-- algebra/category/CommRing/basic.lean
#check @SemiRing.assoc_ring_hom /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @SemiRing.assoc_ring_hom /- _inst_2: semiring ↝ non_assoc_semiring -/

-- algebra/category/Mon/basic.lean
#check @Mon.assoc_monoid_hom /- _inst_1: monoid ↝ mul_one_class -/
#check @Mon.assoc_monoid_hom /- _inst_2: monoid ↝ mul_one_class -/
#check @AddMon.assoc_add_monoid_hom /- _inst_1: add_monoid ↝ add_zero_class -/
#check @AddMon.assoc_add_monoid_hom /- _inst_2: add_monoid ↝ add_zero_class -/

-- algebra/char_p/algebra.lean
#check @algebra.char_p_iff /- _inst_2: comm_semiring ↝ semiring -/
#check @is_fraction_ring.char_p_of_is_fraction_ring /- _inst_2: field ↝ comm_ring -/
#check @is_fraction_ring.char_zero_of_is_fraction_ring /- _inst_5: char_zero ↝ char_p -/

-- algebra/char_p/basic.lean
#check @ring_char.eq_zero /- _inst_2: char_zero ↝ char_p -/
#check @eq_iff_modeq_int /- _inst_1: ring ↝ non_assoc_ring -/
#check @char_p.neg_one_ne_one /- _inst_1: ring ↝ non_assoc_ring -/
#check @char_p.char_p_to_char_zero /- _inst_1: ring ↝ non_assoc_ring -/
#check @char_p.cast_eq_mod /- _inst_1: ring ↝ non_assoc_semiring -/
#check @char_p.false_of_nontrivial_of_char_one /- _inst_3: char_p ↝ subsingleton -/
#check @char_p_of_ne_zero /- _inst_1: comm_ring ↝ non_assoc_ring -/
#check @char_p_of_prime_pow_injective /- _inst_1: comm_ring ↝ ring -/
#check @nat.lcm.char_p /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @nat.lcm.char_p /- _inst_2: semiring ↝ non_assoc_semiring -/

-- algebra/char_p/exp_char.lean
#check @char_prime_of_ne_zero /- _inst_1: semiring ↝ non_assoc_semiring -/

-- algebra/char_p/invertible.lean
#check @not_ring_char_dvd_of_invertible /- _inst_1: field ↝ euclidean_domain -/

-- algebra/char_p/pi.lean
#check @char_p.pi' /- _inst_1: comm_ring ↝ semiring -/

-- algebra/char_p/subring.lean
#check @char_p.subsemiring /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @char_p.subring' /- _inst_1: comm_ring ↝ ring -/

-- algebra/char_p/two.lean
#check @char_two.two_eq_zero /- _inst_1: semiring ↝ non_assoc_semiring -/

-- algebra/char_zero.lean
#check @add_self_eq_zero /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @nat_mul_inj /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_hom.char_zero /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.char_zero /- _inst_2: semiring ↝ non_assoc_semiring -/

-- algebra/continued_fractions/basic.lean
#check @generalized_continued_fraction.pair.has_coe_to_generalized_continued_fraction_pair /- _inst_1: has_coe ↝ has_lift_t -/

-- algebra/continued_fractions/computation/basic.lean
#check @generalized_continued_fraction.int_fract_pair.has_coe_to_int_fract_pair /- _inst_1: has_coe ↝ has_lift_t -/
#check @generalized_continued_fraction.int_fract_pair.of /- _inst_1: linear_ordered_field ↝ linear_ordered_ring -/

-- algebra/cubic_discriminant.lean
#check @cubic.map /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @cubic.map /- _inst_2: semiring ↝ non_assoc_semiring -/
#check @cubic.map_roots /- _inst_1: comm_ring ↝ semiring -/

-- algebra/direct_limit.lean
#check @module.directed_system.map_self /- _inst_1: ring ↝ semiring -/
#check @module.directed_system.map_map /- _inst_1: ring ↝ semiring -/
#check @module.direct_limit /- _inst_2: preorder ↝ has_le -/
#check @module.direct_limit.totalize /- _inst_1: ring ↝ semiring -/
#check @module.direct_limit.totalize /- _inst_2: preorder ↝ has_le -/
#check @ring.direct_limit /- _inst_2: preorder ↝ has_le -/

-- algebra/direct_sum/basic.lean
#check @direct_sum.add_hom_ext /- _inst_2: add_monoid ↝ add_zero_class -/
#check @direct_sum.from_add_monoid /- _inst_2: add_comm_monoid ↝ add_zero_class -/

-- algebra/direct_sum/ring.lean
#check @direct_sum.ring_hom_ext' /- _inst_5: semiring ↝ non_assoc_semiring -/

-- algebra/divisibility.lean
#check @semigroup_has_dvd /- _inst_1: semigroup ↝ has_mul -/
#check @dvd_not_unit /- _inst_1: comm_monoid_with_zero ↝ monoid_with_zero -/

-- algebra/euclidean_domain.lean

-- algebra/field_power.lean
#check @zpow_eq_zero_iff /- _inst_1: linear_ordered_field ↝ group_with_zero -/
#check @zpow_two_nonneg /- _inst_1: linear_ordered_field ↝ linear_ordered_ring -/
#check @zpow_two_pos_of_ne_zero /- _inst_1: linear_ordered_field ↝ linear_ordered_ring -/
#check @rat.cast_zpow /- _inst_1: field ↝ division_ring -/

-- algebra/free_monoid.lean
#check @free_add_monoid.hom_eq /- _inst_1: add_monoid ↝ add_zero_class -/
#check @free_monoid.hom_eq /- _inst_1: monoid ↝ mul_one_class -/

-- algebra/gcd_monoid/basic.lean
#check @norm_unit_eq_one /- _inst_2: unique ↝ normalization_monoid -/
#check @normalize_eq /- _inst_2: unique ↝ normalization_monoid -/

-- algebra/geom_sum.lean
#check @geom_sum₂_self /- _inst_1: comm_ring ↝ semiring -/

-- algebra/graded_monoid.lean
#check @set_like.is_homogeneous /- _inst_1: set_like ↝ has_mem -/

-- algebra/group/basic.lean
#check @bit0_zero /- _inst_1: add_monoid ↝ add_zero_class -/
#check @left_inverse_inv /- _inst_2: group ↝ has_involutive_inv -/
#check @left_inverse_neg /- _inst_2: add_group ↝ has_involutive_neg -/
#check @div_inv_eq_mul /- _inst_1: group ↝ group_with_zero -/
#check @add_sub /- _inst_1: add_group ↝ sub_neg_monoid -/
#check @mul_div /- _inst_1: group ↝ div_inv_monoid -/
#check @div_eq_inv_mul' /- _inst_1: comm_group ↝ comm_group_with_zero -/
#check @div_right_comm' /- _inst_1: comm_group ↝ comm_group_with_zero -/

-- algebra/group/conj.lean
#check @is_conj_one_right /- _inst_1: cancel_monoid ↝ right_cancel_monoid -/

-- algebra/group/defs.lean
#check @group.to_monoid /- _inst_1: group ↝ monoid -/
#check @add_group.to_add_monoid /- _inst_1: add_group ↝ add_monoid -/

-- algebra/group_power/lemmas.lean
#check @nsmul_eq_mul' /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @bit0_mul /- _inst_1: ring ↝ non_unital_non_assoc_ring -/
#check @mul_bit0 /- _inst_1: ring ↝ non_unital_non_assoc_ring -/

-- algebra/hom/iterate.lean
#check @monoid_hom.coe_pow /- _inst_5: comm_monoid ↝ mul_one_class -/
#check @monoid.End.coe_pow /- _inst_1: monoid ↝ mul_one_class -/
#check @add_monoid.End.coe_pow /- _inst_1: add_monoid ↝ add_zero_class -/
#check @ring_hom.coe_pow /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_one /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_zero /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_add /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_mul /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_smul /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @ring_hom.iterate_map_sub /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_hom.iterate_map_neg /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_hom.iterate_map_zsmul /- _inst_1: ring ↝ non_assoc_ring -/

-- algebra/homology/additive.lean
#check @homological_complex.cycles_additive /- _inst_4: category_theory.limits.has_equalizers ↝ category_theory.limits.has_kernels -/

-- algebra/homology/differential_object.lean
#check @homological_complex.d_eq_to_hom /- _inst_1: add_comm_group ↝ add_right_cancel_semigroup -/

-- algebra/homology/exact.lean
#check @category_theory.exact_kernel_subobject_arrow /- _inst_4: category_theory.limits.has_equalizers ↝ category_theory.limits.has_kernels -/

-- algebra/homology/homology.lean
#check @boundaries_to_cycles_naturality /- _inst_4: category_theory.limits.has_equalizers ↝ category_theory.limits.has_kernels -/

-- algebra/invertible.lean
#check @inv_of_two_add_inv_of_two /- _inst_1: semiring ↝ non_assoc_semiring -/

-- algebra/lie/basic.lean
#check @lie_hom.lie_apply /- _inst_7: lie_module ↝ lie_ring_module -/
#check @lie_hom.lie_apply /- _inst_11: lie_module ↝ lie_ring_module -/

-- algebra/lie/cartan_subalgebra.lean
#check @lie_algebra.top_is_cartan_subalgebra_of_nilpotent /- _inst_4: lie_algebra.is_nilpotent ↝ lie_algebra.is_nilpotent -/

-- algebra/lie/classical.lean
#check @lie_algebra.orthogonal.Pso /- _inst_5: comm_ring ↝ mul_zero_one_class -/
#check @lie_algebra.orthogonal.JD /- _inst_5: comm_ring ↝ mul_zero_one_class -/

-- algebra/lie/of_associative.lean
#check @module.End.lie_ring_module /- _inst_2: comm_ring ↝ semiring -/

-- algebra/lie/subalgebra.lean
#check @lie_subalgebra.is_central_scalar /- _inst_7: module ↝ has_scalar -/
#check @lie_subalgebra.is_scalar_tower /- _inst_6: module ↝ has_scalar -/

-- algebra/lie/submodule.lean
#check @lie_submodule.is_central_scalar /- _inst_11: module ↝ has_scalar -/

-- algebra/module/equiv.lean
#check @linear_equiv.trans /- _inst_14: ring_hom_comp_triple ↝ -/

-- algebra/module/linear_map.lean
#check @linear_map.smul_apply /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @linear_map.coe_smul /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @linear_map.smul_comm_class /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @linear_map.smul_comm_class /- _inst_19: smul_comm_class ↝ has_scalar -/
#check @linear_map.is_scalar_tower /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @linear_map.is_scalar_tower /- _inst_19: smul_comm_class ↝ has_scalar -/
#check @linear_map.is_central_scalar /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @linear_map.smul_comp /- _inst_16: smul_comm_class ↝ has_scalar -/
#check @module.End.smul_comm_class /- _inst_10: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @module.End.smul_comm_class' /- _inst_10: is_scalar_tower ↝ smul_comm_class -/

-- algebra/module/submodule.lean
#check @submodule.not_mem_of_ortho /- _inst_2: is_domain ↝ nontrivial -/
#check @subspace /- _inst_1: field ↝ semiring -/
#check @subspace /- _inst_2: add_comm_group ↝ add_comm_monoid -/

-- algebra/module/submodule_pointwise.lean
#check @submodule.smul_le_self_of_tower /- _inst_8: module ↝ has_scalar

-- algebra/module/torsion.lean
#check @module.is_torsion_by /- _inst_1: comm_semiring ↝ semiring -/
#check @module.is_torsion_by /- _inst_3: module ↝ has_scalar -/
#check @module.is_torsion' /- _inst_2: add_comm_monoid ↝ has_zero -/
#check @module.is_torsion /- _inst_1: comm_semiring ↝ semiring -/
#check @module.is_torsion /- _inst_3: module ↝ has_scalar -/

-- algebra/monoid_algebra/basic.lean
#check @monoid_algebra /- _inst_1: semiring ↝ has_zero -/
#check @monoid_algebra.has_scalar /- _inst_3: distrib_mul_action ↝ has_scalar -/
#check @monoid_algebra.has_scalar /- _inst_4: has_faithful_scalar ↝ has_faithful_scalar -/
#check @monoid_algebra.has_scalar /- _inst_5: nonempty ↝ has_faithful_scalar -/
#check @monoid_algebra.comap_distrib_mul_action_self /- _inst_1: group ↝ monoid -/
#check @monoid_algebra.ring_hom_ext /- _inst_2: monoid ↝ mul_one_class -/
#check @monoid_algebra.ring_hom_ext /- _inst_3: semiring ↝ non_assoc_semiring -/
#check @monoid_algebra.induction_on /- _inst_2: monoid ↝ mul_one_class -/
#check @add_monoid_algebra /- _inst_1: semiring ↝ has_zero -/
#check @add_monoid_algebra.has_scalar /- _inst_3: distrib_mul_action ↝ has_scalar -/
#check @add_monoid_algebra.has_scalar /- _inst_4: has_faithful_scalar ↝ has_faithful_scalar -/
#check @add_monoid_algebra.has_scalar /- _inst_5: nonempty ↝ has_faithful_scalar -/
#check @add_monoid_algebra.induction_on /- _inst_2: add_monoid ↝ add_zero_class -/

-- algebra/ne_zero.lean
#check @ne_zero.invertible /- _inst_1: monoid_with_zero ↝ mul_zero_one_class -/
#check @ne_zero.coe_trans /- _inst_2: has_coe ↝ has_lift_t -/
#check @ne_zero.coe_trans /- _inst_3: has_coe_t ↝ has_lift_t -/
#check @ne_zero.trans /- _inst_2: has_coe ↝ has_lift_t -/
#check @ne_zero.trans /- _inst_3: has_coe_t ↝ has_lift_t -/

-- algebra/order/absolute_value.lean
#check @absolute_value.sub_le /- _inst_2: ordered_ring ↝ ordered_semiring -/
#check @absolute_value.map_sub_eq_zero_iff /- _inst_2: ordered_ring ↝ ordered_semiring -/
#check @absolute_value.map_one /- _inst_2: linear_ordered_ring ↝ linear_ordered_field -/
#check @is_absolute_value.abv_one /- _inst_1: linear_ordered_comm_ring ↝ linear_ordered_field -/
#check @is_absolute_value.abv_sub_le /- _inst_1: linear_ordered_field ↝ ordered_semiring -/
#check @is_absolute_value.sub_abv_le_abv_sub /- _inst_1: linear_ordered_field ↝ ordered_ring -/

-- algebra/order/algebra.lean
#check @linear_ordered_comm_ring.to_ordered_smul /- _inst_1: linear_ordered_comm_ring ↝ linear_ordered_semiring -/

-- algebra/order/floor.lean
#check @nat.le_floor_iff /- _inst_1: linear_ordered_semiring ↝ ordered_semiring -/
#check @nat.gc_ceil_coe /- _inst_1: linear_ordered_semiring ↝ ordered_semiring -/

-- algebra/order/group.lean
#check @le_div_iff_mul_le' /- _inst_3: covariant_class ↝ covariant_class -/
#check @le_sub_iff_add_le' /- _inst_3: covariant_class ↝ covariant_class -/
#check @div_le_iff_le_mul' /- _inst_3: covariant_class ↝ covariant_class -/
#check @sub_le_iff_le_add' /- _inst_3: covariant_class ↝ covariant_class -/
#check @lt_sub_iff_add_lt' /- _inst_3: covariant_class ↝ covariant_class -/
#check @lt_div_iff_mul_lt' /- _inst_3: covariant_class ↝ covariant_class -/
#check @sub_lt_iff_lt_add' /- _inst_3: covariant_class ↝ covariant_class -/
#check @div_lt_iff_lt_mul' /- _inst_3: covariant_class ↝ covariant_class -/
#check @le_of_forall_pos_lt_add /- _inst_3: covariant_class ↝ covariant_class -/
#check @le_of_forall_one_lt_lt_mul /- _inst_3: covariant_class ↝ covariant_class -/
#check @le_of_forall_pos_le_add /- _inst_3: covariant_class ↝ covariant_class -/
#check @le_of_forall_one_lt_le_mul /- _inst_3: covariant_class ↝ covariant_class -/
#check @abs_lt /- _inst_3: covariant_class ↝ covariant_class -/
#check @abs_lt /- _inst_4: covariant_class ↝ covariant_class -/

-- algebra/order/lattice_group.lean
#check @lattice_ordered_comm_group.has_zero_lattice_has_pos_part /- _inst_1: lattice ↝ has_sup -/
#check @lattice_ordered_comm_group.has_zero_lattice_has_pos_part /- _inst_2: add_comm_group ↝ has_zero -/
#check @lattice_ordered_comm_group.has_one_lattice_has_pos_part /- _inst_1: lattice ↝ has_sup -/
#check @lattice_ordered_comm_group.has_one_lattice_has_pos_part /- _inst_2: comm_group ↝ has_one -/
#check @lattice_ordered_comm_group.has_one_lattice_has_neg_part /- _inst_1: lattice ↝ has_sup
#check @lattice_ordered_comm_group.has_zero_lattice_has_neg_part /- _inst_1: lattice ↝ has_sup
#check @lattice_ordered_comm_group.le_abs /- _inst_1: lattice ↝ semilattice_sup
#check @lattice_ordered_comm_group.le_mabs /- _inst_1: lattice ↝ semilattice_sup
#check @lattice_ordered_comm_group.inv_le_abs /- _inst_1: lattice ↝ semilattice_sup
#check @lattice_ordered_comm_group.neg_le_abs /- _inst_1: lattice ↝ semilattice_sup
#check @lattice_ordered_comm_group.abs_inv_comm /- _inst_1: lattice ↝ semilattice_sup
#check @lattice_ordered_comm_group.abs_neg_comm /- _inst_1: lattice ↝ semilattice_sup

-- algebra/order/monoid.lean
#check @with_zero.zero_le /- _inst_1: partial_order ↝ preorder -/

-- algebra/order/monoid_lemmas.lean
#check @mul_eq_mul_iff_eq_and_eq /- _inst_3: semigroup ↝ has_mul -/
#check @add_eq_add_iff_eq_and_eq /- _inst_3: add_semigroup ↝ has_add -/
#check @le_add_of_nonneg_left /- _inst_1: preorder ↝ has_le -/
#check @le_mul_of_one_le_left' /- _inst_1: preorder ↝ has_le -/
#check @mul_le_of_le_one_left' /- _inst_1: preorder ↝ has_le -/
#check @add_le_of_nonpos_left /- _inst_1: preorder ↝ has_le -/
#check @lt_mul_of_one_lt_left' /- _inst_1: preorder ↝ has_lt -/
#check @lt_add_of_pos_left /- _inst_1: preorder ↝ has_lt -/

-- algebra/order/ring.lean
#check @add_one_le_two_mul /- _inst_2: semiring ↝ non_assoc_semiring -/

-- algebra/order/sub.lean
#check @tsub_le_iff_right /- _inst_1: preorder ↝ has_le -/
#check @tsub_le_tsub_left /- _inst_5: covariant_class ↝ covariant_class -/
#check @tsub_le_tsub_add_tsub /- _inst_5: covariant_class ↝ covariant_class -/
#check @add_monoid_hom.le_map_tsub /- _inst_2: add_comm_monoid ↝ add_zero_class -/
#check @add_monoid_hom.le_map_tsub /- _inst_6: add_comm_monoid ↝ add_zero_class -/
#check @add_tsub_add_eq_tsub_right /- _inst_5: covariant_class ↝ covariant_class -/
#check @add_tsub_add_eq_tsub_right /- _inst_6: contravariant_class ↝ contravariant_class -/
#check @lt_tsub_iff_right /- _inst_2: add_comm_semigroup ↝ has_add -/

-- algebra/periodic.lean
#check @function.antiperiodic.periodic /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @function.antiperiodic.periodic /- _inst_2: add_group ↝ has_involutive_neg -/
#check @function.antiperiodic.sub_eq /- _inst_2: add_group ↝ has_involutive_neg -/
#check @function.antiperiodic.sub_eq' /- _inst_2: add_group ↝ has_neg -/
#check @function.antiperiodic.add /- _inst_2: add_group ↝ has_involutive_neg -/
#check @function.periodic.add_antiperiod /- _inst_2: add_group ↝ has_involutive_neg -/

-- algebra/polynomial/group_ring_action.lean
#check @prod_X_sub_smul /- _inst_5: mul_semiring_action ↝ mul_action -/

-- algebra/quandle.lean
#check @rack.self_distrib /- _inst_1: rack ↝ shelf -/
#check @rack.is_involutory /- _inst_2: rack ↝ shelf -/
#check @rack.is_abelian /- _inst_2: rack ↝ shelf -/

-- algebra/quaternion.lean
#check @quaternion_algebra.has_coe_t /- _inst_1: comm_ring ↝ has_zero -/
#check @quaternion_algebra.has_zero /- _inst_1: comm_ring ↝ has_zero -/
#check @quaternion_algebra.has_one /- _inst_1: comm_ring ↝ mul_zero_one_class -/
#check @quaternion_algebra.has_add /- _inst_1: comm_ring ↝ has_add -/
#check @quaternion_algebra.has_neg /- _inst_1: comm_ring ↝ has_neg -/
#check @quaternion_algebra.has_sub /- _inst_1: comm_ring ↝ has_sub -/

-- algebra/regular/basic.lean
#check @is_regular_one /- _inst_1: monoid ↝ mul_one_class -/

-- algebra/regular/smul.lean
#check @is_smul_regular.of_smul_eq_one /- _inst_4: mul_action_with_zero ↝ has_scalar -/
#check @is_smul_regular.of_smul_eq_one /- _inst_5: mul_action_with_zero ↝ has_scalar

-- algebra/ring/basic.lean
#check @bit0_eq_two_mul /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @succ_ne_self /- _inst_1: ring ↝ non_assoc_ring -/
#check @is_regular_of_ne_zero' /- _inst_1: ring ↝ non_unital_non_assoc_ring -/
#check @is_domain.to_cancel_monoid_with_zero /- _inst_2: is_domain ↝ no_zero_divisors -/

-- algebra/ring/boolean_ring.lean
#check @boolean_ring.has_inf /- _inst_1: boolean_ring ↝ has_mul -/

-- algebra/ring/equiv.lean
#check @ring_equiv.map_neg /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_equiv.map_neg /- _inst_2: ring ↝ non_assoc_ring -/
#check @ring_equiv.map_sub /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_equiv.map_sub /- _inst_2: ring ↝ non_assoc_ring -/

-- algebra/ring/prod.lean
#check @ring_hom.prod_comp_prod_map /- _inst_1: non_assoc_semiring ↝ mul_one_class -/
#check @ring_hom.prod_comp_prod_map /- _inst_2: non_assoc_semiring ↝ mul_one_class -/
#check @ring_hom.prod_comp_prod_map /- _inst_3: non_assoc_semiring ↝ mul_one_class -/
#check @ring_hom.prod_comp_prod_map /- _inst_4: non_assoc_semiring ↝ mul_one_class -/
#check @ring_hom.prod_comp_prod_map /- _inst_5: non_assoc_semiring ↝ mul_one_class -/

-- algebra/ring_quot.lean
#check @ring_quot.ring_quot_ext /- _inst_5: semiring ↝ non_assoc_semiring -/

-- algebra/squarefree.lean
#check @squarefree.of_mul_left /- _inst_1: comm_monoid ↝ monoid -/
#check @squarefree_of_dvd_of_squarefree /- _inst_1: comm_monoid ↝ monoid -/

-- algebra/star/self_adjoint.lean
#check @self_adjoint.coe_smul /- _inst_2: has_trivial_star ↝ has_scalar -/
#check @self_adjoint.coe_smul /- _inst_6: star_module ↝ has_scalar -/
#check @skew_adjoint.coe_smul /- _inst_2: has_trivial_star ↝ has_scalar -/
#check @skew_adjoint.coe_smul /- _inst_7: star_module ↝ has_scalar -/
#check @is_star_normal_star_self /- _inst_2: star_semigroup ↝ has_involutive_star -/
#check @has_trivial_star.is_star_normal /- _inst_2: star_semigroup ↝ has_star -/
#check @comm_monoid.is_star_normal /- _inst_2: star_semigroup ↝ has_star -/

-- algebra/triv_sq_zero_ext.lean
#check @triv_sq_zero_ext.fst_smul /- _inst_2: has_scalar ↝ has_scalar -/
#check @triv_sq_zero_ext.snd_smul /- _inst_1: has_scalar ↝ has_scalar -/
#check @triv_sq_zero_ext.inr_add /- _inst_2: add_zero_class ↝ has_add -/

-- algebra/tropical/basic.lean
#check @tropical.untrop_zpow /- _inst_1: add_group ↝ sub_neg_monoid -/
#check @tropical.trop_zsmul /- _inst_1: add_group ↝ sub_neg_monoid -/
#check @tropical.covariant_swap_mul_lt /- _inst_1: preorder ↝ has_lt -/
#check @tropical.mul_eq_zero_iff /- _inst_2: linear_ordered_add_comm_monoid ↝ has_add -/

-- algebraic_geometry/prime_spectrum/basic.lean
#check @prime_spectrum /- _inst_1: comm_ring ↝ semiring -/

-- algebraic_geometry/prime_spectrum/noetherian.lean
#check @prime_spectrum.exists_prime_spectrum_prod_le /- _inst_2: is_noetherian_ring ↝ is_noetherian -/
#check @prime_spectrum.exists_prime_spectrum_prod_le /- _inst_5: is_noetherian_ring ↝ is_noetherian -/

-- algebraic_topology/simplicial_object.lean
#check @category_theory.simplicial_object.category_theory.limits.has_limits /- _inst_2: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.simplicial_object.category_theory.limits.has_colimits /- _inst_2: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.simplicial_object.truncated.category_theory.limits.has_limits /- _inst_2: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.simplicial_object.truncated.category_theory.limits.has_colimits /- _inst_2: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.cosimplicial_object.category_theory.limits.has_limits /- _inst_2: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.cosimplicial_object.category_theory.limits.has_colimits /- _inst_2: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.cosimplicial_object.truncated.category_theory.limits.has_limits /- _inst_2: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.cosimplicial_object.truncated.category_theory.limits.has_colimits /- _inst_2: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/

-- analysis/asymptotics/asymptotics.lean
#check @asymptotics.is_O_with.weaken /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_of_subsingleton /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_of_subsingleton /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_norm_right /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_norm_left /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_neg_right /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_neg_left /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with.prod_left_same /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_O_with.prod_left_fst /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_O_with.prod_left_snd /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_O.prod_left_fst /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_O.prod_left_snd /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_o.prod_left_fst /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_o.prod_left_snd /- _inst_6: normed_group ↝ has_norm -/
#check @asymptotics.is_O_with.eq_zero_imp /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with.add /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o.add_add /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_zero /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_zero /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_zero /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_zero /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_zero' /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_refl_left /- _inst_5: normed_group ↝ has_norm -/
#check @asymptotics.is_O_with_zero_right_iff /- _inst_5: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_const_iff /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_const_of_tendsto /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_o_one_iff /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_one_of_tendsto /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with_const_mul_self /- _inst_7: normed_ring ↝ non_unital_semi_normed_ring -/
#check @asymptotics.is_O_with_self_const_mul /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_self_const_mul /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_const_mul_left_iff /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_o_const_mul_left_iff /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O.const_mul_right /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_const_mul_right_iff /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_o.const_mul_right /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_o_const_mul_right_iff /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with.mul /- _inst_7: normed_ring ↝ non_unital_semi_normed_ring -/
#check @asymptotics.is_O_with.mul /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with.inv_rev /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with.inv_rev /- _inst_10: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with.eventually_mul_div_cancel /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O_with_of_eq_mul /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.div_is_bounded_under_of_is_O /- _inst_9: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_o_norm_pow_norm_pow /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with.right_le_sub_of_lt_1 /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_cofinite_iff /- _inst_4: normed_group ↝ semi_normed_group -/
#check @asymptotics.is_O_with_pi /- _inst_5: normed_group ↝ semi_normed_group -/
#check @summable_of_is_O /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/asymptotics/specific_asymptotics.lean
#check @filter.is_bounded_under.is_o_sub_self_inv /- _inst_1: normed_field ↝ normed_division_ring -/
#check @asymptotics.is_O.trans_tendsto_norm_at_top /- _inst_1: normed_linear_ordered_field ↝ normed_group -/

-- analysis/asymptotics/superpolynomial_decay.lean
#check @asymptotics.superpolynomial_decay_iff_norm_tendsto_zero /- _inst_1: normed_linear_ordered_field ↝ semi_normed_comm_ring -/

-- analysis/box_integral/basic.lean
#check @box_integral.integral_sum /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/calculus/fderiv.lean
#check @has_fderiv_at_filter /- _inst_3: normed_space ↝ module -/
#check @has_fderiv_at_filter /- _inst_5: normed_space ↝ module -/
#check @has_strict_fderiv_at /- _inst_3: normed_space ↝ module -/
#check @has_strict_fderiv_at /- _inst_5: normed_space ↝ module -/
#check @has_strict_fderiv_at.const_smul /- _inst_12: smul_comm_class ↝ module -/
#check @has_strict_fderiv_at.const_smul /- _inst_13: has_continuous_const_smul ↝ module -/
#check @has_fderiv_at_filter.const_smul /- _inst_12: smul_comm_class ↝ module -/
#check @has_fderiv_at_filter.const_smul /- _inst_13: has_continuous_const_smul ↝ module -/
#check @has_fderiv_at_filter_real_equiv /- _inst_3: normed_group ↝ semi_normed_group -/
#check @has_strict_fderiv_at.restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_strict_fderiv_at.restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at_filter.restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at_filter.restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at.restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at.restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_within_at.restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_within_at.restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_within_at_of_restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_within_at_of_restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at_of_restrict_scalars /- _inst_7: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @has_fderiv_at_of_restrict_scalars /- _inst_11: is_scalar_tower ↝ linear_map.compatible_smul -/

-- analysis/calculus/fderiv_measurable.lean
#check @fderiv_measurable_aux.A /- _inst_3: normed_space ↝ module -/
#check @fderiv_measurable_aux.A /- _inst_5: normed_space ↝ module -/

-- analysis/calculus/inverse.lean
#check @approximates_linear_on /- _inst_3: normed_space ↝ module -/
#check @approximates_linear_on /- _inst_5: normed_space ↝ module -/

-- analysis/calculus/local_extr.lean
#check @pos_tangent_cone_at /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/calculus/mean_value.lean
#check @image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary /- _inst_5: normed_group ↝ semi_normed_group -/

-- analysis/calculus/tangent_cone.lean
#check @tangent_cone_at /- _inst_3: module ↝ has_scalar -/
#check @tangent_cone_at.lim_zero /- _inst_1: nondiscrete_normed_field ↝ normed_field
#check @mem_tangent_cone_of_segment_subset /- _inst_6: normed_group ↝ semi_normed_group -/
#check @unique_diff_on.unique_diff_within_at /- _inst_3: normed_space ↝ module -/
#check @unique_diff_on_empty /- _inst_3: normed_space ↝ module -/

-- analysis/complex/basic.lean
#check @normed_space.complex_to_real /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/convex/basic.lean
#check @segment_eq_image /- _inst_4: module ↝ has_scalar -/
#check @open_segment_eq_image /- _inst_4: module ↝ has_scalar -/
#check @mem_segment_iff_div /- _inst_4: module ↝ has_scalar -/
#check @mem_open_segment_iff_div /- _inst_4: module ↝ has_scalar -/
#check @mem_open_segment_iff_div /- _inst_2: add_comm_monoid ↝ has_add -/
#check @monotone_on.convex_le /- _inst_3: ordered_add_comm_monoid ↝ preorder -/
#check @monotone_on.convex_lt /- _inst_3: ordered_add_comm_monoid ↝ preorder -/
#check @convex.neg /- _inst_1: ordered_ring ↝ ordered_semiring -/
#check @convex.neg_preimage /- _inst_1: ordered_ring ↝ ordered_semiring -/

-- analysis/convex/combination.lean
#check @finset.center_mass /- _inst_4: module ↝ has_scalar -/
#check @mem_Icc_of_mem_std_simplex /- _inst_1: linear_ordered_field ↝ ordered_semiring -/

-- analysis/convex/function.lean
#check @linear_order.strict_convex_on_of_lt /- _inst_5: module ↝ has_scalar -/
#check @linear_order.strict_convex_on_of_lt /- _inst_6: module ↝ has_scalar -/
#check @convex_on.comp_affine_map /- _inst_1: linear_ordered_field ↝ ordered_ring -/

-- analysis/convex/gauge.lean
#check @gauge /- _inst_1: add_comm_group ↝ add_comm_monoid -/
#check @absorbent.gauge_set_nonempty /- _inst_1: add_comm_group ↝ add_comm_monoid -/
#check @balanced.star_convex /- _inst_1: add_comm_group ↝ add_comm_monoid -/

-- analysis/convex/independent.lean
#check @convex_independent /- _inst_2: add_comm_group ↝ add_comm_monoid -/

-- analysis/convex/quasiconvex.lean
#check @quasiconvex_on /- _inst_4: ordered_add_comm_monoid ↝ has_le -/
#check @quasiconcave_on /- _inst_4: ordered_add_comm_monoid ↝ has_le -/

-- analysis/convex/specific_functions.lean
#check @convex_on_norm /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/convex/star.lean
#check @star_convex.neg /- _inst_1: ordered_ring ↝ ordered_semiring -/
#check @star_convex.neg_preimage /- _inst_1: ordered_ring ↝ ordered_semiring -/
#check @star_convex_iff_div /- _inst_3: module ↝ has_scalar -/

-- analysis/convex/strict.lean
#check @convex.strict_convex /- _inst_6: module ↝ has_scalar -/
#check @strict_convex_singleton /- _inst_6: module ↝ has_scalar -/
#check @set.subsingleton.strict_convex /- _inst_6: module ↝ has_scalar -/
#check @strict_convex.linear_image /- _inst_6: module ↝ has_scalar -/
#check @strict_convex.linear_image /- _inst_7: module ↝ has_scalar -/
#check @strict_convex.linear_image /- _inst_10: order_topology ↝ order_closed_topology -/
#check @strict_convex_Iio /- _inst_10: order_topology ↝ order_closed_topology -/
#check @strict_convex_Ioi /- _inst_10: order_topology ↝ order_closed_topology -/
#check @strict_convex.eq_of_open_segment_subset_frontier /- _inst_6: module ↝ has_scalar -/
#check @strict_convex.neg /- _inst_1: ordered_ring ↝ ordered_semiring -/
#check @strict_convex.neg_preimage /- _inst_1: ordered_ring ↝ ordered_semiring -/
#check @strict_convex.neg_preimage /- _inst_8: topological_add_group ↝ has_continuous_neg -/
#check @strict_convex_iff_div /- _inst_5: module ↝ has_scalar -/

-- analysis/convex/topology.lean
#check @convex.combo_interior_self_subset_interior /- _inst_4: topological_add_group ↝ has_continuous_add -/
#check @convex.closure /- _inst_4: topological_add_group ↝ has_continuous_add -/
#check @normed_space.path_connected /- _inst_1: normed_group ↝ semi_normed_group -/
#check @dist_add_dist_of_mem_segment /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/hofer.lean
#check @hofer /- _inst_1: metric_space ↝ pseudo_metric_space -/

-- analysis/inner_product_space/basic.lean
#check @has_inner.is_R_or_C_to_real /- _inst_2: inner_product_space ↝ has_inner -/

-- analysis/inner_product_space/pi_L2.lean
#check @euclidean_space /- _inst_6: is_R_or_C ↝ -/
#check @euclidean_space /- _inst_7: fintype ↝ -/

-- analysis/locally_convex/balanced_core_hull.lean
#check @balanced_core_aux /- _inst_1: semi_normed_ring ↝ has_norm -/
#check @balanced_hull /- _inst_1: semi_normed_ring ↝ has_norm -/
#check @balanced_core_aux_empty /- _inst_3: module ↝ has_scalar -/
#check @balanced_core_aux_maximal /- _inst_5: has_continuous_smul ↝ has_continuous_const_smul -/

-- analysis/locally_convex/basic.lean
#check @absorbs /- _inst_1: semi_normed_ring ↝ has_norm -/
#check @absorbent /- _inst_1: semi_normed_ring ↝ has_norm -/
#check @balanced /- _inst_1: semi_normed_ring ↝ has_norm -/
#check @absorbent_univ /- _inst_9: has_continuous_smul ↝ has_continuous_const_smul -/
#check @balanced.closure /- _inst_9: has_continuous_smul ↝ has_continuous_const_smul -/

-- analysis/locally_convex/bounded.lean
#check @bornology.is_vonN_bounded.of_topological_space_le /- _inst_3: module ↝ has_scalar -/

-- analysis/locally_convex/with_seminorms.lean
#check @seminorm_family /- _inst_1: normed_field ↝ semi_normed_ring -/
#check @seminorm_family /- _inst_3: module ↝ has_scalar -/

-- analysis/normed/group/basic.lean
#check @controlled_sum_of_mem_closure_range /- _inst_1: semi_normed_group ↝ add_group -/
#check @eventually_ne_of_tendsto_norm_at_top /- _inst_1: semi_normed_group ↝ has_norm -/

-- analysis/normed/group/hom.lean
#check @exists_pos_bound_of_bound /- _inst_2: semi_normed_group ↝ has_norm -/
#check @normed_group_hom.op_norm_zero_iff /- _inst_5: normed_group ↝ semi_normed_group -/
#check @normed_group_hom.coe_smul /- _inst_8: has_bounded_smul ↝ has_scalar -/
#check @normed_group_hom.smul_apply /- _inst_8: has_bounded_smul ↝ has_scalar -/
#check @normed_group_hom.smul_comm_class /- _inst_8: has_bounded_smul ↝ has_scalar -/
#check @normed_group_hom.smul_comm_class /- _inst_12: has_bounded_smul ↝ has_scalar -/
#check @normed_group_hom.is_scalar_tower /- _inst_8: has_bounded_smul ↝ has_scalar -/
#check @normed_group_hom.is_scalar_tower /- _inst_12: has_bounded_smul ↝ has_scalar -/
#check @controlled_closure_of_complete /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/normed/normed_field.lean
#check @finset.norm_prod_le' /- _inst_2: normed_comm_ring ↝ semi_normed_comm_ring -/
#check @finset.norm_prod_le /- _inst_2: normed_comm_ring ↝ semi_normed_comm_ring -/
#check @summable.mul_norm /- _inst_1: normed_ring ↝ non_unital_semi_normed_ring -/
#check @summable_norm_sum_mul_antidiagonal_of_summable_norm /- _inst_1: normed_ring ↝ non_unital_semi_normed_ring -/

-- analysis/normed_space/basic.lean
#check @normed_space.to_module' /- _inst_5: normed_space ↝ module -/

-- analysis/normed_space/bounded_linear_maps.lean
#check @is_bounded_linear_map.is_O_id /- _inst_1: nondiscrete_normed_field ↝ normed_field -/

-- analysis/normed_space/conformal_linear_map.lean
#check @is_conformal_map /- _inst_4: normed_space ↝ module

-- analysis/normed_space/dual.lean
#check @normed_space.dual /- _inst_3: normed_space ↝ module -/
#check @normed_space.dual.finite_dimensional /- _inst_6: finite_dimensional ↝ finite_dimensional -/

-- analysis/normed_space/finite_dimension.lean
#check @linear_map.continuous_on_pi /- _inst_6: topological_add_group ↝ has_continuous_add -/
#check @linear_map.continuous_on_pi /- _inst_6: finite_dimensional ↝ finite_dimensional -/
#check @linear_map.continuous_on_pi /- _inst_12: finite_dimensional ↝ finite_dimensional -/
#check @continuous_linear_map.topological_space.second_countable_topology /- _inst_14: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- analysis/normed_space/indicator_function.lean
#check @norm_indicator_eq_indicator_norm /- _inst_1: normed_group ↝ semi_normed_group -/
#check @nnnorm_indicator_eq_indicator_nnnorm /- _inst_1: normed_group ↝ semi_normed_group -/
#check @indicator_norm_le_norm_self /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/normed_space/is_R_or_C.lean
#check @is_R_or_C.norm_coe_norm /- _inst_2: normed_group ↝ semi_normed_group -/

-- analysis/normed_space/multilinear.lean
#check @multilinear_map.norm_image_sub_le_of_bound' /- _inst_15: normed_space ↝ module -/
#check @multilinear_map.restr_norm_le /- _inst_15: normed_space ↝ module -/
#check @multilinear_map.restr_norm_le /- _inst_17: normed_space ↝ module -/
#check @continuous_multilinear_map.op_norm /- _inst_15: normed_space ↝ module -/
#check @continuous_multilinear_map.bounds_bdd_below /- _inst_15: normed_space ↝ module -/
#check @continuous_multilinear_map.norm_restrict_scalars /- _inst_19: normed_algebra ↝ has_scalar -/
#check @continuous_multilinear_map.uncurry0 /- _inst_17: normed_space ↝ module -/
#check @continuous_multilinear_map.curry0 /- _inst_15: normed_space ↝ module -/

-- analysis/normed_space/operator_norm.lean
#check @linear_map.lipschitz_of_bound /- _inst_8: normed_space ↝ module -/
#check @linear_map.lipschitz_of_bound /- _inst_9: normed_space ↝ module -/
#check @linear_map.lipschitz_of_bound_nnnorm /- _inst_8: normed_space ↝ module -/
#check @linear_map.lipschitz_of_bound_nnnorm /- _inst_9: normed_space ↝ module -/
#check @linear_map.antilipschitz_of_bound /- _inst_8: normed_space ↝ module -/
#check @linear_map.antilipschitz_of_bound /- _inst_9: normed_space ↝ module -/
#check @linear_map.bound_of_antilipschitz /- _inst_8: normed_space ↝ module -/
#check @linear_map.bound_of_antilipschitz /- _inst_9: normed_space ↝ module -/
#check @norm_image_of_norm_zero /- _inst_9: normed_space ↝ module -/
#check @norm_image_of_norm_zero /- _inst_10: normed_space ↝ module -/
#check @continuous_linear_map.op_norm /- _inst_9: normed_space ↝ module -/
#check @continuous_linear_map.op_norm /- _inst_10: normed_space ↝ module -/
#check @continuous_linear_map.bounds_bdd_below /- _inst_9: normed_space ↝ module -/
#check @continuous_linear_map.bounds_bdd_below /- _inst_10: normed_space ↝ module -/
#check @continuous_linear_map.op_norm_smul_le /- _inst_19: smul_comm_class ↝ module -/
#check @continuous_linear_map.isometry_iff_norm /- _inst_9: normed_space ↝ module -/
#check @continuous_linear_map.isometry_iff_norm /- _inst_10: normed_space ↝ module -/
#check @continuous_linear_map.norm_restrict_scalars /- _inst_21: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @continuous_linear_map.norm_restrict_scalars /- _inst_23: is_scalar_tower ↝ linear_map.compatible_smul -/
#check @continuous_linear_equiv.homothety_inverse /- _inst_9: normed_space ↝ module -/
#check @continuous_linear_equiv.homothety_inverse /- _inst_10: normed_space ↝ module -/
#check @continuous_linear_map.bilinear_comp /- _inst_9: normed_space ↝ module -/
#check @is_coercive /- _inst_1: normed_group ↝ semi_normed_group -/

-- analysis/normed_space/pointwise.lean
#check @affinity_unit_ball /- _inst_2: normed_group ↝ semi_normed_group -/

-- analysis/normed_space/riesz_lemma.lean
#check @riesz_lemma /- _inst_3: normed_space ↝ module -/

-- analysis/normed_space/spectrum.lean
#check @spectrum.mem_resolvent_set_of_spectral_radius_lt /- _inst_3: normed_algebra ↝ algebra -/

-- analysis/normed_space/star/exponential.lean
#check @self_adjoint.exp_i_smul_unitary /- _inst_4: cstar_ring ↝ normed_star_group -/

-- analysis/seminorm.lean
#check @seminorm.is_scalar_tower /- _inst_6: is_scalar_tower ↝ has_scalar -/
#check @seminorm.is_scalar_tower /- _inst_9: is_scalar_tower ↝ has_scalar -/
#check @seminorm.coe_smul /- _inst_6: is_scalar_tower ↝ has_scalar -/
#check @seminorm.smul_apply /- _inst_6: is_scalar_tower ↝ has_scalar -/
#check @seminorm.smul_comp /- _inst_10: is_scalar_tower ↝ has_scalar -/

-- analysis/specific_limits/basic.lean
#check @tendsto_nat_floor_mul_div_at_top /- _inst_4: floor_ring ↝ floor_semiring -/
#check @tendsto_nat_ceil_mul_div_at_top /- _inst_4: floor_ring ↝ floor_semiring -/

-- analysis/specific_limits/normed.lean
#check @normed_field.tendsto_norm_inverse_nhds_within_0_at_top /- _inst_1: normed_field ↝ normed_division_ring -/
#check @tendsto_pow_at_top_nhds_0_of_norm_lt_1 /- _inst_1: normed_ring ↝ semi_normed_ring -/
#check @normed_ring.summable_geometric_of_norm_lt_1 /- _inst_1: normed_ring ↝ semi_normed_ring -/

-- category_theory/abelian/basic.lean
#check @category_theory.abelian.epi_pullback_of_epi_g /- _inst_4: category_theory.epi ↝ category_theory.epi -/
#check @category_theory.abelian.mono_pushout_of_mono_g /- _inst_4: category_theory.mono ↝ category_theory.mono -/

-- category_theory/abelian/diagram_lemmas/four.lean
#check @category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso /- _inst_9: category_theory.is_iso ↝ category_theory.epi -/
#check @category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso /- _inst_12: category_theory.is_iso ↝ category_theory.mono -/

-- category_theory/abelian/left_derived.lean
#check @category_theory.abelian.functor.left_derived_zero_to_self_app /- _inst_6: category_theory.enough_projectives ↝ category_theory.has_projective_resolutions -/
#check @category_theory.abelian.functor.left_derived_zero_to_self_app_inv /- _inst_6: category_theory.enough_projectives ↝ category_theory.has_projective_resolutions -/

-- category_theory/abelian/non_preadditive.lean
#check @category_theory.non_preadditive_abelian.mono_Δ /- _inst_2: category_theory.non_preadditive_abelian ↝ category_theory.limits.has_finite_products -/

-- category_theory/abelian/right_derived.lean
#check @category_theory.abelian.functor.right_derived_zero_to_self_app /- _inst_6: category_theory.enough_injectives ↝ category_theory.has_injective_resolutions -/
#check @category_theory.abelian.functor.right_derived_zero_to_self_app_inv /- _inst_6: category_theory.enough_injectives ↝ category_theory.has_injective_resolutions -/

-- category_theory/adjunction/lifting.lean
#check @category_theory.adjoint_square_lift /- _inst_5: category_theory.is_right_adjoint ↝ category_theory.is_right_adjoint -/
#check @category_theory.adjoint_square_lift /- _inst_7: category_theory.is_right_adjoint ↝ category_theory.is_right_adjoint -/
#check @category_theory.monadic_adjoint_square_lift /- _inst_5: category_theory.is_right_adjoint ↝ category_theory.is_right_adjoint -/
#check @category_theory.monadic_adjoint_square_lift /- _inst_7: category_theory.is_right_adjoint ↝ category_theory.is_right_adjoint -/

-- category_theory/adjunction/limits.lean
#check @category_theory.adjunction.has_colimits_of_equivalence /- _inst_5: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.adjunction.has_limits_of_equivalence /- _inst_5: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/category/basic.lean
#check @category_theory.eq_whisker /- _inst_1: category_theory.category ↝ category_theory.category_struct -/
#check @category_theory.whisker_eq /- _inst_1: category_theory.category ↝ category_theory.category_struct -/
#check @category_theory.comp_dite /- _inst_1: category_theory.category ↝ category_theory.category_struct -/
#check @category_theory.dite_comp /- _inst_1: category_theory.category ↝ category_theory.category_struct -/

-- category_theory/category/ulift.lean
#check @category_theory.as_small /- _inst_2: category_theory.category ↝ -/

-- category_theory/closed/ideal.lean
#check @category_theory.exponential_ideal.mk_of_iso /- _inst_5: category_theory.reflective ↝ category_theory.is_right_adjoint -/

-- category_theory/concrete_category/bundled_hom.lean
#check @category_theory.bundled_hom.bundled_hom_of_parent_projection /- _inst_1: category_theory.bundled_hom.parent_projection ↝ -/

-- category_theory/core.lean
#check @category_theory.core.forget_functor_to_core /- _inst_2: category_theory.groupoid ↝ category_theory.category -/

-- category_theory/endomorphism.lean
#check @category_theory.End /- _inst_1: category_theory.category_struct ↝ quiver -/

-- category_theory/enriched/basic.lean
#check @category_theory.forget_enrichment /- _inst_9: category_theory.enriched_category ↝ -/

-- category_theory/fin_category.lean
#check @category_theory.fin_category.obj_as_type /- _inst_3: category_theory.fin_category ↝ -/
#check @category_theory.fin_category.as_type /- _inst_3: category_theory.fin_category ↝ -/

-- category_theory/full_subcategory.lean
#check @category_theory.induced_category /- _inst_1: category_theory.category ↝ -/

-- category_theory/functor/flat.lean
#check @category_theory.flat_of_preserves_finite_limits /- _inst_3: category_theory.limits.has_finite_limits ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/generator.lean
#check @category_theory.is_separating /- _inst_1: category_theory.category ↝ category_theory.category_struct -/
#check @category_theory.is_coseparating /- _inst_1: category_theory.category ↝ category_theory.category_struct -/

-- category_theory/graded_object.lean
#check @category_theory.graded_object_with_shift /- _inst_1: add_comm_group ↝ -/

-- category_theory/idempotents/karoubi.lean
#check @category_theory.idempotents.to_karoubi_is_equivalence /- _inst_2: category_theory.is_idempotent_complete ↝ category_theory.ess_surj -/

-- category_theory/is_connected.lean
#check @category_theory.zag /- _inst_1: category_theory.category ↝ quiver -/

-- category_theory/limits/comma.lean
#check @category_theory.comma.has_limits /- _inst_5: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.comma.has_limits /- _inst_6: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.comma.has_colimits /- _inst_5: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.comma.has_colimits /- _inst_6: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.arrow.has_limits /- _inst_5: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.arrow.has_colimits /- _inst_5: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.structured_arrow.has_limits /- _inst_5: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.costructured_arrow.has_colimits /- _inst_5: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/limits/creates.lean
#check @category_theory.has_limits_of_has_limits_creates_limits /- _inst_4: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.has_colimits_of_has_colimits_creates_colimits /- _inst_4: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.preserves_limits_of_creates_limits_and_has_limits /- _inst_5: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.preserves_colimits_of_creates_colimits_and_has_colimits /- _inst_5: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/limits/filtered_colimit_commutes_finite_limit.lean
#check @category_theory.limits.colim.preserves_finite_limits /- _inst_9: category_theory.limits.has_finite_limits ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/limits/functor_category.lean
#check @category_theory.limits.functor_category_has_limits_of_size /- _inst_5: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.limits.functor_category_has_colimits_of_size /- _inst_5: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.limits.evaluation_preserves_limits /- _inst_5: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.limits.evaluation_preserves_colimits /- _inst_5: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/limits/over.lean
#check @category_theory.over.category_theory.limits.has_colimits /- _inst_3: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.under.category_theory.limits.has_limits /- _inst_3: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/limits/preserves/basic.lean
#check @category_theory.limits.reflects_limits_of_shape_of_nat_iso /- _inst_4: category_theory.limits.reflects_limits_of_shape ↝ category_theory.limits.reflects_limit -/
#check @category_theory.limits.reflects_limits_of_reflects_isomorphisms /- _inst_5: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.limits.reflects_colimits_of_shape_of_nat_iso /- _inst_4: category_theory.limits.reflects_colimits_of_shape ↝ category_theory.limits.reflects_colimit -/
#check @category_theory.limits.reflects_colimits_of_reflects_isomorphisms /- _inst_5: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/limits/preserves/functor_category.lean
#check @category_theory.functor_category.prod_preserves_colimits /- _inst_5: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.whiskering_left_preserves_limits /- _inst_4: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.whiskering_right_preserves_limits /- _inst_7: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/limits/preserves/shapes/biproducts.lean
#check @category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts /- _inst_6: category_theory.limits.preserves_biproducts ↝ category_theory.limits.preserves_biproducts_of_shape -/

-- category_theory/limits/shapes/biproducts.lean
#check @category_theory.limits.has_binary_products_of_has_binary_biproducts /- _inst_4: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/
#check @category_theory.limits.has_binary_coproducts_of_has_binary_biproducts /- _inst_4: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/
#check @category_theory.limits.biprod.symmetry' /- _inst_4: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/
#check @category_theory.limits.biproduct.matrix_map /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.biproduct.map_matrix /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.inl_of_is_limit /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.inr_of_is_limit /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.fst_of_is_colimit /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.snd_of_is_colimit /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.limits.biprod.map_eq /- _inst_6: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/
#check @category_theory.subsingleton_preadditive_of_has_binary_biproducts /- _inst_3: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/

-- category_theory/limits/shapes/disjoint_coproduct.lean
#check @category_theory.limits.initial_mono_class_of_disjoint_coproducts /- _inst_2: category_theory.limits.coproducts_disjoint ↝ category_theory.limits.coproduct_disjoint -/

-- category_theory/limits/shapes/finite_limits.lean
#check @category_theory.limits.has_finite_limits_of_has_limits /- _inst_2: category_theory.limits.has_limits ↝ category_theory.limits.has_finite_limits -/
#check @category_theory.limits.has_finite_colimits_of_has_colimits /- _inst_2: category_theory.limits.has_colimits ↝ category_theory.limits.has_finite_colimits -/

-- category_theory/limits/shapes/normal_mono/equalizers.lean
#check @category_theory.normal_mono_category.epi_of_zero_cokernel /- _inst_3: category_theory.limits.has_finite_products ↝ category_theory.limits.has_equalizers -/
#check @category_theory.normal_mono_category.epi_of_zero_cokernel /- _inst_4: category_theory.limits.has_kernels ↝ category_theory.limits.has_equalizers -/
#check @category_theory.normal_epi_category.mono_of_zero_kernel /- _inst_3: category_theory.limits.has_finite_coproducts ↝ category_theory.limits.has_coequalizers -/
#check @category_theory.normal_epi_category.mono_of_zero_kernel /- _inst_4: category_theory.limits.has_cokernels ↝ category_theory.limits.has_coequalizers -/

-- category_theory/limits/shapes/reflexive.lean
#check @category_theory.limits.has_coequalizer_of_common_section /- _inst_3: category_theory.limits.has_reflexive_coequalizers ↝ category_theory.limits.has_coequalizer -/
#check @category_theory.limits.has_equalizer_of_common_retraction /- _inst_3: category_theory.limits.has_coreflexive_equalizers ↝ category_theory.limits.has_equalizer -/

-- category_theory/linear/default.lean
#check @category_theory.linear.category_theory.End.module /- _inst_3: comm_ring ↝ semiring -/

-- category_theory/monad/limits.lean
#check @category_theory.comp_comparison_forget_has_limit /- _inst_4: category_theory.monadic_right_adjoint ↝ category_theory.is_right_adjoint -/
#check @category_theory.has_limit_of_reflective /- _inst_5: category_theory.reflective ↝ category_theory.monadic_right_adjoint -/
#check @category_theory.has_limits_of_reflective /- _inst_4: category_theory.limits.has_limits_of_size ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.has_colimits_of_reflective /- _inst_5: category_theory.limits.has_colimits_of_size ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/monoidal/transport.lean
#check @category_theory.monoidal.transported /- _inst_2: category_theory.monoidal_category ↝ -/

-- category_theory/preadditive/biproducts.lean
#check @category_theory.is_iso_left_of_is_iso_biprod_map /- _inst_3: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/
#check @category_theory.biprod.column_nonzero_of_iso /- _inst_3: category_theory.limits.has_binary_biproducts ↝ category_theory.limits.has_binary_biproduct -/

-- category_theory/preadditive/default.lean
#check @category_theory.preadditive.is_iso.comp_left_eq_zero /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.preadditive.is_iso.comp_right_eq_zero /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/

-- category_theory/preadditive/functor_category.lean
#check @category_theory.nat_trans.app_zero /- _inst_3: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/

-- category_theory/preadditive/opposite.lean
#check @category_theory.unop_zero /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/
#check @category_theory.op_zero /- _inst_2: category_theory.preadditive ↝ category_theory.limits.has_zero_morphisms -/

-- category_theory/preadditive/schur.lean
#check @category_theory.finrank_hom_simple_simple_eq_zero_of_not_iso /- _inst_3: field ↝ division_ring -/

-- category_theory/sites/dense_subsite.lean
#check @category_theory.cover_dense.types.pushforward_family /- _inst_5: category_theory.full ↝ -/

-- category_theory/sites/grothendieck.lean
#check @category_theory.grothendieck_topology.right_ore_condition /- _inst_2: category_theory.category ↝ category_theory.category_struct -/

-- category_theory/sites/left_exact.lean
#check @category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits /- _inst_4: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_finite_limits /- _inst_7: category_theory.limits.has_finite_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits /- _inst_12: category_theory.limits.has_finite_limits ↝ category_theory.limits.has_limits_of_shape -/

-- category_theory/sites/limits.lean
#check @category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits /- _inst_4: category_theory.limits.has_limits ↝ category_theory.limits.has_limits_of_shape -/
#check @category_theory.Sheaf.category_theory.limits.has_colimits /- _inst_6: category_theory.limits.preserves_limits ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.Sheaf.category_theory.limits.has_colimits /- _inst_9: category_theory.reflects_isomorphisms ↝ category_theory.limits.has_colimits_of_shape -/
#check @category_theory.Sheaf.category_theory.limits.has_colimits /- _inst_10: category_theory.limits.has_colimits ↝ category_theory.limits.has_colimits_of_shape -/

-- category_theory/sites/sieves.lean
#check @category_theory.presieve /- _inst_1: category_theory.category ↝ quiver -/

-- category_theory/subterminal.lean
#check @category_theory.is_subterminal /- _inst_1: category_theory.category ↝ quiver -/

-- combinatorics/additive/salem_spencer.lean
#check @mul_salem_spencer /- _inst_1: monoid ↝ has_mul -/
#check @add_salem_spencer /- _inst_1: add_monoid ↝ has_add -/

-- combinatorics/hindman.lean
#check @ultrafilter.continuous_mul_left /- _inst_1: semigroup ↝ has_mul -/
#check @ultrafilter.continuous_add_left /- _inst_1: add_semigroup ↝ has_add -/

-- combinatorics/simple_graph/inc_matrix.lean
#check @simple_graph.inc_matrix_mul_transpose_apply_of_adj /- _inst_2: semiring ↝ non_assoc_semiring -/

-- computability/partrec.lean
#check @partrec /- _inst_1: primcodable ↝ encodable -/
#check @partrec /- _inst_2: primcodable ↝ encodable -/

-- computability/primrec.lean
#check @primrec /- _inst_1: primcodable ↝ encodable -/
#check @primrec /- _inst_2: primcodable ↝ encodable -/

-- computability/reduce.lean
#check @to_nat /- _inst_1: primcodable ↝ encodable -/

-- computability/turing_machine.lean
#check @turing.TM0.machine /- _inst_2: inhabited ↝ -/
#check @turing.TM1to0.Λ' /- _inst_2: inhabited ↝ -/
#check @turing.TM1to0.Λ' /- _inst_3: inhabited ↝ -/
#check @turing.TM2to1.Γ' /- _inst_1: decidable_eq ↝ -/
#check @turing.TM2to1.st_run /- _inst_2: inhabited ↝ -/

-- control/bitraversable/instances.lean
#check @const.bitraverse /- _inst_2: applicative ↝ -/

-- control/fold.lean
#check @traversable.mfoldl.unop_of_free_monoid /- _inst_2: is_lawful_monad ↝ -/

-- control/monad/cont.lean
#check @writer_t.monad_cont /- _inst_1: monad ↝ -/
#check @state_t.mk_label /- _inst_1: monad ↝ -/

-- control/monad/writer.lean
#check @writer_t.ext /- _inst_1: monad ↝ -/
#check @writer_t.monad_map /- _inst_2: monad ↝ -/
#check @writer_t.monad_map /- _inst_3: monad ↝ -/
#check @writer_t.monad_except /- _inst_1: monad ↝ -/

-- control/traversable/instances.lean
#check @option.comp_traverse /- _inst_3: is_lawful_applicative ↝ -/
#check @list.comp_traverse /- _inst_3: is_lawful_applicative ↝ -/
#check @sum.comp_traverse /- _inst_3: is_lawful_applicative ↝ -/

-- data/complex/exponential.lean
#check @is_cau_geo_series /- _inst_5: field ↝ euclidean_domain -/
#check @abv_sum_le_sum_abv /- _inst_1: ring ↝ semiring

-- data/complex/module.lean
#check @module.complex_to_real /- _inst_1: add_comm_group ↝ add_comm_monoid -/

-- data/dfinsupp/basic.lean
#check @monoid_hom.coe_dfinsupp_prod /- _inst_4: monoid ↝ mul_one_class -/
#check @add_monoid_hom.coe_dfinsupp_sum /- _inst_4: add_monoid ↝ add_zero_class -/
#check @add_monoid_hom.dfinsupp_sum_apply /- _inst_4: add_monoid ↝ add_zero_class -/
#check @monoid_hom.dfinsupp_prod_apply /- _inst_4: monoid ↝ mul_one_class -/

-- data/fin/basic.lean
#check @fin.order_iso_subsingleton /- _inst_1: preorder ↝ has_le -/

-- data/fin_enum.lean
#check @fin_enum.mem_pi /- _inst_1: fin_enum ↝ decidable_eq -/

-- data/finset/lattice.lean
#check @finset.supr_option_to_finset /- _inst_1: complete_lattice ↝ has_Sup -/

-- data/finset/locally_finite.lean
#check @finset.Ico_inter_Ico_consecutive /- _inst_1: partial_order ↝ preorder -/

-- data/finset/noncomm_prod.lean
#check @finset.noncomm_sum_add_distrib_aux /- _inst_1: add_monoid ↝ add_semigroup -/
#check @finset.noncomm_prod_mul_distrib_aux /- _inst_1: monoid ↝ semigroup -/

-- data/finset/pointwise.lean
#check @finset.smul_comm_class_set /- _inst_4: smul_comm_class ↝ smul_comm_class -/
#check @finset.vadd_comm_class_set /- _inst_4: vadd_comm_class ↝ vadd_comm_class -/
#check @finset.is_scalar_tower' /- _inst_6: is_scalar_tower ↝ is_scalar_tower -/
#check @finset.is_central_scalar /- _inst_5: is_central_scalar ↝ is_central_scalar -/

-- data/finsupp/basic.lean
#check @ring_hom.map_finsupp_sum /- _inst_2: semiring ↝ non_assoc_semiring -/
#check @ring_hom.map_finsupp_sum /- _inst_3: semiring ↝ non_assoc_semiring -/
#check @monoid_hom.coe_finsupp_prod /- _inst_2: monoid ↝ mul_one_class -/
#check @add_monoid_hom.coe_finsupp_sum /- _inst_2: add_monoid ↝ add_zero_class -/
#check @add_monoid_hom.finsupp_sum_apply /- _inst_2: add_monoid ↝ add_zero_class -/
#check @monoid_hom.finsupp_prod_apply /- _inst_2: monoid ↝ mul_one_class -/
#check @finsupp.lift_add_hom_apply /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.lift_add_hom_symm_apply /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.lift_add_hom_symm_apply_apply /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.lift_add_hom_apply_single /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.sum_sub_index /- _inst_1: add_comm_group ↝ add_group -/
#check @finsupp.prod_sum_index /- _inst_1: add_comm_monoid ↝ has_zero -/
#check @finsupp.sum_sum_index /- _inst_1: add_comm_monoid ↝ has_zero -/
#check @finsupp.sum_update_add /- _inst_2: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.eq_zero_of_comap_domain_eq_zero /- _inst_1: add_comm_monoid ↝ has_zero -/
#check @finsupp.some_add /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @finsupp.comap_has_scalar /- _inst_2: mul_action ↝ has_scalar -/
#check @finsupp.smul_comm_class /- _inst_3: add_comm_monoid ↝ add_monoid
#check @nat.cast_finsupp_sum /- _inst_2: comm_semiring ↝ non_assoc_semiring -/
#check @int.cast_finsupp_sum /- _inst_2: comm_ring ↝ non_assoc_ring -/

-- data/fintype/basic.lean
#check @fintype.univ_of_is_empty /- _inst_1: is_empty ↝ fintype -/
#check @fintype.card_of_is_empty /- _inst_1: is_empty ↝ fintype -/
#check @infinite.nonempty /- _inst_1: infinite ↝ nonempty -/

-- data/fp/basic.lean
#check @fp.div_nat_lt_two_pow /- C: fp.float_cfg ↝ -/

-- data/fun_like/basic.lean
#check @fun_like.congr_fun /- i: fun_like ↝ has_coe_to_fun -/

-- data/fun_like/equiv.lean
#check @equiv_like.injective /- iE: equiv_like ↝ embedding_like -/
#check @equiv_like.apply_eq_iff_eq /- iE: equiv_like ↝ embedding_like -/
#check @equiv_like.comp_injective /- iF: equiv_like ↝ embedding_like -/

-- data/holor.lean
#check @holor.zero_mul /- _inst_1: ring ↝ mul_zero_class -/
#check @holor.mul_zero /- _inst_1: ring ↝ mul_zero_class -/
#check @holor.mul_scalar_mul /- _inst_1: monoid ↝ has_mul -/
#check @holor.unit_vec /- _inst_1: monoid ↝ has_one -/
#check @holor.unit_vec /- _inst_2: add_monoid ↝ has_zero -/
#check @holor.slice_unit_vec_mul /- _inst_1: ring ↝ semiring -/
#check @holor.cprank_max_nil /- _inst_1: monoid ↝ has_mul -/
#check @holor.cprank_max_1 /- _inst_1: monoid ↝ has_mul -/
#check @holor.cprank_max_sum /- _inst_1: ring ↝ semiring -/

-- data/int/cast.lean
#check @int.cast_one /- _inst_1: add_monoid ↝ add_zero_class -/
#check @int.cast_bit0 /- _inst_1: ring ↝ non_assoc_ring -/
#check @int.coe_int_dvd /- _inst_1: comm_ring ↝ ring -/
#check @monoid_hom.ext_int /- _inst_1: monoid ↝ mul_one_class -/
#check @ring_hom.eq_int_cast /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_hom.ext_int /- _inst_3: semiring ↝ non_assoc_semiring -/

-- data/list/big_operators.lean
#check @list.prod_singleton /- _inst_1: monoid ↝ mul_one_class -/
#check @list.sum_singleton /- _inst_1: add_monoid ↝ add_zero_class -/
#check @list.sum_le_foldr_max /- _inst_2: add_monoid ↝ has_zero -/
#check @list.dvd_sum /- _inst_1: semiring ↝ non_unital_semiring -/
#check @list.alternating_sum_cons_cons /- _inst_2: add_comm_group ↝ sub_neg_monoid -/

-- data/list/func.lean
#check @list.func.get_add /- _inst_1: add_monoid ↝ add_zero_class -/
#check @list.func.nil_add /- _inst_1: add_monoid ↝ add_zero_class -/
#check @list.func.add_nil /- _inst_1: add_monoid ↝ add_zero_class -/
#check @list.func.nil_sub /- _inst_1: add_group ↝ sub_neg_monoid -/

-- data/list/infix.lean
#check @list.insert_nil /- _inst_1: decidable_eq ↝ has_insert -/

-- data/list/zip.lean
#check @list.sum_zip_with_distrib_left /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/

-- data/matrix/basic.lean
#check @matrix.bit1_apply /- _inst_2: add_monoid ↝ add_zero_class -/
#check @matrix.smul_eq_diagonal_mul /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.transpose_smul /- _inst_1: has_scalar ↝ has_scalar -/
#check @matrix.minor_smul /- _inst_3: module ↝ has_scalar -/
#check @matrix.row_vec_mul /- _inst_2: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.col_vec_mul /- _inst_2: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.col_mul_vec /- _inst_2: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.row_mul_vec /- _inst_2: semiring ↝ non_unital_non_assoc_semiring -/
#check @ring_hom.map_matrix_mul /- _inst_2: semiring ↝ non_assoc_semiring -/
#check @ring_hom.map_matrix_mul /- _inst_3: semiring ↝ non_assoc_semiring -/
#check @ring_hom.map_dot_product /- _inst_4: semiring ↝ non_assoc_semiring -/
#check @ring_hom.map_dot_product /- _inst_5: semiring ↝ non_assoc_semiring -/

-- data/matrix/basis.lean
#check @matrix.std_basis_matrix /- _inst_4: semiring ↝ has_zero -/

-- data/matrix/block.lean
#check @matrix.from_blocks_smul /- _inst_1: semiring ↝ has_mul -/
#check @matrix.from_blocks_add /- _inst_1: semiring ↝ has_add -/
#check @matrix.from_blocks_diagonal /- _inst_1: semiring ↝ has_zero -/
#check @matrix.from_blocks_one /- _inst_1: semiring ↝ mul_zero_one_class -/
#check @matrix.block_diagonal_add /- _inst_2: add_monoid ↝ add_zero_class -/
#check @matrix.block_diagonal_mul /- _inst_4: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.block_diagonal'_add /- _inst_2: add_monoid ↝ add_zero_class -/
#check @matrix.block_diagonal'_mul /- _inst_2: semiring ↝ non_unital_non_assoc_semiring -/

-- data/matrix/dmatrix.lean
#check @dmatrix /- _inst_1: fintype ↝ -/
#check @dmatrix /- _inst_2: fintype ↝ -/

-- data/matrix/kronecker.lean
#check @matrix.smul_kronecker /- _inst_2: monoid ↝ has_mul -/
#check @matrix.smul_kronecker /- _inst_3: mul_action ↝ has_scalar -/
#check @matrix.kronecker_smul /- _inst_2: monoid ↝ has_mul -/
#check @matrix.kronecker_smul /- _inst_3: mul_action ↝ has_scalar -/

-- data/matrix/notation.lean
#check @matrix.empty_vec_mul /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.vec_mul_empty /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.cons_vec_mul /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.vec_mul_cons /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.empty_mul_vec /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.mul_vec_empty /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.cons_mul_vec /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/
#check @matrix.empty_vec_mul_vec /- _inst_1: semiring ↝ has_mul -/
#check @matrix.vec_mul_vec_empty /- _inst_1: semiring ↝ has_mul -/
#check @matrix.cons_vec_mul_vec /- _inst_1: semiring ↝ has_mul -/
#check @matrix.vec_mul_vec_cons /- _inst_1: semiring ↝ has_mul -/
#check @matrix.smul_mat_empty /- _inst_1: semiring ↝ has_scalar -/
#check @matrix.smul_mat_cons /- _inst_1: semiring ↝ has_mul -/

-- data/matrix/pequiv.lean
#check @pequiv.mul_matrix_apply /- _inst_3: semiring ↝ non_assoc_semiring -/
#check @pequiv.matrix_mul_apply /- _inst_2: semiring ↝ non_assoc_semiring -/
#check @pequiv.to_matrix_injective /- _inst_2: monoid_with_zero ↝ mul_zero_one_class -/
#check @pequiv.to_matrix_swap /- _inst_2: ring ↝ non_assoc_ring -/

-- data/multiset/locally_finite.lean
#check @multiset.Ico_disjoint_Ico /- _inst_1: partial_order ↝ preorder -/

-- data/mv_polynomial/basic.lean
#check @mv_polynomial /- _inst_1: comm_semiring ↝ semiring -/
#check @mv_polynomial.alg_hom_ext' /- _inst_4: comm_semiring ↝ semiring -/

-- data/mv_polynomial/comm_ring.lean
#check @mv_polynomial.hom_C /- _inst_2: comm_ring ↝ ring -/

-- data/mv_polynomial/variables.lean
#check @mv_polynomial.vars_C_mul /- _inst_3: is_domain ↝ no_zero_divisors -/

-- data/nat/cast.lean
#check @ext_nat' /- _inst_1: add_monoid ↝ add_zero_class -/
#check @ext_nat'' /- _inst_1: monoid_with_zero ↝ mul_zero_one_class -/

-- data/nat/prime.lean
#check @nat.monoid.prime_pow /- _inst_1: monoid ↝ has_pow -/

-- data/num/lemmas.lean
#check @pos_num.cast_mul /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @num.cast_add /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @num.cast_of_znum /- _inst_1: add_group ↝ add_monoid -/

-- data/ordmap/ordnode.lean
#check @ordnode.of_list /- _inst_2: decidable_rel ↝ has_insert -/

-- data/polynomial/algebra_map.lean
#check @polynomial.alg_hom_ext' /- _inst_2: comm_semiring ↝ semiring -/
#check @polynomial.alg_hom_eval₂_algebra_map /- _inst_6: comm_ring ↝ comm_semiring -/
#check @polynomial.alg_hom_eval₂_algebra_map /- _inst_7: ring ↝ semiring -/
#check @polynomial.alg_hom_eval₂_algebra_map /- _inst_8: ring ↝ semiring -/
#check @polynomial.eval₂_algebra_map_X /- _inst_7: ring ↝ semiring -/
#check @polynomial.aeval_sum /- _inst_8: comm_semiring ↝ semiring -/

-- data/polynomial/basic.lean
#check @polynomial.add_hom_ext /- _inst_2: add_monoid ↝ add_zero_class -/

-- data/polynomial/cancel_leads.lean
#check @polynomial.cancel_leads /- _inst_1: comm_ring ↝ ring -/

-- data/polynomial/denoms_clearable.lean
#check @denoms_clearable /- _inst_2: comm_semiring ↝ semiring -/

-- data/polynomial/derivative.lean
#check @polynomial.mem_support_derivative /- _inst_2: is_domain ↝ no_zero_divisors -/

-- data/polynomial/div.lean
#check @polynomial.sum_fin /- _inst_1: comm_ring ↝ semiring -/

-- data/polynomial/eval.lean
#check @polynomial.eval₂_eq_sum_range /- _inst_2: comm_semiring ↝ semiring -/
#check @polynomial.eval₂_eq_sum_range' /- _inst_2: comm_semiring ↝ semiring -/
#check @polynomial.eval₂_comp /- _inst_1: comm_semiring ↝ semiring -/
#check @polynomial.eval₂_hom /- _inst_1: comm_semiring ↝ semiring -/
#check @polynomial.eval₂_hom /- _inst_2: comm_semiring ↝ semiring -/
#check @polynomial.support_map_subset /- _inst_1: comm_semiring ↝ semiring -/
#check @polynomial.support_map_subset /- _inst_2: comm_semiring ↝ semiring -/

-- data/polynomial/field_division.lean
#check @polynomial.degree_map /- _inst_1: field ↝ division_ring -/
#check @polynomial.degree_map /- _inst_2: field ↝ euclidean_domain -/
#check @polynomial.map_eq_zero /- _inst_1: field ↝ division_ring -/

-- data/polynomial/integral_normalization.lean
#check @polynomial.integral_normalization_eval₂_eq_zero /- _inst_3: comm_ring ↝ comm_semiring -/

-- data/polynomial/lifts.lean
#check @polynomial.map_alg /- _inst_6: algebra ↝ algebra -/

-- data/polynomial/monic.lean
#check @polynomial.monic.nat_degree_map /- _inst_1: ring ↝ semiring -/
#check @polynomial.monic.degree_map /- _inst_1: ring ↝ semiring -/
#check @polynomial.degree_map_eq_of_injective /- _inst_1: ring ↝ semiring -/

-- data/polynomial/reverse.lean
#check @polynomial.reverse_mul_of_domain /- _inst_3: is_domain ↝ no_zero_divisors -/

-- data/polynomial/ring_division.lean
#check @polynomial.nat_degree_pos_of_aeval_root /- _inst_2: ring ↝ semiring -/
#check @polynomial.no_zero_divisors /- _inst_1: ring ↝ semiring -/
#check @polynomial.root_mul /- _inst_1: comm_ring ↝ comm_semiring -/
#check @polynomial.monic.comp /- _inst_2: is_domain ↝ no_zero_divisors -/
#check @polynomial.comp_eq_zero_iff /- _inst_2: is_domain ↝ no_zero_divisors -/
#check @polynomial.root_set /- _inst_3: comm_ring ↝ comm_semiring -/
#check @polynomial.leading_coeff_div_by_monic_X_sub_C /- _inst_2: is_domain ↝ nontrivial -/
#check @polynomial.monic.irreducible_of_irreducible_map /- _inst_2: is_domain ↝ no_zero_divisors -/

-- data/rbmap/default.lean
#check @rbmap.mem_of_min_eq /- _inst_1: is_strict_total_order ↝ is_strict_weak_order -/
#check @rbmap.mem_of_max_eq /- _inst_1: is_strict_total_order ↝ is_strict_weak_order -/

-- data/rbtree/insert.lean
#check @rbnode.equiv_or_mem_of_mem_ins /- _inst_2: is_strict_weak_order ↝ is_strict_order -/
#check @rbnode.find_balance1_gt /- _inst_1: is_strict_weak_order ↝ is_strict_order -/
#check @rbnode.find_balance2_lt /- _inst_1: is_strict_weak_order ↝ is_trans -/

-- data/rbtree/main.lean
#check @rbtree.mem_of_mem_of_eqv /- _inst_1: is_strict_weak_order ↝ is_incomp_trans -/
#check @rbtree.find_correct_exact /- _inst_2: is_strict_total_order ↝ is_strict_weak_order -/

-- data/real/cau_seq.lean
#check @is_cau_seq /- _inst_2: ring ↝ has_sub -/
#check @cau_seq.one_not_equiv_zero /- _inst_2: ring ↝ euclidean_domain -/
#check @cau_seq.one_not_equiv_zero /- _inst_3: is_domain ↝ nontrivial -/

-- data/real/cau_seq_completion.lean
#check @cau_seq.completion.Cauchy /- _inst_2: comm_ring ↝ ring -/
#check @cau_seq.completion.cau_seq_zero_ne_one /- _inst_2: field ↝ euclidean_domain -/

-- data/set/intervals/basic.lean
#check @set.Ioo /- _inst_1: preorder ↝ has_lt -/
#check @set.Iio /- _inst_1: preorder ↝ has_lt -/
#check @set.Icc /- _inst_1: preorder ↝ has_le -/
#check @set.Iic /- _inst_1: preorder ↝ has_le -/
#check @set.Ici /- _inst_1: preorder ↝ has_le -/
#check @set.Ioi /- _inst_1: preorder ↝ has_lt -/
#check @set.Icc_bot_top /- _inst_2: bounded_order ↝ bounded_order -/

-- data/set/intervals/disjoint.lean
#check @set.Union_Ico_eq_Iio_self_iff /- _inst_1: linear_order ↝ preorder -/
#check @set.Union_Ioc_eq_Ioi_self_iff /- _inst_1: linear_order ↝ preorder -/
#check @set.bUnion_Ico_eq_Iio_self_iff /- _inst_1: linear_order ↝ preorder -/
#check @set.bUnion_Ioc_eq_Ioi_self_iff /- _inst_1: linear_order ↝ preorder -/

-- data/set/intervals/surj_on.lean
#check @surj_on_Ioo_of_monotone_surjective /- _inst_2: partial_order ↝ preorder -/
#check @surj_on_Ioi_of_monotone_surjective /- _inst_2: partial_order ↝ preorder -/

-- data/set/pointwise.lean
#check @set.univ_mul_univ /- _inst_1: monoid ↝ mul_one_class -/
#check @set.univ_add_univ /- _inst_1: add_monoid ↝ add_zero_class -/
#check @add_submonoid.add_subset /- _inst_1: add_monoid ↝ add_zero_class -/
#check @submonoid.mul_subset /- _inst_1: monoid ↝ mul_one_class -/
#check @submonoid.coe_mul_self_eq /- _inst_1: monoid ↝ mul_one_class -/
#check @add_submonoid.coe_add_self_eq /- _inst_1: add_monoid ↝ add_zero_class -/
#check @submonoid.closure_mul_le /- _inst_1: monoid ↝ mul_one_class -/
#check @add_submonoid.closure_add_le /- _inst_1: add_monoid ↝ add_zero_class -/

-- data/set_like/basic.lean
#check @set_like.has_mem /- i: set_like ↝ has_coe_t -/
#check @set_like.has_coe_to_sort /- i: set_like ↝ has_mem -/
#check @set_like.coe_mk /- i: set_like ↝ has_mem -/

-- data/vector/basic.lean
#check @vector.comp_traverse /- _inst_3: is_lawful_applicative ↝ -/

-- data/zmod/basic.lean
#check @zmod.cast_add /- _inst_1: ring ↝ non_assoc_ring -/
#check @zmod.ring_hom_eq_of_ker_eq /- _inst_1: comm_ring ↝ ring -/

-- deprecated/group.lean
#check @is_add_hom.add /- _inst_4: add_semigroup ↝ has_add -/
#check @is_mul_hom.mul /- _inst_4: semigroup ↝ has_mul -/
#check @add_equiv.is_add_hom /- _inst_1: add_zero_class ↝ has_add -/
#check @add_equiv.is_add_hom /- _inst_2: add_zero_class ↝ has_add -/
#check @mul_equiv.is_mul_hom /- _inst_1: mul_one_class ↝ has_mul -/
#check @mul_equiv.is_mul_hom /- _inst_2: mul_one_class ↝ has_mul -/
#check @is_add_hom.to_is_add_monoid_hom /- _inst_2: add_group ↝ add_left_cancel_monoid -/
#check @is_mul_hom.to_is_monoid_hom /- _inst_2: group ↝ left_cancel_monoid -/
#check @ring_hom.to_is_add_group_hom /- _inst_1: ring ↝ non_assoc_ring -/
#check @ring_hom.to_is_add_group_hom /- _inst_2: ring ↝ non_assoc_ring -/

-- deprecated/subgroup.lean
#check @is_subgroup.trivial /- _inst_2: group ↝ has_one -/
#check @is_add_subgroup.trivial /- _inst_2: add_group ↝ has_zero -/
#check @is_subgroup.center /- _inst_2: group ↝ has_mul -/
#check @is_add_subgroup.add_center /- _inst_2: add_group ↝ has_add -/

-- deprecated/submonoid.lean
#check @powers /- _inst_1: monoid ↝ has_pow -/

-- dynamics/flow.lean
#check @is_fw_invariant /- _inst_1: preorder ↝ has_le -/
#check @flow.is_invariant_iff_image_eq /- _inst_3: topological_add_group ↝ has_continuous_add -/

-- dynamics/omega_limit.lean
#check @flow.omega_limit_image_eq /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @flow.omega_limit_omega_limit /- _inst_3: topological_add_group ↝ has_continuous_add -/

-- field_theory/adjoin.lean
#check @intermediate_field.lifts /- _inst_3: field ↝ semiring -/

-- field_theory/finite/basic.lean
#check @finite_field.prod_univ_units_id_eq_neg_one /- _inst_2: is_domain ↝ no_zero_divisors -/
#check @finite_field.X_pow_card_sub_X_nat_degree_eq /- _inst_3: field ↝ euclidean_domain -/

-- field_theory/finite/galois_field.lean
#check @galois_poly_separable /- _inst_1: field ↝ comm_ring -/

-- field_theory/finite/polynomial.lean
#check @mv_polynomial.indicator /- _inst_1: field ↝ comm_ring -/
#check @mv_polynomial.evalₗ /- _inst_2: fintype ↝ -/
#check @mv_polynomial.evalₗ /- _inst_3: fintype ↝ -/
#check @mv_polynomial.R /- _inst_1: fintype ↝

-- field_theory/galois.lean
#check @is_galois.integral /- _inst_4: is_galois ↝ normal -/
#check @is_galois.separable /- _inst_4: is_galois ↝ is_separable -/
#check @is_galois.splits /- _inst_4: is_galois ↝ normal -/

-- field_theory/is_alg_closed/algebraic_closure.lean
#check @algebraic_closure.monic_irreducible /- _inst_1: field ↝ ring -/

-- field_theory/is_alg_closed/basic.lean
#check @is_alg_closed.exists_eval₂_eq_zero /- _inst_2: field ↝ division_ring -/

-- field_theory/is_alg_closed/classification.lean

-- field_theory/minpoly.lean
#check @minpoly.dvd_map_of_is_scalar_tower /- _inst_6: comm_ring ↝ ring -/
#check @minpoly.eq_of_algebra_map_eq /- _inst_6: comm_ring ↝ ring -/
#check @minpoly.coeff_zero_eq_zero /- _inst_2: ring ↝ euclidean_domain -/

-- field_theory/perfect_closure.lean
#check @perfect_closure.eq_iff /- _inst_2: is_domain ↝ is_reduced -/

-- field_theory/primitive_element.lean
#check @field.primitive_element_inf_aux_exists_c /- _inst_1: field ↝ division_ring

-- field_theory/ratfunc.lean
#check @ratfunc.lift_on_condition_of_lift_on'_condition /- hdomain: is_domain ↝ no_zero_divisors -/

-- field_theory/separable.lean
#check @polynomial.contract /- _inst_1: comm_semiring ↝ semiring -/
#check @is_separable_tower_top_of_is_separable /- _inst_1: field ↝ comm_ring -/
#check @is_separable_tower_top_of_is_separable /- _inst_3: field ↝ comm_ring -/
#check @is_separable_tower_bot_of_is_separable /- _inst_3: field ↝ euclidean_domain -/

-- field_theory/splitting_field.lean
#check @polynomial.splits /- _inst_1: field ↝ semiring -/
#check @polynomial.splits /- _inst_2: field ↝ ring -/
#check @polynomial.factor /- _inst_1: field ↝ ring -/

-- field_theory/subfield.lean
#check @ring_hom.restrict_field /- _inst_2: field ↝ non_assoc_semiring -/
#check @ring_hom.eq_of_eq_on_subfield_top /- _inst_2: field ↝ non_assoc_semiring -/

-- field_theory/tower.lean
#check @finite_dimensional.right /- _inst_2: field ↝ division_ring -/
#check @finite_dimensional.right /- _inst_4: algebra ↝ has_scalar -/

-- geometry/euclidean/basic.lean
#check @euclidean_geometry.angle /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.dist_left_midpoint_eq_dist_right_midpoint /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.inner_weighted_vsub /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.inner_vsub_vsub_of_dist_eq_of_dist_eq /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.dist_smul_vadd_sq /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @euclidean_geometry.cospherical /- _inst_2: metric_space ↝ has_dist -/

-- geometry/euclidean/monge_point.lean
#check @affine.simplex.monge_plane /- _inst_2: metric_space ↝ pseudo_metric_space -/
#check @affine.simplex.altitude /- _inst_2: metric_space ↝ pseudo_metric_space -/

-- geometry/euclidean/sphere.lean
#check @euclidean_geometry.mul_dist_eq_abs_sub_sq_dist /- _inst_2: metric_space ↝ pseudo_metric_space -/

-- geometry/manifold/algebra/monoid.lean
#check @smooth_left_mul_one /- _inst_14: monoid ↝ mul_one_class -/
#check @smooth_right_mul_one /- _inst_14: monoid ↝ mul_one_class -/

-- geometry/manifold/algebra/smooth_functions.lean
#check @smooth_map.has_zero /- _inst_15: add_monoid ↝ has_zero -/
#check @smooth_map.has_one /- _inst_15: monoid ↝ has_one -/

-- geometry/manifold/cont_mdiff.lean
#check @cont_mdiff_within_at_iff' /- Is: smooth_manifold_with_corners ↝ has_groupoid
I's: smooth_manifold_with_corners ↝ has_groupoid -/
#check @cont_mdiff_on_iff /- Is: smooth_manifold_with_corners ↝ has_groupoid
I's: smooth_manifold_with_corners ↝ has_groupoid -/
#check @cont_mdiff_within_at_iff_cont_mdiff_on_nhds /- Is: smooth_manifold_with_corners ↝ has_groupoid
I's: smooth_manifold_with_corners ↝ has_groupoid -/
#check @cont_mdiff_on_of_mem_maximal_atlas /- Is: smooth_manifold_with_corners ↝ has_groupoid -/
#check @cont_mdiff_on_symm_of_mem_maximal_atlas /- Is: smooth_manifold_with_corners ↝ has_groupoid -/

-- geometry/manifold/diffeomorph.lean
#check @diffeomorph.smooth_manifold_with_corners_trans_diffeomorph /- _inst_17: smooth_manifold_with_corners ↝ has_groupoid -/

-- geometry/manifold/mfderiv.lean
#check @mdifferentiable_at_atlas /- _inst_7: smooth_manifold_with_corners ↝ has_groupoid -/
#check @mdifferentiable_at_atlas_symm /- _inst_7: smooth_manifold_with_corners ↝ has_groupoid -/

-- geometry/manifold/smooth_manifold_with_corners.lean
#check @smooth_manifold_with_corners.mem_maximal_atlas_of_mem_atlas /- _inst_7: smooth_manifold_with_corners ↝ has_groupoid -/
#check @smooth_manifold_with_corners.chart_mem_maximal_atlas /- _inst_7: smooth_manifold_with_corners ↝ has_groupoid -/
#check @smooth_manifold_with_corners.prod /- _inst_16: smooth_manifold_with_corners ↝ has_groupoid -/
#check @smooth_manifold_with_corners.prod /- _inst_19: smooth_manifold_with_corners ↝ has_groupoid -/
#check @topological_space.opens.smooth_manifold_with_corners /- _inst_7: smooth_manifold_with_corners ↝ has_groupoid -/

-- group_theory/abelianization.lean
#check @abelianization.hom_ext /- _inst_2: monoid ↝ mul_one_class -/

-- group_theory/complement.lean
#check @subgroup.is_complement /- _inst_1: group ↝ has_mul -/
#check @add_subgroup.is_complement /- _inst_1: add_group ↝ has_add -/

-- group_theory/coset.lean
#check @one_left_coset /- _inst_1: monoid ↝ mul_one_class -/
#check @zero_left_add_coset /- _inst_1: add_monoid ↝ add_zero_class -/
#check @right_coset_one /- _inst_1: monoid ↝ mul_one_class -/
#check @right_add_coset_zero /- _inst_1: add_monoid ↝ add_zero_class -/
#check @mem_own_left_add_coset /- _inst_1: add_monoid ↝ add_zero_class -/
#check @mem_own_left_coset /- _inst_1: monoid ↝ mul_one_class -/
#check @mem_own_right_add_coset /- _inst_1: add_monoid ↝ add_zero_class -/
#check @mem_own_right_coset /- _inst_1: monoid ↝ mul_one_class -/

-- group_theory/double_coset.lean
#check @doset.setoid /- _inst_1: group ↝ has_mul -/

-- group_theory/exponent.lean
#check @add_monoid.lcm_add_order_eq_exponent /- _inst_1: add_left_cancel_monoid ↝ add_monoid -/
#check @monoid.lcm_order_eq_exponent /- _inst_1: left_cancel_monoid ↝ monoid -/
#check @monoid.exponent_eq_supr_order_of /- _inst_1: cancel_comm_monoid ↝ comm_monoid -/
#check @add_monoid.exponent_eq_supr_order_of /- _inst_1: add_cancel_comm_monoid ↝ add_comm_monoid -/

-- group_theory/finiteness.lean
#check @submonoid.fg /- _inst_1: monoid ↝ mul_one_class -/
#check @add_submonoid.fg /- _inst_1: add_monoid ↝ add_zero_class -/

-- group_theory/group_action/basic.lean
#check @add_action.orbit /- _inst_2: add_action ↝ has_vadd -/
#check @mul_action.orbit /- _inst_2: mul_action ↝ has_scalar -/
#check @mul_action.fixed_points /- _inst_2: mul_action ↝ has_scalar -/
#check @add_action.fixed_points /- _inst_2: add_action ↝ has_vadd -/
#check @mul_action.fixed_by /- _inst_2: mul_action ↝ has_scalar -/
#check @add_action.fixed_by /- _inst_2: add_action ↝ has_vadd -/

-- group_theory/group_action/units.lean
#check @units.coe_smul /- _inst_4: smul_comm_class ↝ mul_action -/
#check @units.coe_smul /- _inst_5: is_scalar_tower ↝ mul_action -/
#check @units.coe_smul /- _inst_4: smul_comm_class ↝ mul_action -/
#check @units.coe_smul /- _inst_5: is_scalar_tower ↝ mul_action -/
#check @units.smul_comm_class' /- _inst_5: smul_comm_class ↝ mul_action -/
#check @units.smul_comm_class' /- _inst_7: smul_comm_class ↝ mul_action -/
#check @units.smul_comm_class' /- _inst_8: is_scalar_tower ↝ mul_action -/
#check @units.smul_comm_class' /- _inst_9: is_scalar_tower ↝ mul_action -/
#check @units.is_scalar_tower' /- _inst_6: smul_comm_class ↝ mul_action -/
#check @units.is_scalar_tower' /- _inst_8: smul_comm_class ↝ mul_action -/
#check @units.is_scalar_tower' /- _inst_9: is_scalar_tower ↝ mul_action -/
#check @units.is_scalar_tower' /- _inst_10: is_scalar_tower ↝ mul_action -/
#check @units.is_scalar_tower'_left /- _inst_6: smul_comm_class ↝ mul_action -/
#check @units.is_scalar_tower'_left /- _inst_7: is_scalar_tower ↝ mul_action -/

-- group_theory/monoid_localization.lean
#check @localization.r /- _inst_1: comm_monoid ↝ mul_one_class -/
#check @add_localization.r /- _inst_1: add_comm_monoid ↝ add_zero_class -/
#check @submonoid.localization_map.mul_inv_left /- _inst_1: comm_monoid ↝ monoid -/
#check @add_submonoid.localization_map.add_neg_left /- _inst_1: add_comm_monoid ↝ add_monoid -/
#check @add_submonoid.localization_map.is_add_unit_comp /- _inst_3: add_comm_monoid ↝ add_monoid -/
#check @submonoid.localization_map.is_unit_comp /- _inst_3: comm_monoid ↝ monoid -/

-- group_theory/nielsen_schreier.lean
#check @is_free_groupoid.generators /- _inst_1: category_theory.groupoid ↝ -/

-- group_theory/order_of_element.lean
#check @mem_multiples_iff_mem_range_add_order_of' /- _inst_1: add_left_cancel_monoid ↝ add_monoid -/
#check @mem_powers_iff_mem_range_order_of' /- _inst_1: left_cancel_monoid ↝ monoid -/
#check @pow_eq_one_iff_modeq /- _inst_1: left_cancel_monoid ↝ monoid -/
#check @nsmul_inj_iff_of_add_order_of_eq_zero /- _inst_1: add_group ↝ add_left_cancel_monoid -/
#check @pow_inj_iff_of_order_of_eq_zero /- _inst_1: group ↝ left_cancel_monoid -/
#check @order_eq_card_powers /- _inst_5: decidable_eq ↝ decidable_pred -/
#check @add_order_of_eq_card_multiples /- _inst_5: decidable_eq ↝ decidable_pred -/
#check @decidable_zpowers /- _inst_5: decidable_eq ↝ decidable_pred -/
#check @decidable_zmultiples /- _inst_5: decidable_eq ↝ decidable_pred -/
#check @order_eq_card_zpowers /- _inst_5: decidable_eq ↝ decidable_pred -/
#check @add_order_eq_card_zmultiples /- _inst_5: decidable_eq ↝ decidable_pred -/

-- group_theory/quotient_group.lean
#check @quotient_group.monoid_hom_ext /- _inst_2: group ↝ mul_one_class -/
#check @quotient_add_group.add_monoid_hom_ext /- _inst_2: add_group ↝ add_zero_class -/

-- group_theory/subgroup/basic.lean
#check @group.conjugates_of_set /- _inst_1: group ↝ monoid -/
#check @monoid_hom.restrict /- _inst_3: group ↝ mul_one_class -/
#check @add_monoid_hom.restrict /- _inst_3: add_group ↝ add_zero_class -/
#check @monoid_hom.comap_ker /- _inst_4: group ↝ mul_one_class -/
#check @add_monoid_hom.comap_ker /- _inst_4: add_group ↝ add_zero_class -/
#check @monoid_hom.eq_of_eq_on_top /- _inst_3: group ↝ mul_one_class -/
#check @add_monoid_hom.eq_of_eq_on_top /- _inst_3: add_group ↝ add_zero_class -/
#check @monoid_hom.fintype_mrange /- _inst_5: monoid ↝ mul_one_class -/
#check @monoid_hom.fintype_mrange /- _inst_6: monoid ↝ mul_one_class -/
#check @add_monoid_hom.fintype_mrange /- _inst_5: add_monoid ↝ add_zero_class -/
#check @add_monoid_hom.fintype_mrange /- _inst_6: add_monoid ↝ add_zero_class -/
#check @add_subgroup.ker_saturated /- _inst_4: add_comm_group ↝ add_group -/
#check @add_subgroup.ker_saturated /- _inst_5: add_comm_group ↝ add_comm_monoid -/

-- group_theory/submonoid/pointwise.lean
#check @add_submonoid.mem_smul_pointwise_iff_exists /- _inst_3: group ↝ monoid -/

-- group_theory/subsemigroup/basic.lean
#check @mul_hom.eq_of_eq_on_mtop /- _inst_3: mul_one_class ↝ has_mul -/
#check @add_hom.eq_of_eq_on_mtop /- _inst_3: add_zero_class ↝ has_add -/

-- group_theory/torsion.lean
#check @exponent_exists.is_add_torsion /- _inst_1: add_group ↝ add_monoid -/
#check @exponent_exists.is_torsion /- _inst_1: group ↝ monoid -/
#check @is_torsion.exponent_exists /- _inst_1: group ↝ monoid -/
#check @is_add_torsion.exponent_exists /- _inst_1: add_group ↝ add_monoid -/

-- linear_algebra/affine_space/affine_map.lean
#check @affine_map.coe_smul /- _inst_16: smul_comm_class ↝ mul_action -/

-- linear_algebra/affine_space/affine_subspace.lean
#check @vector_span /- _inst_1: ring ↝ semiring -/
#check @vector_span /- _inst_4: add_torsor ↝ has_vsub -/

-- linear_algebra/affine_space/basis.lean
#check @affine_basis.exists_affine_basis /- _inst_3: field ↝ division_ring -/

-- linear_algebra/affine_space/combination.lean
#check @finset.weighted_vsub_of_point /- S: add_torsor ↝ has_vsub -/

-- linear_algebra/alternating.lean
#check @alternating_map.smul_apply /- _inst_13: smul_comm_class ↝ has_scalar -/
#check @alternating_map.coe_fn_smul /- _inst_13: smul_comm_class ↝ has_scalar -/

-- linear_algebra/basic.lean
#check @pi_eq_sum_univ /- _inst_2: semiring ↝ non_assoc_semiring -/
#check @linear_map.ker_eq_bot_of_inverse /- _inst_12: ring_hom_inv_pair ↝ ring_hom_comp_triple -/
#check @linear_map.sub_mem_ker_iff /- _inst_1: ring ↝ semiring -/
#check @linear_map.sub_mem_ker_iff /- _inst_2: ring ↝ semiring -/
#check @linear_map.disjoint_ker' /- _inst_2: ring ↝ semiring -/
#check @linear_map.ker_le_iff /- _inst_2: ring ↝ semiring -/
#check @linear_map.ker_le_iff /- _inst_5: add_comm_group ↝ add_comm_monoid -/
#check @linear_map.submodule_image_apply_of_le /- _inst_11: add_comm_group ↝ add_comm_monoid -/
#check @linear_equiv.smul_of_ne_zero /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @submodule.inf_comap_le_comap_add /- _inst_1: comm_semiring ↝ semiring -/
#check @submodule.inf_comap_le_comap_add /- _inst_2: comm_semiring ↝ semiring -/

-- linear_algebra/basis.lean
#check @basis.no_zero_smul_divisors /- _inst_6: no_zero_divisors ↝ no_zero_smul_divisors -/
#check @basis.group_smul_span_eq_top /- _inst_9: distrib_mul_action ↝ has_scalar -/
#check @basis.group_smul_span_eq_top /- _inst_10: distrib_mul_action ↝ mul_action -/
#check @linear_map.exists_extend /- _inst_3: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/bilinear_form.lean
#check @bilin_form.ne_zero_of_not_is_ortho_self /- _inst_13: field ↝ semiring -/
#check @bilin_form.ne_zero_of_not_is_ortho_self /- _inst_14: add_comm_group ↝ add_comm_monoid -/
#check @bilin_form.is_ortho_smul_left /- _inst_21: is_domain ↝ no_zero_divisors
#check @bilin_form.is_ortho_smul_right /- _inst_21: is_domain ↝ no_zero_divisors
#check @bilin_form.is_alt.neg /- _inst_5: add_comm_group ↝ add_comm_monoid -/
#check @bilin_form.is_skew_adjoint /- _inst_4: ring ↝ semiring -/

-- linear_algebra/bilinear_map.lean
#check @linear_map.ext₂ /- _inst_30: smul_comm_class ↝ module -/
#check @linear_map.congr_fun₂ /- _inst_30: smul_comm_class ↝ module -/
#check @linear_map.ext_basis /- _inst_1: comm_ring ↝ semiring -/
#check @linear_map.ext_basis /- _inst_5: add_comm_group ↝ add_comm_monoid -/
#check @linear_map.ext_basis /- _inst_12: smul_comm_class ↝ module -/

-- linear_algebra/determinant.lean
#check @equiv_of_pi_lequiv_pi /- _inst_12: nontrivial ↝ invariant_basis_number -/

-- linear_algebra/dimension.lean
#check @dim_le /- _inst_1: ring ↝ semiring -/
#check @dim_le /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @dim_le /- _inst_2: add_comm_group ↝ add_comm_monoid
#check @dim_range_of_surjective /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @dim_punit /- _inst_1: ring ↝ semiring -/
#check @basis.le_span'' /- _inst_3: add_comm_group ↝ add_comm_monoid -/
#check @rank /- _inst_2: add_comm_group ↝ add_comm_monoid

-- linear_algebra/dual.lean
#check @module.dual /- _inst_1: comm_semiring ↝ semiring -/
#check @module.dual.add_comm_group /- _inst_5: add_comm_group ↝ add_comm_monoid -/
#check @dual_pair.lc /- _inst_1: comm_ring ↝ semiring -/
#check @dual_pair.lc /- _inst_3: module ↝ has_scalar -/
#check @subspace.quot_dual_equiv_annihilator /- _inst_6: finite_dimensional ↝ finite_dimensional -/

-- linear_algebra/finite_dimensional.lean
#check @finite_dimensional /- _inst_1: division_ring ↝ semiring -/
#check @finite_dimensional /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @finite_dimensional.finrank /- _inst_7: add_comm_group ↝ add_comm_monoid -/
#check @finite_dimensional.finrank_eq_of_dim_eq /- _inst_1: division_ring ↝ semiring -/
#check @finite_dimensional.finite_dimensional_of_finrank_eq_succ /- _inst_6: field ↝ division_ring -/
#check @finite_dimensional.fact_finite_dimensional_of_finrank_eq_succ /- _inst_6: field ↝ division_ring -/
#check @finrank_eq_zero_of_dim_eq_zero /- _inst_1: field ↝ division_ring -/
#check @linear_equiv.finite_dimensional /- _inst_1: field ↝ division_ring -/
#check @finite_dimensional.nonempty_linear_equiv_of_finrank_eq /- _inst_1: field ↝ division_ring -/
#check @linear_map.finite_dimensional_of_surjective /- _inst_1: field ↝ division_ring -/
#check @finrank_zero_iff_forall_zero /- _inst_1: field ↝ division_ring -/
#check @finrank_eq_one_iff /- _inst_1: field ↝ division_ring -/

-- linear_algebra/free_module/finite/basic.lean
#check @module.finite.of_basis /- _inst_8: comm_ring ↝ semiring -/
#check @module.finite.of_basis /- _inst_9: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/free_module/pid.lean
#check @eq_bot_of_generator_maximal_map_eq_zero /- _inst_2: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/general_linear_group.lean
#check @matrix.general_linear_group /- _inst_3: comm_ring ↝ ring -/

-- linear_algebra/invariant_basis_number.lean
#check @noetherian_ring_strong_rank_condition /- _inst_3: is_noetherian_ring ↝ is_noetherian -/

-- linear_algebra/linear_independent.lean
#check @linear_independent_iff_injective_total /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @linear_independent.group_smul /- _inst_1: ring ↝ semiring -/
#check @linear_independent.group_smul /- _inst_9: distrib_mul_action ↝ has_scalar -/
#check @linear_independent.units_smul /- _inst_1: ring ↝ semiring -/
#check @linear_independent.units_smul /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @linear_independent.image_subtype /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @linear_independent_monoid_hom /- _inst_8: monoid ↝ mul_one_class -/

-- linear_algebra/matrix/basis.lean
#check @basis.to_matrix /- _inst_2: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/matrix/block.lean
#check @matrix.block_triangular_matrix' /- _inst_5: comm_ring ↝ has_zero -/
#check @matrix.block_triangular_matrix /- _inst_5: comm_ring ↝ has_zero -/

-- linear_algebra/matrix/charpoly/basic.lean
#check @charmatrix /- _inst_1: comm_ring ↝ ring -/

-- linear_algebra/matrix/circulant.lean
#check @matrix.circulant_mul /- _inst_1: semiring ↝ non_unital_non_assoc_semiring -/

-- linear_algebra/matrix/nondegenerate.lean
#check @matrix.nondegenerate /- _inst_2: comm_ring ↝ non_unital_non_assoc_semiring -/
#check @matrix.nondegenerate_of_det_ne_zero /- _inst_4: is_domain ↝ no_zero_divisors -/

-- linear_algebra/matrix/transvection.lean
#check @matrix.transvection /- _inst_4: comm_ring ↝ semiring -/
#check @matrix.transvection_struct.det_to_matrix_prod /- _inst_1: field ↝ comm_ring -/

-- linear_algebra/multilinear/basic.lean
#check @multilinear_map.smul_apply /- _inst_18: smul_comm_class ↝ has_scalar -/
#check @multilinear_map.coe_smul /- _inst_18: smul_comm_class ↝ has_scalar -/

-- linear_algebra/orientation.lean
#check @basis.adjust_to_orientation /- _inst_1: linear_ordered_comm_ring ↝ ordered_comm_ring -/

-- linear_algebra/pi_tensor_product.lean
#check @pi_tensor_product.smul_tprod_coeff' /- _inst_14: smul_comm_class ↝ has_scalar -/

-- linear_algebra/prod.lean
#check @linear_map.ker_prod_ker_le_ker_coprod /- _inst_12: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/projection.lean
#check @linear_map.of_is_compl /- _inst_4: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/projective_space/basic.lean
#check @projectivization_setoid /- _inst_3: module ↝ mul_action -/

-- linear_algebra/quadratic_form/basic.lean
#check @quadratic_form.polar /- _inst_1: add_comm_group ↝ has_add -/
#check @quadratic_form.polar /- _inst_2: ring ↝ has_sub -/
#check @quadratic_form.coe_fn_smul /- _inst_8: smul_comm_class ↝ has_scalar -/
#check @quadratic_form.smul_apply /- _inst_8: smul_comm_class ↝ has_scalar -/

-- linear_algebra/quotient.lean
#check @submodule.quot_hom_ext /- _inst_4: add_comm_group ↝ add_comm_monoid -/
#check @submodule.linear_map_qext /- _inst_5: add_comm_group ↝ add_comm_monoid -/
#check @linear_map.ker_le_range_iff /- _inst_1: ring ↝ semiring -/
#check @linear_map.ker_le_range_iff /- _inst_3: ring ↝ semiring -/

-- linear_algebra/ray.lean
#check @same_ray /- _inst_3: module ↝ has_scalar -/
#check @smul_ray_of_ne_zero /- _inst_9: smul_comm_class ↝ mul_action -/

-- linear_algebra/sesquilinear_form.lean
#check @linear_map.is_ortho /- _inst_2: comm_semiring ↝ semiring -/
#check @linear_map.is_ortho /- _inst_2: field ↝ comm_semiring -/
#check @linear_map.is_ortho /- _inst_3: add_comm_group ↝ add_comm_monoid
#check @linear_map.separating_left /- _inst_2: comm_semiring ↝ semiring
#check @linear_map.separating_right /- _inst_2: comm_semiring ↝ semiring

-- linear_algebra/span.lean
#check @submodule.span_singleton_smul_le /- _inst_9: mul_action ↝ has_scalar -/
#check @linear_map.span_singleton_sup_ker_eq_top /- _inst_1: field ↝ division_ring -/

-- linear_algebra/tensor_product.lean
#check @tensor_product.smul_tmul' /- _inst_16: smul_comm_class ↝ has_scalar -/
#check @tensor_product.tmul_smul /- _inst_16: smul_comm_class ↝ has_scalar -/
#check @tensor_product.tmul_smul /- _inst_19: is_scalar_tower ↝ is_scalar_tower -/
#check @tensor_product.neg.aux /- _inst_3: add_comm_group ↝ add_comm_monoid -/

-- linear_algebra/unitary_group.lean
#check @matrix.unitary_group /- _inst_3: comm_ring ↝ ring -/

-- linear_algebra/vandermonde.lean
#check @matrix.vandermonde /- _inst_1: comm_ring ↝ has_pow -/

-- logic/basic.lean
#check @coe_coe /- _inst_1: has_coe ↝ has_lift_t -/
#check @coe_coe /- _inst_2: has_coe_t ↝ has_lift_t -/
#check @coe_fn_coe_trans /- _inst_3: has_coe_to_fun ↝ has_coe_to_fun -/
#check @coe_sort_coe_trans /- _inst_2: has_coe_t_aux ↝ has_coe_to_sort -/

-- logic/encodable/basic.lean
#check @directed.le_sequence /- _inst_3: preorder ↝ has_le -/

-- logic/equiv/transfer_instance.lean

-- logic/unique.lean
#check @unique.bijective /- _inst_2: unique ↝ subsingleton -/

-- measure_theory/constructions/borel_space.lean
#check @measurable_set_of_continuous_at /- _inst_14: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_set_le' /- _inst_16: partial_order ↝ preorder -/
#check @dense.borel_eq_generate_from_Ico_mem /- _inst_23: no_min_order ↝ no_bot_order -/
#check @dense.borel_eq_generate_from_Ioc_mem /- _inst_23: no_max_order ↝ no_top_order -/
#check @topological_group.has_measurable_inv /- _inst_17: topological_group ↝ has_continuous_inv -/
#check @topological_add_group.has_measurable_neg /- _inst_17: topological_add_group ↝ has_continuous_neg -/
#check @measurable_of_continuous_on_compl_singleton /- _inst_16: t1_space ↝ measurable_singleton_class -/
#check @monotone.measurable /- _inst_6: borel_space ↝ opens_measurable_space -/
#check @is_R_or_C.measurable_space /- _inst_1: is_R_or_C ↝ topological_space -/
#check @measurable_set_ball /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable_set_closed_ball /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable_inf_dist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable_inf_nndist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable_dist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable.dist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable_nndist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @measurable.nndist /- _inst_1: metric_space ↝ pseudo_metric_space -/
#check @tendsto_measure_cthickening /- _inst_1: metric_space ↝ pseudo_emetric_space -/
#check @measurable_set_eball /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_edist_right /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_edist_left /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_inf_edist /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_edist /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable.edist /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @ae_measurable.edist /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measurable_norm /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measurable_nnnorm /- _inst_2: normed_group ↝ semi_normed_group -/
#check @continuous_linear_map.measurable /- _inst_4: normed_space ↝ module -/
#check @continuous_linear_map.measurable /- _inst_8: normed_space ↝ module -/

-- measure_theory/constructions/polish.lean
#check @measurable.exists_continuous /- _inst_7: borel_space ↝ opens_measurable_space -/
#check @measure_theory.measurably_separable_range_of_disjoint /- _inst_4: borel_space ↝ opens_measurable_space -/

-- measure_theory/covering/besicovitch.lean
#check @besicovitch.exist_finset_disjoint_balls_large_measure /- _inst_2: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- measure_theory/covering/differentiation.lean
#check @vitali_family.measure_le_of_frequently_le /- _inst_3: borel_space ↝ measure_theory.measure.outer_regular -/
#check @vitali_family.measure_le_of_frequently_le /- _inst_4: measure_theory.is_locally_finite_measure ↝ measure_theory.measure.outer_regular -/

-- measure_theory/covering/vitali.lean
#check @vitali.exists_disjoint_subfamily_covering_enlargment_closed_ball /- _inst_1: metric_space ↝ pseudo_metric_space -/

-- measure_theory/covering/vitali_family.lean
#check @vitali_family.fine_subfamily_on.index_countable /- _inst_2: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- measure_theory/function/ae_eq_fun.lean
#check @measure_theory.ae_eq_fun.smul_comm_class /- _inst_9: smul_comm_class ↝ smul_comm_class -/

-- measure_theory/function/ae_eq_of_integral.lean
#check @measure_theory.ae_eq_zero_of_forall_inner /- _inst_3: topological_space.second_countable_topology ↝ topological_space.separable_space -/
#check @measure_theory.ae_eq_zero_of_forall_dual /- _inst_4: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- measure_theory/function/ae_measurable_sequence.lean
#check @ae_seq.supr /- _inst_3: complete_lattice ↝ has_Sup -/

-- measure_theory/function/conditional_expectation.lean
#check @measure_theory.ae_strongly_measurable'.sub /- _inst_3: topological_add_group ↝ has_continuous_sub -/

-- measure_theory/function/convergence_in_measure.lean
#check @measure_theory.exists_seq_tendsto_ae.exists_nat_measure_lt_two_inv /- _inst_1: metric_space ↝ has_dist -/
#check @measure_theory.tendsto_in_measure.exists_seq_tendsto_in_measure_at_top /- _inst_1: metric_space ↝ has_dist -/
#check @measure_theory.tendsto_in_measure.ae_measurable /- _inst_2: normed_group ↝ metric_space -/

-- measure_theory/function/egorov.lean
#check @measure_theory.egorov.not_convergent_seq /- _inst_1: metric_space ↝ has_dist -/
#check @measure_theory.egorov.not_convergent_seq /- _inst_2: preorder ↝ has_le -/

-- measure_theory/function/ess_sup.lean
#check @ess_sup_const /- _inst_1: complete_lattice ↝ conditionally_complete_lattice -/
#check @ess_sup_smul_measure /- _inst_1: complete_lattice ↝ conditionally_complete_lattice -/
#check @ennreal.ess_sup_liminf_le /- _inst_2: linear_order ↝ preorder -/

-- measure_theory/function/floor.lean
#check @int.measurable_floor /- _inst_5: order_topology ↝ order_closed_topology -/
#check @int.measurable_ceil /- _inst_5: order_topology ↝ order_closed_topology -/
#check @nat.measurable_floor /- _inst_5: order_topology ↝ order_closed_topology -/
#check @nat.measurable_ceil /- _inst_5: order_topology ↝ order_closed_topology -/

-- measure_theory/function/jacobian.lean
#check @exists_partition_approximates_linear_on_of_has_fderiv_within_at /- _inst_7: borel_space ↝ opens_measurable_space -/

-- measure_theory/function/l1_space.lean
#check @measure_theory.lintegral_nnnorm_eq_lintegral_edist /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.lintegral_norm_eq_lintegral_edist /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.lintegral_nnnorm_zero /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.lintegral_nnnorm_neg /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.has_finite_integral /- _inst_2: normed_group ↝ has_nnnorm -/
#check @measure_theory.all_ae_of_real_F_le_bound /- _inst_2: normed_group ↝ has_norm -/
#check @measure_theory.all_ae_tendsto_of_real_norm /- _inst_2: normed_group ↝ semi_normed_group -/

-- measure_theory/function/lp_space.lean
#check @measure_theory.snorm' /- _inst_2: normed_group ↝ has_nnnorm -/
#check @measure_theory.snorm_ess_sup /- _inst_2: normed_group ↝ has_nnnorm -/
#check @continuous_linear_map.smul_comp_Lp /- _inst_9: smul_comm_class ↝ module -/
#check @measure_theory.Lp.snorm'_lim_eq_lintegral_liminf /- _inst_4: nonempty ↝ filter.ne_bot
#check @measure_theory.Lp.snorm_exponent_top_lim_eq_ess_sup_liminf /- _inst_4: nonempty ↝ filter.ne_bot

-- measure_theory/function/simple_func_dense_lp.lean
#check @measure_theory.simple_func.mem_ℒp_approx_on /- _inst_5: borel_space ↝ opens_measurable_space -/
#check @measure_theory.simple_func.tendsto_approx_on_range_Lp_snorm /- _inst_5: borel_space ↝ opens_measurable_space -/
#check @measure_theory.simple_func.exists_forall_norm_le /- _inst_3: normed_group ↝ has_norm -/
#check @measure_theory.Lp.simple_func.coe_fn_zero /- _inst_4: normed_lattice_add_comm_group ↝ normed_group -/

-- measure_theory/function/strongly_measurable.lean
#check @measure_theory.strongly_measurable.neg /- _inst_4: topological_add_group ↝ has_continuous_neg -/
#check @measure_theory.strongly_measurable.inv /- _inst_4: topological_group ↝ has_continuous_inv -/
#check @measurable.strongly_measurable /- _inst_5: topological_space.second_countable_topology ↝ topological_space.separable_space -/
#check @measure_theory.strongly_measurable.norm /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.strongly_measurable.nnnorm /- _inst_2: normed_group ↝ semi_normed_group -/
#check @measure_theory.strongly_measurable.measurable_set_le /- _inst_3: linear_order ↝ partial_order -/
#check @measure_theory.fin_strongly_measurable.mul /- _inst_3: monoid_with_zero ↝ mul_zero_class -/
#check @measure_theory.fin_strongly_measurable.add /- _inst_3: add_monoid ↝ add_zero_class -/
#check @measure_theory.fin_strongly_measurable.neg /- _inst_4: topological_add_group ↝ has_continuous_neg -/
#check @measure_theory.fin_strongly_measurable.const_smul /- _inst_7: has_continuous_smul ↝ has_continuous_const_smul -/
#check @measure_theory.ae_strongly_measurable.div /- _inst_5: topological_group ↝ has_continuous_div -/
#check @measure_theory.ae_strongly_measurable.sub /- _inst_5: topological_add_group ↝ has_continuous_sub -/
#check @measure_theory.ae_strongly_measurable.sup /- _inst_4: semilattice_sup ↝ has_sup -/
#check @measure_theory.ae_strongly_measurable.inf /- _inst_4: semilattice_inf ↝ has_inf -/
#check @measure_theory.ae_strongly_measurable.norm /- _inst_4: normed_group ↝ semi_normed_group -/
#check @measure_theory.ae_strongly_measurable.nnnorm /- _inst_4: normed_group ↝ semi_normed_group -/
#check @measure_theory.ae_strongly_measurable.edist /- _inst_4: normed_group ↝ pseudo_emetric_space -/
#check @ae_strongly_measurable_with_density_iff /- _inst_4: normed_group ↝ semi_normed_group -/

-- measure_theory/function/uniform_integrable.lean
#check @measure_theory.tendsto_indicator_ge /- _inst_1: normed_group ↝ semi_normed_group -/
#check @measure_theory.uniform_integrable_subsingleton /- _inst_2: subsingleton ↝ fintype -/

-- measure_theory/group/arithmetic.lean
#check @measurable_neg_iff /- _inst_4: add_group ↝ has_involutive_neg -/
#check @measurable_inv_iff /- _inst_4: group ↝ has_involutive_inv -/
#check @ae_measurable_neg_iff /- _inst_4: add_group ↝ has_involutive_neg -/
#check @ae_measurable_inv_iff /- _inst_4: group ↝ has_involutive_inv -/
#check @measurable_inv_iff₀ /- _inst_4: group_with_zero ↝ has_involutive_inv -/
#check @ae_measurable_inv_iff₀ /- _inst_4: group_with_zero ↝ has_involutive_inv -/
#check @add_submonoid.has_measurable_vadd /- _inst_4: add_action ↝ has_vadd -/
#check @submonoid.has_measurable_smul /- _inst_4: mul_action ↝ has_scalar -/
#check @add_units.has_measurable_vadd /- _inst_4: add_action ↝ has_vadd -/
#check @units.has_measurable_smul /- _inst_4: mul_action ↝ has_scalar -/

-- measure_theory/group/fundamental_domain.lean
#check @measure_theory.is_add_fundamental_domain.mk' /- _inst_1: add_group ↝ add_monoid -/
#check @measure_theory.is_fundamental_domain.mk' /- _inst_1: group ↝ monoid -/
#check @measure_theory.is_fundamental_domain.mono /- _inst_1: group ↝ monoid -/
#check @measure_theory.is_fundamental_domain.mono /- _inst_2: mul_action ↝ has_scalar -/
#check @measure_theory.is_add_fundamental_domain.mono /- _inst_1: add_group ↝ add_monoid -/
#check @measure_theory.is_add_fundamental_domain.mono /- _inst_2: add_action ↝ has_vadd -/

-- measure_theory/group/integration.lean
#check @measure_theory.integrable.comp_inv /- _inst_6: group ↝ has_inv -/
#check @measure_theory.integrable.comp_neg /- _inst_6: add_group ↝ has_neg -/
#check @measure_theory.integral_neg_eq_self /- _inst_6: add_group ↝ has_involutive_neg -/
#check @measure_theory.integral_inv_eq_self /- _inst_6: group ↝ has_involutive_inv -/
#check @measure_theory.integrable.comp_add_left /- _inst_6: add_group ↝ has_add -/
#check @measure_theory.integrable.comp_mul_left /- _inst_6: group ↝ has_mul -/
#check @measure_theory.integrable.comp_add_right /- _inst_6: add_group ↝ has_add -/
#check @measure_theory.integrable.comp_mul_right /- _inst_6: group ↝ has_mul -/

-- measure_theory/group/measure.lean
#check @measure_theory.map_div_right_eq_self /- _inst_2: group ↝ div_inv_monoid -/
#check @measure_theory.map_sub_right_eq_self /- _inst_2: add_group ↝ sub_neg_monoid -/
#check @measure_theory.measure.map_sub_left_eq_self /- _inst_2: add_group ↝ sub_neg_monoid -/
#check @measure_theory.measure.map_div_left_eq_self /- _inst_2: group ↝ div_inv_monoid -/
#check @measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact /- _inst_3: borel_space ↝ has_measurable_mul -/
#check @measure_theory.is_open_pos_measure_of_add_left_invariant_of_compact /- _inst_3: borel_space ↝ has_measurable_add -/
#check @measure_theory.measure_lt_top_of_is_compact_of_is_add_left_invariant /- _inst_3: borel_space ↝ has_measurable_add -/
#check @measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant /- _inst_3: borel_space ↝ has_measurable_mul -/
#check @measure_theory.is_mul_left_invariant.is_mul_right_invariant /- _inst_2: comm_group ↝ comm_semigroup -/
#check @measure_theory.is_mul_left_invariant.is_add_right_invariant /- _inst_2: add_comm_group ↝ add_comm_semigroup -/
#check @measure_theory.measure.is_locally_finite_measure_of_is_add_haar_measure /- _inst_6: measure_theory.measure.is_add_haar_measure ↝ measure_theory.is_finite_measure_on_compacts -/
#check @measure_theory.measure.is_locally_finite_measure_of_is_haar_measure /- _inst_6: measure_theory.measure.is_haar_measure ↝ measure_theory.is_finite_measure_on_compacts -/
#check @measure_theory.measure.add_haar_singleton /- _inst_4: measure_theory.measure.is_add_haar_measure ↝ measure_theory.measure.is_add_left_invariant -/
#check @measure_theory.measure.add_haar_singleton /- _inst_5: topological_add_group ↝ has_measurable_add -/
#check @measure_theory.measure.add_haar_singleton /- _inst_6: borel_space ↝ has_measurable_add -/
#check @measure_theory.measure.haar_singleton /- _inst_4: measure_theory.measure.is_haar_measure ↝ measure_theory.measure.is_mul_left_invariant -/
#check @measure_theory.measure.haar_singleton /- _inst_5: topological_group ↝ has_measurable_mul -/
#check @measure_theory.measure.haar_singleton /- _inst_6: borel_space ↝ has_measurable_mul -/
#check @measure_theory.measure.haar_singleton /- _inst_6: topological_add_group ↝ has_continuous_add -/
#check @measure_theory.measure.haar_singleton /- _inst_12: topological_add_group ↝ has_continuous_add -/
#check @measure_theory.measure.haar_singleton /- _inst_6: topological_group ↝ has_continuous_mul -/
#check @measure_theory.measure.haar_singleton /- _inst_12: topological_group ↝ has_continuous_mul -/
#check @measure_theory.measure.is_add_haar_measure.sigma_finite /- _inst_4: measure_theory.measure.is_add_haar_measure ↝ measure_theory.is_finite_measure_on_compacts -/
#check @measure_theory.measure.is_haar_measure.sigma_finite /- _inst_4: measure_theory.measure.is_haar_measure ↝ measure_theory.is_finite_measure_on_compacts -/

-- measure_theory/integral/bochner.lean
#check @measure_theory.weighted_smul_smul /- _inst_4: normed_space ↝ has_scalar -/

-- measure_theory/integral/divergence_theorem.lean
#check @measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_of_equiv /- _inst_6: partial_order ↝ preorder -/

-- measure_theory/integral/lebesgue.lean
#check @measure_theory.simple_func.coe_le /- _inst_2: preorder ↝ has_le -/
#check @measure_theory.simple_func.has_nat_pow /- _inst_2: monoid ↝ has_pow -/
#check @measure_theory.simple_func.has_int_pow /- _inst_2: div_inv_monoid ↝ has_pow -/
#check @measure_theory.simple_func.fin_meas_supp.add /- _inst_3: add_monoid ↝ add_zero_class -/
#check @measure_theory.simple_func.fin_meas_supp.mul /- _inst_3: monoid_with_zero ↝ mul_zero_class -/
#check @measure_theory.ae_measurable_with_density_iff /- _inst_1: normed_group ↝ semi_normed_group -/

-- measure_theory/integral/set_to_l1.lean
#check @measure_theory.fin_meas_additive /- _inst_8: add_monoid ↝ has_add -/
#check @measure_theory.fin_meas_additive.zero /- _inst_8: add_comm_monoid ↝ add_monoid -/
#check @measure_theory.fin_meas_additive.of_eq_top_imp_eq_top /- _inst_8: add_comm_monoid ↝ add_monoid -/
#check @measure_theory.fin_meas_additive.map_empty_eq_zero /- _inst_9: add_cancel_monoid ↝ add_left_cancel_monoid -/
#check @measure_theory.simple_func.set_to_simple_func /- _inst_3: normed_group ↝ semi_normed_group -/
#check @measure_theory.simple_func.set_to_simple_func /- _inst_5: normed_group ↝ semi_normed_group -/
#check @measure_theory.simple_func.set_to_simple_func_mono_left /- _inst_8: normed_lattice_add_comm_group ↝ normed_linear_ordered_group -/
#check @measure_theory.simple_func.set_to_simple_func_mono_left' /- _inst_8: normed_lattice_add_comm_group ↝ normed_linear_ordered_group -/
#check @measure_theory.simple_func.set_to_simple_func_nonneg /- _inst_8: normed_lattice_add_comm_group ↝ normed_linear_ordered_group
#check @measure_theory.simple_func.set_to_simple_func_nonneg' /- _inst_8: normed_lattice_add_comm_group ↝ normed_linear_ordered_group

-- measure_theory/integral/vitali_caratheodory.lean
#check @measure_theory.simple_func.exists_le_lower_semicontinuous_lintegral_ge /- _inst_3: borel_space ↝ opens_measurable_space -/
#check @measure_theory.simple_func.exists_le_lower_semicontinuous_lintegral_ge /- _inst_4: measure_theory.measure.weakly_regular ↝ measure_theory.measure.outer_regular -/
#check @measure_theory.simple_func.exists_upper_semicontinuous_le_lintegral_le /- _inst_3: borel_space ↝ opens_measurable_space -/

-- measure_theory/measurable_space.lean
#check @measurable_of_empty /- _inst_4: is_empty ↝ subsingleton -/
#check @measurable_set.coe_insert /- _inst_2: measurable_singleton_class ↝ has_insert -/

-- measure_theory/measure/content.lean
#check @measure_theory.content.is_add_left_invariant_inner_content /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @measure_theory.content.is_mul_left_invariant_inner_content /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @measure_theory.content.is_add_left_invariant_outer_measure /- _inst_4: topological_add_group ↝ has_continuous_add -/
#check @measure_theory.content.is_mul_left_invariant_outer_measure /- _inst_4: topological_group ↝ has_continuous_mul -/

-- measure_theory/measure/finite_measure_weak_convergence.lean
#check @measure_theory.finite_measure.coe_smul /- _inst_4: is_scalar_tower ↝ has_scalar

-- measure_theory/measure/haar.lean
#check @measure_theory.measure.haar.add_index /- _inst_1: add_group ↝ has_add -/
#check @measure_theory.measure.haar.index /- _inst_1: group ↝ has_mul -/
#check @measure_theory.measure.sigma_finite_add_haar_measure /- _inst_7: topological_space.second_countable_topology ↝ sigma_compact_space -/
#check @measure_theory.measure.sigma_finite_haar_measure /- _inst_7: topological_space.second_countable_topology ↝ sigma_compact_space -/

-- measure_theory/measure/haar_quotient.lean
#check @subgroup.smul_invariant_measure /- _inst_4: topological_group ↝ has_measurable_mul -/
#check @subgroup.smul_invariant_measure /- _inst_5: borel_space ↝ has_measurable_mul -/
#check @add_subgroup.vadd_invariant_measure /- _inst_4: topological_add_group ↝ has_measurable_add -/
#check @add_subgroup.vadd_invariant_measure /- _inst_5: borel_space ↝ has_measurable_add -/
#check @quotient_group.has_measurable_smul /- _inst_5: borel_space ↝ opens_measurable_space -/
#check @quotient_add_group.has_measurable_vadd /- _inst_5: borel_space ↝ opens_measurable_space -/
#check @measure_theory.is_fundamental_domain.map_restrict_quotient /- _inst_12: measure_theory.measure.is_haar_measure ↝ measure_theory.measure.is_mul_left_invariant -/
#check @measure_theory.is_add_fundamental_domain.map_restrict_quotient /- _inst_12: measure_theory.measure.is_add_haar_measure ↝ measure_theory.measure.is_add_left_invariant -/

-- measure_theory/measure/hausdorff.lean
#check @measure_theory.outer_measure.mk_metric'.pre /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @measure_theory.outer_measure.trim_mk_metric /- _inst_4: borel_space ↝ opens_measurable_space -/

-- measure_theory/measure/measure_space.lean
#check @measure_theory.measure.coe_smul /- _inst_4: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.measure.smul_apply /- _inst_4: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.measure.smul_comm_class /- _inst_4: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.measure.smul_comm_class /- _inst_6: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.measure.is_scalar_tower /- _inst_4: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.measure.is_scalar_tower /- _inst_6: is_scalar_tower ↝ has_scalar -/
#check @measure_Icc_lt_top /- _inst_4: measure_theory.is_locally_finite_measure ↝ measure_theory.is_finite_measure_on_compacts -/

-- measure_theory/measure/open_pos.lean
#check @measure_theory.measure.measure_Ioi_pos /- _inst_3: order_topology ↝ order_closed_topology -/
#check @measure_theory.measure.measure_Iio_pos /- _inst_3: order_topology ↝ order_closed_topology -/
#check @measure_theory.measure.measure_Ioo_pos /- _inst_3: order_topology ↝ order_closed_topology -/
#check @measure_theory.measure.measure_Ioo_eq_zero /- _inst_3: order_topology ↝ order_closed_topology -/
#check @measure_theory.measure.eq_on_Ioo_of_ae_eq /- _inst_3: order_topology ↝ order_closed_topology -/

-- measure_theory/measure/outer_measure.lean
#check @measure_theory.outer_measure.coe_smul /- _inst_2: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.outer_measure.smul_apply /- _inst_2: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.outer_measure.smul_comm_class /- _inst_2: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.outer_measure.smul_comm_class /- _inst_4: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.outer_measure.is_scalar_tower /- _inst_2: is_scalar_tower ↝ has_scalar -/
#check @measure_theory.outer_measure.is_scalar_tower /- _inst_4: is_scalar_tower ↝ has_scalar -/

-- measure_theory/measure/regular.lean
#check @measure_theory.measure.regular.sigma_finite /- _inst_4: measure_theory.measure.regular ↝ measure_theory.is_finite_measure_on_compacts -/
#check @measure_theory.measure.regular.sigma_finite /- _inst_6: borel_space ↝ measure_theory.measure.outer_regular

-- measure_theory/measure/vector_measure.lean
#check @measure_theory.vector_measure.coe_smul /- _inst_5: has_continuous_const_smul ↝ has_scalar -/
#check @measure_theory.vector_measure.smul_apply /- _inst_5: has_continuous_const_smul ↝ has_scalar -/
#check @measure_theory.vector_measure.absolutely_continuous.map /- _inst_7: measure_theory.measure_space ↝ measurable_space -/

-- number_theory/arithmetic_function.lean
#check @nat.arithmetic_function.pmul_zeta /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @nat.arithmetic_function.zeta_pmul /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @nat.arithmetic_function.coe_moebius_mul_coe_zeta /- _inst_1: comm_ring ↝ ring -/
#check @nat.arithmetic_function.sum_eq_iff_sum_mul_moebius_eq /- _inst_1: comm_ring ↝ ring -/

-- number_theory/bernoulli.lean
#check @bernoulli'_power_series /- _inst_1: comm_ring ↝ semiring -/
#check @bernoulli_power_series /- _inst_1: comm_ring ↝ semiring -/

-- number_theory/class_number/admissible_card_pow_degree.lean
#check @polynomial.exists_eq_polynomial /- _inst_1: field ↝ semiring -/
#check @polynomial.exists_approx_polynomial_aux /- _inst_1: field ↝ ring -/

-- number_theory/class_number/finite.lean
#check @class_group.norm_lt /- _inst_16: linear_ordered_comm_ring ↝ linear_ordered_ring -/
#check @class_group.exists_min /- _inst_1: euclidean_domain ↝ comm_ring -/
#check @class_group.exists_min /- _inst_3: is_domain ↝ nontrivial -/

-- number_theory/cyclotomic/basic.lean
#check @cyclotomic_field.algebra_base /- _inst_7: is_domain ↝ -/
#check @cyclotomic_field.algebra_base /- _inst_9: is_fraction_ring ↝ -/

-- number_theory/function_field.lean
#check @function_field /- _inst_2: field ↝ ring -/
#check @function_field /- _inst_2: field ↝ euclidean_domain -/
#check @function_field.ring_of_integers /- _inst_1: field ↝ comm_ring -/
#check @function_field.ring_of_integers /- _inst_2: field ↝ comm_ring -/

-- number_theory/liouville/basic.lean
#check @liouville.exists_one_le_pow_mul_dist /- _inst_1: metric_space ↝ pseudo_metric_space -/

-- number_theory/number_field.lean
#check @number_field.ring_of_integers /- _inst_1: field ↝ comm_ring -/
#check @number_field.ring_of_integers.char_zero /- _inst_3: number_field ↝ char_zero -/

-- number_theory/padics/ring_homs.lean
#check @padic_int.nth_hom /- _inst_1: comm_ring ↝ non_assoc_semiring -/
#check @padic_int.to_zmod_pow_eq_iff_ext /- _inst_1: comm_ring ↝ non_assoc_semiring -/

-- number_theory/zsqrtd/basic.lean
#check @zsqrtd.hom_ext /- _inst_1: comm_ring ↝ ring -/

-- order/atoms.lean
#check @fintype.is_simple_order.card /- _inst_4: decidable_eq ↝ subsingleton -/

-- order/basic.lean
#check @eq.not_lt /- _inst_1: partial_order ↝ preorder -/
#check @ge_iff_le /- _inst_1: preorder ↝ has_le -/
#check @gt_iff_lt /- _inst_1: preorder ↝ has_lt -/
#check @decidable.ne_iff_lt_iff_le /- _inst_2: decidable_rel ↝ decidable_eq -/

-- order/bounded_order.lean
#check @eq_bot_of_bot_eq_top /- _inst_2: bounded_order ↝ bounded_order -/
#check @eq_top_of_bot_eq_top /- _inst_2: bounded_order ↝ bounded_order -/
#check @subsingleton_of_top_le_bot /- _inst_2: bounded_order ↝ bounded_order -/
#check @with_top.lt_iff_exists_coe_btwn /- _inst_1: partial_order ↝ preorder -/
#check @with_top.lt_iff_exists_coe_btwn /- _inst_2: order_bot ↝ has_bot -/
#check @disjoint_top /- _inst_2: bounded_order ↝ bounded_order -/
#check @top_disjoint /- _inst_2: bounded_order ↝ bounded_order -/
#check @inf_eq_bot_iff_le_compl /- _inst_2: bounded_order ↝ bounded_order -/

-- order/bounds.lean
#check @upper_bounds /- _inst_1: preorder ↝ has_le -/
#check @lower_bounds /- _inst_1: preorder ↝ has_le -/

-- order/category/Frame.lean
#check @Frame.hom /- _inst_1: order.frame ↝ complete_lattice -/
#check @Frame.hom /- _inst_2: order.frame ↝ complete_lattice -/

-- order/circular.lean
#check @set.cIcc /- _inst_1: circular_preorder ↝ has_btw -/
#check @set.cIoo /- _inst_1: circular_preorder ↝ has_sbtw -/

-- order/closure.lean
#check @closure_operator.ext /- _inst_1: partial_order ↝ preorder -/
#check @closure_operator.monotone /- _inst_1: partial_order ↝ preorder -/
#check @closure_operator.le_closure /- _inst_1: partial_order ↝ preorder -/
#check @closure_operator.idempotent /- _inst_1: partial_order ↝ preorder -/
#check @closure_operator.closed /- _inst_1: partial_order ↝ preorder -/
#check @lower_adjoint.mem_closed_iff_closure_le /- _inst_2: partial_order ↝ preorder -/
#check @lower_adjoint.closure_is_closed /- _inst_2: partial_order ↝ preorder -/
#check @lower_adjoint.closed_eq_range_close /- _inst_2: partial_order ↝ preorder -/
#check @lower_adjoint.closure_le_closed_iff_le /- _inst_2: partial_order ↝ preorder -/

-- order/complete_lattice.lean
#check @Sup_eq_of_forall_le_of_forall_lt_exists_gt /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @le_supr /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @infi_le /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/
#check @le_supr' /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @infi_le' /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/
#check @is_lub_supr /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @is_glb_infi /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/
#check @is_lub.supr_eq /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @is_glb.infi_eq /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/
#check @supr_le /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @le_infi /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/
#check @infi_const /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/

-- order/complete_lattice_intervals.lean
#check @Sup_within_of_ord_connected /- _inst_1: conditionally_complete_linear_order ↝ conditionally_complete_lattice -/
#check @Inf_within_of_ord_connected /- _inst_1: conditionally_complete_linear_order ↝ conditionally_complete_lattice -/

-- order/conditionally_complete_lattice.lean
#check @csupr_set /- _inst_1: conditionally_complete_lattice ↝ has_Sup -/

-- order/filter/archimedean.lean
#check @filter.tendsto.at_bot_mul_neg_const' /- _inst_1: linear_ordered_ring ↝ linear_ordered_field -/
#check @filter.tendsto.at_top_nsmul_const /- _inst_1: linear_ordered_cancel_add_comm_monoid ↝ ordered_add_comm_monoid -/
#check @filter.tendsto.at_top_zsmul_const /- _inst_1: linear_ordered_add_comm_group ↝ ordered_add_comm_group -/

-- order/filter/at_top_bot.lean
#check @filter.prod_at_top_at_top_eq /- _inst_1: semilattice_sup ↝ preorder -/
#check @filter.prod_at_top_at_top_eq /- _inst_2: semilattice_sup ↝ preorder -/
#check @filter.tendsto_at_top_of_monotone_of_subseq /- _inst_3: filter.ne_bot ↝ filter.ne_bot -/
#check @filter.tendsto_at_bot_of_monotone_of_subseq /- _inst_3: filter.ne_bot ↝ filter.ne_bot -/

-- order/filter/extr.lean
#check @is_min_filter /- _inst_1: preorder ↝ has_le -/
#check @is_max_filter /- _inst_1: preorder ↝ has_le -/
#check @is_max_on.supr_eq /- _inst_1: conditionally_complete_linear_order ↝ conditionally_complete_lattice -/

-- order/filter/filter_product.lean
#check @filter.germ.const_div /- _inst_1: division_ring ↝ has_div -/

-- order/filter/germ.lean
#check @filter.germ.has_nat_pow /- _inst_1: monoid ↝ has_pow -/
#check @filter.germ.has_int_pow /- _inst_1: div_inv_monoid ↝ has_pow -/

-- order/filter/indicator_function.lean
#check @indicator_union_eventually_eq /- _inst_1: add_monoid ↝ add_zero_class -/

-- order/filter/interval.lean
#check @filter.tendsto_Ico_pure_bot /- _inst_1: partial_order ↝ preorder -/
#check @filter.tendsto_Ioc_pure_bot /- _inst_1: partial_order ↝ preorder -/
#check @filter.tendsto.interval /- _inst_2: filter.tendsto_Ixx_class ↝ filter.tendsto_Ixx_class -/

-- order/filter/ultrafilter.lean
#check @filter.hyperfilter /- _inst_1: infinite ↝ filter.ne_bot -/

-- order/fixed_points.lean
#check @order_hom.le_map_sup_fixed_points /- _inst_1: complete_lattice ↝ semilattice_sup -/
#check @order_hom.le_map_Sup_subset_fixed_points /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @order_hom.map_Inf_subset_fixed_points_le /- _inst_1: complete_lattice ↝ complete_semilattice_Inf -/

-- order/galois_connection.lean
#check @galois_connection /- _inst_1: preorder ↝ has_le -/
#check @galois_connection /- _inst_2: preorder ↝ has_le -/
#check @galois_connection.l_supr /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/

-- order/hom/basic.lean
#check @order_embedding.le_iff_le /- _inst_1: preorder ↝ has_le -/
#check @order_embedding.le_iff_le /- _inst_2: preorder ↝ has_le -/
#check @order_embedding.eq_iff_eq /- _inst_1: preorder ↝ has_le -/
#check @order_embedding.eq_iff_eq /- _inst_2: preorder ↝ has_le -/

-- order/hom/lattice.lean
#check @map_finset_sup /- _inst_5: sup_bot_hom_class ↝ sup_bot_hom_class -/
#check @map_finset_inf /- _inst_5: inf_top_hom_class ↝ inf_top_hom_class -/

-- order/hom/order.lean
#check @order_hom.has_bot /- _inst_3: order_bot ↝ has_bot -/
#check @order_hom.has_top /- _inst_3: order_top ↝ has_top -/

-- order/ideal.lean
#check @order.ideal.mem_compl_of_ge /- _inst_1: preorder ↝ has_le -/
#check @order.ideal.ideal_Inter_nonempty.all_Inter_nonempty /- _inst_1: preorder ↝ has_le -/
#check @order.ideal.ideal_Inter_nonempty.all_bInter_nonempty /- _inst_1: preorder ↝ has_le -/

-- order/imp.lean
#check @lattice.imp_mono /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/
#check @lattice.inf_imp_eq /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/
#check @lattice.imp_self /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/
#check @lattice.compl_imp_compl /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/
#check @lattice.inf_imp_eq_imp_imp /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/
#check @lattice.le_imp_iff /- _inst_1: boolean_algebra ↝ boolean_algebra.core -/

-- order/liminf_limsup.lean
#check @filter.liminf_le_limsup /- _inst_2: filter.ne_bot ↝ filter.ne_bot -/

-- order/locally_finite.lean
#check @finset.Ici /- _inst_2: order_top ↝ has_top -/
#check @finset.Ioi /- _inst_2: order_top ↝ has_top -/
#check @finset.Iic /- _inst_2: order_bot ↝ has_bot -/
#check @finset.Iio /- _inst_2: order_bot ↝ has_bot -/

-- order/monotone.lean
#check @monotone /- _inst_1: preorder ↝ has_le -/
#check @monotone /- _inst_2: preorder ↝ has_le -/
#check @antitone /- _inst_1: preorder ↝ has_le -/
#check @antitone /- _inst_2: preorder ↝ has_le -/
#check @monotone_on /- _inst_1: preorder ↝ has_le -/
#check @monotone_on /- _inst_2: preorder ↝ has_le -/
#check @antitone_on /- _inst_1: preorder ↝ has_le -/
#check @antitone_on /- _inst_2: preorder ↝ has_le -/
#check @strict_mono /- _inst_1: preorder ↝ has_lt -/
#check @strict_mono /- _inst_2: preorder ↝ has_lt -/
#check @strict_anti /- _inst_1: preorder ↝ has_lt -/
#check @strict_anti /- _inst_2: preorder ↝ has_lt -/
#check @strict_mono_on /- _inst_1: preorder ↝ has_lt -/
#check @strict_mono_on /- _inst_2: preorder ↝ has_lt -/
#check @strict_anti_on /- _inst_1: preorder ↝ has_lt -/
#check @strict_anti_on /- _inst_2: preorder ↝ has_lt -/

-- order/monovary.lean
#check @monovary /- _inst_1: preorder ↝ has_le -/
#check @monovary /- _inst_2: preorder ↝ has_lt -/
#check @antivary /- _inst_1: preorder ↝ has_le -/
#check @antivary /- _inst_2: preorder ↝ has_lt -/
#check @monovary_on /- _inst_1: preorder ↝ has_le -/
#check @monovary_on /- _inst_2: preorder ↝ has_lt -/
#check @antivary_on /- _inst_1: preorder ↝ has_le -/
#check @antivary_on /- _inst_2: preorder ↝ has_lt -/

-- order/omega_complete_partial_order.lean
#check @omega_complete_partial_order.continuous_hom.ωSup_bind /- _inst_1: omega_complete_partial_order ↝ preorder -/

-- order/ord_continuous.lean
#check @left_ord_continuous.map_Sup' /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/
#check @left_ord_continuous.map_Sup' /- _inst_2: complete_lattice ↝ complete_semilattice_Sup -/

-- order/pfilter.lean
#check @order.is_pfilter /- _inst_1: preorder ↝ has_le -/

-- order/rel_classes.lean
#check @is_well_order.is_strict_total_order /- _inst_1: is_well_order ↝ is_strict_total_order -/
#check @is_well_order.is_extensional /- _inst_1: is_well_order ↝ is_extensional -/
#check @is_well_order.is_trichotomous /- _inst_1: is_well_order ↝ is_trichotomous -/
#check @is_well_order.is_trans /- _inst_1: is_well_order ↝ is_trans -/
#check @is_well_order.is_irrefl /- _inst_1: is_well_order ↝ is_irrefl -/
#check @is_well_order.is_asymm /- _inst_1: is_well_order ↝ is_asymm -/
#check @is_well_order.linear_order /- _inst_1: is_well_order ↝ is_strict_total_order' -/

-- order/semiconj_Sup.lean
#check @is_order_right_adjoint /- _inst_2: preorder ↝ has_le -/
#check @is_order_right_adjoint_Sup /- _inst_1: complete_lattice ↝ complete_semilattice_Sup -/

-- order/well_founded_set.lean
#check @set.well_founded_on_iff_no_descending_seq /- _inst_1: is_strict_order ↝ is_strict_order -/
#check @set.is_wf_iff_no_descending_seq /- _inst_1: partial_order ↝ preorder -/
#check @set.is_pwo /- _inst_1: preorder ↝ has_le -/
#check @set.is_pwo.exists_monotone_subseq /- _inst_1: partial_order ↝ preorder -/
#check @set.is_pwo_iff_exists_monotone_subseq /- _inst_1: partial_order ↝ preorder -/
#check @set.is_pwo.image_of_monotone /- _inst_1: partial_order ↝ preorder -/
#check @set.is_pwo.image_of_monotone /- _inst_2: partial_order ↝ preorder -/
#check @finset.is_pwo /- _inst_1: partial_order ↝ preorder -/
#check @set.is_wf.min /- _inst_1: partial_order ↝ has_lt -/
#check @set.add_antidiagonal /- _inst_1: add_monoid ↝ has_add -/
#check @set.mul_antidiagonal /- _inst_1: monoid ↝ has_mul -/
#check @set.add_antidiagonal.fst_eq_fst_iff_snd_eq_snd /- _inst_1: add_cancel_comm_monoid ↝ add_cancel_monoid -/
#check @set.mul_antidiagonal.fst_eq_fst_iff_snd_eq_snd /- _inst_1: cancel_comm_monoid ↝ cancel_monoid -/

-- probability/martingale.lean
#check @measure_theory.supermartingale.smul_nonneg /- _inst_6: normed_lattice_add_comm_group ↝ normed_linear_ordered_group -/

-- probability/stopping.lean
#check @measure_theory.prog_measurable.sub /- _inst_5: topological_add_group ↝ has_continuous_sub -/
#check @measure_theory.prog_measurable.div /- _inst_5: topological_group ↝ has_continuous_div -/

-- ring_theory/adjoin/basic.lean
#check @algebra.adjoin_singleton_one /- _inst_2: comm_semiring ↝ semiring -/
#check @algebra.adjoin_int /- _inst_1: comm_ring ↝ ring -/

-- ring_theory/adjoin_root.lean
#check @adjoin_root.algebra /- _inst_3: algebra ↝ algebra -/
#check @adjoin_root.algebra /- _inst_7: is_scalar_tower ↝ is_scalar_tower -/
#check @adjoin_root.algebra /- _inst_6: smul_comm_class ↝ smul_comm_class -/
#check @adjoin_root.aeval_alg_hom_eq_zero /- _inst_2: comm_ring ↝ semiring -/

-- ring_theory/algebra_tower.lean
#check @alg_hom.restrict_domain /- _inst_2: comm_semiring ↝ semiring -/
#check @alg_hom.restrict_domain /- _inst_3: comm_semiring ↝ semiring -/

-- ring_theory/algebraic.lean
#check @is_algebraic /- _inst_2: ring ↝ semiring -/
#check @is_algebraic_of_larger_base_of_injective /- _inst_5: comm_ring ↝ ring -/
#check @is_algebraic_of_larger_base /- _inst_2: field ↝ euclidean_domain -/
#check @algebra.is_algebraic_of_larger_base /- _inst_2: field ↝ euclidean_domain -/

-- ring_theory/algebraic_independent.lean
#check @algebraic_independent /- _inst_2: comm_ring ↝ comm_semiring -/

-- ring_theory/artinian.lean
#check @is_artinian_of_injective /- _inst_1: ring ↝ semiring -/
#check @is_artinian_of_injective /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_injective /- _inst_3: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_surjective /- _inst_1: ring ↝ semiring -/
#check @is_artinian_of_surjective /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_surjective /- _inst_3: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_range_eq_ker /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_fintype /- _inst_1: ring ↝ semiring -/
#check @is_artinian_of_fintype /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_iff_well_founded /- _inst_1: ring ↝ semiring -/
#check @is_artinian_iff_well_founded /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian.induction /- _inst_1: ring ↝ semiring -/
#check @is_artinian.induction /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_artinian_of_tower /- _inst_4: algebra ↝ has_scalar -/
#check @is_artinian_of_fg_of_artinian /- _inst_4: is_artinian_ring ↝ is_artinian -/
#check @is_artinian_ring_of_surjective /- _inst_1: comm_ring ↝ ring -/
#check @is_artinian_ring_of_surjective /- _inst_2: comm_ring ↝ ring -/
#check @is_artinian_ring.is_nilpotent_jacobson_bot /- _inst_2: is_artinian_ring ↝ is_artinian -/

-- ring_theory/chain_of_divisors.lean
#check @divisor_chain.card_subset_divisors_le_length_of_chain /- _inst_1: cancel_comm_monoid_with_zero ↝ comm_monoid -/

-- ring_theory/dedekind_domain/adic_valuation.lean

-- ring_theory/dedekind_domain/basic.lean
#check @ring.dimension_le_one /- _inst_1: comm_ring ↝ semiring -/

-- ring_theory/dedekind_domain/ideal.lean

-- ring_theory/derivation.lean
#check @derivation.coe_smul /- _inst_9: smul_comm_class ↝ has_scalar -/
#check @derivation.coe_smul /- _inst_10: smul_comm_class ↝ has_scalar -/
#check @derivation.coe_smul_linear_map /- _inst_10: smul_comm_class ↝ has_scalar -/
#check @derivation.smul_apply /- _inst_9: smul_comm_class ↝ has_scalar -/
#check @derivation.smul_apply /- _inst_10: smul_comm_class ↝ has_scalar -/
#check @derivation.map_neg /- _inst_1: comm_ring ↝ comm_semiring -/
#check @derivation.map_sub /- _inst_1: comm_ring ↝ comm_semiring -/
#check @derivation.leibniz_of_mul_eq_one /- _inst_1: comm_ring ↝ comm_semiring -/

-- ring_theory/discrete_valuation_ring.lean
#check @discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization /- _inst_1: comm_ring ↝ monoid_with_zero -/
#check @discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.to_unique_factorization_monoid /- _inst_2: is_domain ↝ cancel_comm_monoid_with_zero -/
#check @discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.of_ufd_of_unique_irreducible /- _inst_3: unique_factorization_monoid ↝ wf_dvd_monoid -/
#check @discrete_valuation_ring.unit_mul_pow_congr_pow /- _inst_3: discrete_valuation_ring ↝ unique_factorization_monoid -/

-- ring_theory/discriminant.lean
#check @algebra.discr_eq_discr_of_to_matrix_coeff_is_integral /- _inst_19: number_field ↝ char_zero -/

-- ring_theory/euclidean_domain.lean
#check @gcd_ne_zero_of_left /- _inst_1: euclidean_domain ↝ cancel_comm_monoid_with_zero -/
#check @gcd_ne_zero_of_right /- _inst_1: euclidean_domain ↝ cancel_comm_monoid_with_zero -/

-- ring_theory/finiteness.lean
#check @module.finite.of_restrict_scalars_finite /- _inst_11: algebra ↝ has_scalar -/
#check @algebra.finite_type.self /- _inst_1: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.of_restrict_scalars_finite_type /- _inst_1: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.of_restrict_scalars_finite_type /- _inst_2: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.of_restrict_scalars_finite_type /- _inst_4: comm_ring ↝ semiring -/
#check @algebra.finite_type.of_surjective /- _inst_1: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.of_surjective /- _inst_2: comm_ring ↝ semiring -/
#check @algebra.finite_type.of_surjective /- _inst_4: comm_ring ↝ semiring -/
#check @algebra.finite_type.trans /- _inst_1: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.trans /- _inst_2: comm_ring ↝ comm_semiring -/
#check @algebra.finite_type.trans /- _inst_4: comm_ring ↝ comm_semiring -/
#check @algebra.finite_presentation.equiv /- _inst_2: comm_ring ↝ ring -/
#check @algebra.finite_presentation.equiv /- _inst_4: comm_ring ↝ semiring -/
#check @ring_hom.finite_type /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ring_hom.finite_type /- _inst_2: comm_ring ↝ comm_semiring -/
#check @ring_hom.finite_presentation /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ring_hom.finite_presentation /- _inst_2: comm_ring ↝ comm_semiring -/
#check @alg_hom.finite /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_hom.finite_type /- _inst_1: comm_ring ↝ comm_semiring -/
#check @alg_hom.finite_presentation /- _inst_1: comm_ring ↝ comm_semiring -/
#check @add_monoid_algebra.exists_finset_adjoin_eq_top /- _inst_1: comm_ring ↝ comm_semiring -/
#check @add_monoid_algebra.exists_finset_adjoin_eq_top /- _inst_2: add_comm_monoid ↝ add_monoid -/
#check @add_monoid_algebra.exists_finset_adjoin_eq_top /- _inst_2: add_comm_monoid ↝ add_zero_class -/
#check @monoid_algebra.exists_finset_adjoin_eq_top /- _inst_1: comm_ring ↝ comm_semiring -/
#check @monoid_algebra.exists_finset_adjoin_eq_top /- _inst_2: comm_monoid ↝ monoid -/
#check @monoid_algebra.exists_finset_adjoin_eq_top /- _inst_2: comm_monoid ↝ mul_one_class -/

-- ring_theory/fractional_ideal.lean
#check @fractional_ideal.map_ne_zero /- _inst_5: field ↝ comm_ring -/
#check @fractional_ideal.coe_ideal_injective /- _inst_4: field ↝ comm_ring -/
#check @fractional_ideal.nontrivial /- _inst_5: field ↝ euclidean_domain -/
#check @fractional_ideal.is_noetherian_coe_to_fractional_ideal /- _inst_7: is_noetherian_ring ↝ is_noetherian -/

-- ring_theory/graded_algebra/homogeneous_ideal.lean
#check @ideal.homogeneous_core' /- _inst_3: algebra ↝ module -/

-- ring_theory/hahn_series.lean
#check @hahn_series.emb_domain_one /- _inst_3: non_assoc_semiring ↝ mul_zero_one_class -/
#check @hahn_series.is_pwo_Union_support_powers /- _inst_2: ring ↝ euclidean_domain -/

-- ring_theory/ideal/basic.lean
#check @ideal.maximal_of_no_maximal /- _inst_2: comm_semiring ↝ semiring -/
#check @ideal.span_singleton_eq_span_singleton /- _inst_3: is_domain ↝ cancel_monoid_with_zero -/
#check @ideal.span_singleton_lt_span_singleton /- _inst_3: is_domain ↝ cancel_comm_monoid_with_zero -/
#check @ideal.factors_decreasing /- _inst_3: is_domain ↝ cancel_monoid_with_zero -/
#check @zero_mem_nonunits /- _inst_1: semiring ↝ monoid_with_zero -/

-- ring_theory/ideal/local_ring.lean
#check @is_local_ring_hom_of_comp /- _inst_1: comm_ring ↝ semiring -/
#check @is_local_ring_hom_of_comp /- _inst_2: comm_ring ↝ semiring -/
#check @is_local_ring_hom_of_comp /- _inst_3: comm_ring ↝ semiring -/

-- ring_theory/ideal/operations.lean
#check @submodule.union_eq_smul_set /- _inst_1: comm_semiring ↝ semiring -/
#check @submodule.union_eq_smul_set /- _inst_3: module ↝ has_scalar -/
#check @ideal.mul_eq_bot /- _inst_3: is_domain ↝ no_zero_divisors -/
#check @ideal.radical_bot_of_is_domain /- _inst_3: is_domain ↝ no_zero_divisors -/
#check @ideal.subset_union /- _inst_2: comm_ring ↝ ring -/
#check @ideal.comap_le_comap_iff_of_surjective /- _inst_1: ring ↝ semiring -/
#check @ideal.comap_le_comap_iff_of_surjective /- _inst_2: ring ↝ semiring -/
#check @ideal.map_of_equiv /- _inst_1: ring ↝ semiring -/
#check @ideal.map_of_equiv /- _inst_2: ring ↝ semiring -/
#check @ideal.comap_of_equiv /- _inst_1: ring ↝ semiring -/
#check @ideal.comap_of_equiv /- _inst_2: ring ↝ semiring -/
#check @ideal.map_mul /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ideal.map_mul /- _inst_2: comm_ring ↝ comm_semiring -/
#check @ideal.comap_radical /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ideal.comap_radical /- _inst_2: comm_ring ↝ comm_semiring -/
#check @ideal.map_radical_le /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ideal.map_radical_le /- _inst_2: comm_ring ↝ comm_semiring -/
#check @associates.mk_ne_zero' /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ring_hom.ker_is_prime /- _inst_1: ring ↝ semiring -/
#check @ring_hom.ker_is_maximal_of_surjective /- _inst_2: field ↝ division_ring -/
#check @ideal.map_eq_iff_sup_ker_eq_of_surjective /- _inst_1: comm_ring ↝ ring -/
#check @ideal.map_eq_iff_sup_ker_eq_of_surjective /- _inst_2: comm_ring ↝ ring -/

-- ring_theory/ideal/over.lean
#check @ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem /- _inst_1: comm_ring ↝ semiring -/
#check @ideal.exists_coeff_ne_zero_mem_comap_of_root_mem /- _inst_3: is_domain ↝ no_zero_divisors -/
#check @ideal.mem_of_one_mem /- _inst_2: comm_ring ↝ semiring -/

-- ring_theory/ideal/quotient.lean
#check @ideal.map_pi /- _inst_1: comm_ring ↝ comm_semiring -/

-- ring_theory/integral_closure.lean
#check @ring_hom.is_integral_elem /- _inst_1: comm_ring ↝ semiring -/
#check @ring_hom.is_integral_elem /- _inst_2: ring ↝ semiring -/
#check @is_integral_alg_hom /- _inst_2: comm_ring ↝ ring -/
#check @is_integral_alg_hom /- _inst_3: comm_ring ↝ ring -/
#check @is_integral_of_is_scalar_tower /- _inst_3: comm_ring ↝ ring -/
#check @is_integral.algebra_map /- _inst_3: comm_ring ↝ ring -/
#check @ring_hom.is_integral_zero /- _inst_4: comm_ring ↝ ring -/
#check @ring_hom.is_integral_one /- _inst_4: comm_ring ↝ ring -/
#check @is_integral_smul /- _inst_1: comm_ring ↝ comm_semiring -/
#check @normalize_scale_roots /- _inst_1: comm_ring ↝ ring -/
#check @normalize_scale_roots_eval₂_leading_coeff_mul /- _inst_4: comm_ring ↝ comm_semiring -/
#check @ring_hom.is_integral_of_surjective /- _inst_4: comm_ring ↝ ring -/
#check @ring_hom.is_integral_elem_of_is_integral_elem_comp /- _inst_5: comm_ring ↝ ring -/
#check @is_integral_tower_top_of_is_integral /- _inst_3: comm_ring ↝ ring -/

-- ring_theory/integral_domain.lean
#check @fintype.division_ring_of_is_domain /- _inst_4: ring ↝ division_ring -/
#check @card_nth_roots_subgroup_units /- _inst_3: group ↝ monoid -/

-- ring_theory/integrally_closed.lean
#check @is_integrally_closed_iff /- _inst_3: field ↝ comm_ring -/
#check @is_integrally_closed.is_integral_iff /- iic: is_integrally_closed ↝ is_integral_closure -/
#check @is_integrally_closed.is_integral_iff /- _inst_5: is_fraction_ring ↝ is_integral_closure -/

-- ring_theory/jacobson.lean
#check @ideal.disjoint_powers_iff_not_mem /- _inst_1: comm_ring ↝ comm_semiring -/
#check @ideal.polynomial.jacobson_bot_of_integral_localization /- _inst_7: is_domain ↝ no_zero_divisors -/

-- ring_theory/jacobson_ideal.lean
#check @ideal.jacobson /- _inst_1: comm_ring ↝ semiring -/
#check @ideal.comap_jacobson /- _inst_1: comm_ring ↝ semiring -/

-- ring_theory/laurent_series.lean
#check @laurent_series.power_series_part /- _inst_1: semiring ↝ has_zero -/

-- ring_theory/localization/basic.lean
#check @is_localization.is_unit_comp /- _inst_4: comm_ring ↝ comm_semiring -/
#check @is_localization.eq_of_eq /- _inst_4: comm_ring ↝ comm_semiring -/
#check @is_localization.monoid_hom_ext /- _inst_4: comm_ring ↝ comm_monoid -/
#check @localization.zero /- _inst_1: comm_ring ↝ comm_monoid_with_zero -/

-- ring_theory/localization/fraction_ring.lean
#check @is_fraction_ring.mk'_mk_eq_div /- _inst_6: is_domain ↝ nontrivial -/
#check @is_fraction_ring.is_unit_map_of_injective /- _inst_6: is_domain ↝ nontrivial -/
#check @is_fraction_ring.is_unit_map_of_injective /- _inst_10: field ↝ division_ring -/
#check @is_fraction_ring.mk'_eq_zero_iff_eq_zero /- _inst_9: field ↝ comm_ring -/
#check @is_fraction_ring.lift /- _inst_9: field ↝ comm_ring -/
#check @is_fraction_ring.field_equiv_of_ring_equiv /- _inst_9: field ↝ comm_ring -/
#check @is_fraction_ring.field_equiv_of_ring_equiv /- _inst_10: field ↝ comm_ring -/
#check @fraction_ring /- _inst_1: comm_ring ↝ comm_monoid_with_zero -/
#check @fraction_ring.alg_equiv /- _inst_7: field ↝ comm_ring -/

-- ring_theory/localization/integer.lean
#check @is_localization.is_integer /- _inst_2: comm_ring ↝ ring -/

-- ring_theory/localization/integral.lean
#check @is_localization.integer_normalization_eval₂_eq_zero /- _inst_6: comm_ring ↝ semiring -/

-- ring_theory/localization/inv_submonoid.lean
#check @is_localization.inv_submonoid /- _inst_1: comm_ring ↝ comm_semiring -/
#check @is_localization.inv_submonoid /- _inst_2: comm_ring ↝ semiring -/

-- ring_theory/localization/localization_localization.lean
#check @is_localization.localization_localization_submodule /- _inst_1: comm_ring ↝ comm_semiring -/
#check @is_localization.localization_localization_submodule /- _inst_2: comm_ring ↝ semiring -/

-- ring_theory/localization/num_denom.lean

-- ring_theory/matrix_algebra.lean
#check @matrix_equiv_tensor.inv_fun /- _inst_3: algebra ↝ module -/

-- ring_theory/nilpotent.lean
#check @commute.is_nilpotent_mul_left /- _inst_1: semiring ↝ monoid_with_zero -/

-- ring_theory/noetherian.lean
#check @submodule.fg_ker_comp /- _inst_11: add_comm_group ↝ add_comm_monoid -/
#check @submodule.fg_restrict_scalars /- _inst_6: comm_ring ↝ comm_semiring -/
#check @submodule.fg_restrict_scalars /- _inst_7: comm_ring ↝ semiring
#check @is_noetherian_of_range_eq_ker /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot /- _inst_1: ring ↝ semiring -/
#check @is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_noetherian.disjoint_partial_sups_eventually_bot /- _inst_1: ring ↝ semiring -/
#check @is_noetherian.disjoint_partial_sups_eventually_bot /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_noetherian_ring_iff_ideal_fg /- _inst_1: comm_semiring ↝ semiring -/
#check @is_noetherian_ring_iff_ideal_fg /- _inst_4: is_noetherian_ring ↝ is_noetherian -/
#check @is_noetherian_ring_of_surjective /- _inst_1: comm_ring ↝ ring -/
#check @is_noetherian_ring_of_surjective /- _inst_2: comm_ring ↝ ring -/

-- ring_theory/norm.lean
#check @algebra.norm_eq_prod_embeddings_gen /- _inst_5: field ↝ comm_ring -/

-- ring_theory/nullstellensatz.lean
#check @mv_polynomial.zero_locus /- _inst_1: field ↝ comm_ring -/

-- ring_theory/perfection.lean
#check @ring.perfection /- _inst_1: comm_semiring ↝ has_pow -/
#check @mod_p /- _inst_1: field ↝ comm_ring -/

-- ring_theory/polynomial/basic.lean
#check @polynomial.degree_le /- _inst_1: comm_ring ↝ ring -/
#check @polynomial.degree_lt /- _inst_1: comm_ring ↝ ring -/
#check @polynomial.frange /- _inst_1: comm_ring ↝ semiring -/
#check @polynomial.eval₂_restriction /- _inst_2: ring ↝ semiring -/
#check @polynomial.of_subring /- _inst_1: comm_ring ↝ ring -/
#check @ideal.polynomial_mem_ideal_of_coeff_mem_ideal /- _inst_1: comm_ring ↝ comm_semiring -/
#check @polynomial.ker_map_ring_hom /- _inst_2: comm_ring ↝ semiring -/
#check @mv_polynomial.map_mv_polynomial_eq_eval₂ /- _inst_5: comm_ring ↝ comm_semiring -/

-- ring_theory/polynomial/bernstein.lean
#check @bernstein_polynomial /- _inst_1: comm_ring ↝ ring -/

-- ring_theory/polynomial/content.lean
#check @polynomial.is_primitive /- _inst_1: comm_semiring ↝ semiring -/
#check @polynomial.content /- _inst_2: is_domain ↝ cancel_comm_monoid_with_zero -/

-- ring_theory/polynomial/cyclotomic/basic.lean
#check @polynomial.is_root_cyclotomic_iff_char_zero /- _inst_3: char_zero ↝ ne_zero -/

-- ring_theory/polynomial/cyclotomic/eval.lean
#check @polynomial.eval_one_cyclotomic_not_prime_pow /- _inst_1: comm_ring ↝ ring -/

-- ring_theory/polynomial/eisenstein.lean
#check @polynomial.is_weakly_eisenstein_at.map /- _inst_2: comm_ring ↝ comm_semiring -/
#check @polynomial.monic.leading_coeff_not_mem /- _inst_1: comm_semiring ↝ semiring -/

-- ring_theory/polynomial/gauss_lemma.lean

-- ring_theory/polynomial/rational_root.lean

-- ring_theory/polynomial/scale_roots.lean
#check @scale_roots /- _inst_4: comm_ring ↝ ring -/
#check @scale_roots_eval₂_eq_zero /- _inst_4: comm_ring ↝ comm_semiring -/
#check @scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero /- _inst_2: is_domain ↝ nontrivial -/

-- ring_theory/polynomial/tower.lean
#check @is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field /- _inst_10: comm_semiring ↝ semiring -/

-- ring_theory/power_basis.lean
#check @power_basis.degree_minpoly_gen /- _inst_16: is_domain ↝ nontrivial -/
#check @power_basis.minpoly_gen_monic /- _inst_16: is_domain ↝ nontrivial -/
#check @power_basis.nat_degree_lt_nat_degree /- _inst_1: comm_ring ↝ semiring -/

-- ring_theory/power_series/basic.lean
#check @mv_power_series.map.is_local_ring_hom /- _inst_2: comm_ring ↝ semiring -/
#check @power_series.eq_zero_or_eq_zero_of_mul_eq_zero /- _inst_2: is_domain ↝ no_zero_divisors -/
#check @power_series.is_domain /- _inst_1: ring ↝ euclidean_domain -/
#check @polynomial.coe_to_power_series /- _inst_1: comm_semiring ↝ semiring -/

-- ring_theory/power_series/well_known.lean
#check @power_series.inv_units_sub /- _inst_1: ring ↝ monoid -/
#check @power_series.exp /- _inst_1: ring ↝ semiring -/
#check @power_series.sin /- _inst_1: ring ↝ semiring -/
#check @power_series.cos /- _inst_1: ring ↝ semiring -/

-- ring_theory/principal_ideal_domain.lean
#check @submodule.is_principal.generator_map_dvd_of_mem /- _inst_1: add_comm_group ↝ add_comm_monoid -/
#check @submodule.is_principal.generator_map_dvd_of_mem /- _inst_2: is_domain ↝ cancel_monoid_with_zero
#check @is_field.is_principal_ideal_ring /- _inst_1: comm_ring ↝ ring -/
#check @principal_ideal_ring.irreducible_iff_prime /- _inst_2: is_domain ↝ cancel_comm_monoid_with_zero -/
#check @principal_ideal_ring.ring_hom_mem_submonoid_of_factors_subset_of_units_subset /- _inst_7: semiring ↝ non_assoc_semiring -/
#check @principal_ideal_ring.ring_hom_mem_submonoid_of_factors_subset_of_units_subset /- _inst_2: is_domain ↝ cancel_comm_monoid_with_zero

-- ring_theory/roots_of_unity.lean
#check @roots_of_unity.coe_pow /- _inst_5: comm_ring ↝ comm_monoid -/
#check @is_primitive_root.zpow_eq_one /- _inst_3: comm_group ↝ comm_group_with_zero -/
#check @is_primitive_root.eq_neg_one_of_two_right /- _inst_6: is_domain ↝ no_zero_divisors -/
#check @is_primitive_root.mem_roots_of_unity /- _inst_5: comm_ring ↝ comm_monoid -/
#check @is_primitive_root.pow /- _inst_5: comm_ring ↝ comm_monoid -/

-- ring_theory/simple_module.lean
#check @is_simple_module /- _inst_1: ring ↝ semiring -/
#check @is_simple_module /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @is_semisimple_module /- _inst_1: ring ↝ semiring -/
#check @is_semisimple_module /- _inst_2: add_comm_group ↝ add_comm_monoid -/
#check @linear_map.surjective_or_eq_zero /- _inst_2: add_comm_group ↝ add_comm_monoid -/

-- ring_theory/subring/basic.lean
#check @ring_hom.restrict /- _inst_2: ring ↝ non_assoc_semiring -/
#check @ring_hom.eq_of_eq_on_set_top /- _inst_2: ring ↝ non_assoc_semiring -/
#check @subring.range_fst /- _inst_1: ring ↝ non_assoc_semiring -/
#check @subring.range_fst /- _inst_2: ring ↝ non_assoc_semiring -/
#check @subring.range_snd /- _inst_1: ring ↝ non_assoc_semiring -/
#check @subring.range_snd /- _inst_2: ring ↝ non_assoc_semiring -/

-- ring_theory/unique_factorization_domain.lean
#check @is_noetherian_ring.wf_dvd_monoid /- _inst_3: is_noetherian_ring ↝ is_noetherian -/
#check @unique_factorization_monoid.le_multiplicity_iff_repeat_le_normalized_factors /- _inst_3: nontrivial ↝ nonempty -/
#check @associates.factor_set /- _inst_2: cancel_comm_monoid_with_zero ↝ comm_monoid_with_zero -/
#check @associates.quot_out /- _inst_1: comm_monoid ↝ monoid -/

-- ring_theory/witt_vector/init_tail.lean
#check @witt_vector.select /- _inst_1: comm_ring ↝ has_zero -/

-- ring_theory/witt_vector/teichmuller.lean
#check @witt_vector.teichmuller_fun /- _inst_1: comm_ring ↝ has_zero -/

-- ring_theory/witt_vector/truncated.lean
#check @truncated_witt_vector.out /- _inst_1: comm_ring ↝ has_zero -/
#check @witt_vector.lift_fun /- _inst_2: semiring ↝ non_assoc_semiring -/

-- ring_theory/witt_vector/verschiebung.lean
#check @witt_vector.verschiebung_fun /- _inst_1: comm_ring ↝ has_zero -/

-- ring_theory/witt_vector/witt_polynomial.lean
#check @aeval_witt_polynomial /- _inst_3: comm_ring ↝ comm_semiring -/

-- set_theory/zfc.lean
#check @Set.map_definable_aux /- H: pSet.definable ↝ -/

-- tactic/abel.lean
#check @tactic.abel.term /- _inst_1: add_comm_monoid ↝ add_monoid -/
#check @tactic.abel.termg /- _inst_1: add_comm_group ↝ sub_neg_monoid -/
#check @tactic.abel.smul /- _inst_1: add_comm_monoid ↝ add_monoid -/
#check @tactic.abel.smulg /- _inst_1: add_comm_group ↝ sub_neg_monoid -/
#check @tactic.abel.unfold_sub /- _inst_1: add_group ↝ sub_neg_monoid -/

-- tactic/cancel_denoms.lean
#check @cancel_factors.mul_subst /- _inst_1: comm_ring ↝ comm_semigroup -/
#check @cancel_factors.div_subst /- _inst_1: field ↝ comm_group_with_zero -/
#check @cancel_factors.cancel_factors_eq_div /- _inst_1: field ↝ comm_group_with_zero -/
#check @cancel_factors.add_subst /- _inst_1: ring ↝ non_unital_non_assoc_ring -/

-- tactic/linarith/lemmas.lean
#check @linarith.eq_of_eq_of_eq /- _inst_1: ordered_semiring ↝ add_zero_class -/
#check @linarith.mul_zero_eq /- _inst_1: semiring ↝ mul_zero_class -/
#check @linarith.zero_mul_eq /- _inst_1: semiring ↝ mul_zero_class -/

-- tactic/norm_num.lean
#check @norm_num.zero_succ /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.zero_adc /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.adc_zero /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.add_bit0_bit0 /- _inst_1: semiring ↝ add_comm_semigroup -/
#check @norm_num.bit0_mul /- _inst_1: semiring ↝ distrib -/
#check @norm_num.mul_bit0' /- _inst_1: semiring ↝ distrib -/
#check @norm_num.mul_bit1_bit1 /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.clear_denom_div /- _inst_1: division_ring ↝ group_with_zero -/
#check @norm_num.nat_cast_one /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.nat_cast_bit0 /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.nat_cast_bit1 /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.int_cast_neg /- _inst_1: ring ↝ non_assoc_ring -/
#check @norm_num.nat_cast_ne /- _inst_1: semiring ↝ non_assoc_semiring -/
#check @norm_num.int_cast_ne /- _inst_1: ring ↝ non_assoc_ring -/
#check @norm_num.clear_denom_simple_nat /- _inst_1: division_ring ↝ euclidean_domain -/
#check @norm_num.clear_denom_simple_div /- _inst_1: division_ring ↝ group_with_zero -/
#check @norm_num.clear_denom_mul /- _inst_1: field ↝ cancel_comm_monoid_with_zero -/
#check @norm_num.inv_one /- _inst_1: division_ring ↝ group_with_zero -/
#check @norm_num.inv_one_div /- _inst_1: division_ring ↝ group_with_zero -/
#check @norm_num.inv_div_one /- _inst_1: division_ring ↝ div_inv_monoid -/
#check @norm_num.inv_div /- _inst_1: division_ring ↝ group_with_zero -/
#check @norm_num.div_eq /- _inst_1: division_ring ↝ div_inv_monoid -/
#check @norm_num.sub_pos /- _inst_1: add_group ↝ sub_neg_monoid -/

-- tactic/ring.lean
#check @tactic.ring.pow_succ /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring.subst_into_pow /- _inst_1: monoid ↝ has_pow -/
#check @tactic.ring.unfold_sub /- _inst_1: add_group ↝ sub_neg_monoid -/
#check @tactic.ring.unfold_div /- _inst_1: division_ring ↝ div_inv_monoid -/
#check @tactic.ring.add_neg_eq_sub /- _inst_1: add_group ↝ sub_neg_monoid -/

-- tactic/ring_exp.lean
#check @tactic.ring_exp.exp_congr /- _inst_1: comm_semiring ↝ has_pow -/
#check @tactic.ring_exp.base_to_exp_pf /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.exp_to_prod_pf /- _inst_1: comm_semiring ↝ mul_one_class -/
#check @tactic.ring_exp.prod_to_sum_pf /- _inst_1: comm_semiring ↝ add_zero_class -/
#check @tactic.ring_exp.atom_to_sum_pf /- _inst_1: comm_semiring ↝ semiring -/
#check @tactic.ring_exp.mul_coeff_pf_one_mul /- _inst_1: comm_semiring ↝ mul_one_class -/
#check @tactic.ring_exp.mul_coeff_pf_mul_one /- _inst_1: comm_semiring ↝ mul_one_class -/
#check @tactic.ring_exp.add_overlap_pf /- _inst_1: comm_semiring ↝ distrib -/
#check @tactic.ring_exp.add_overlap_pf_zero /- _inst_1: comm_semiring ↝ non_unital_non_assoc_semiring -/
#check @tactic.ring_exp.add_pf_z_sum /- _inst_1: comm_semiring ↝ add_zero_class -/
#check @tactic.ring_exp.add_pf_sum_z /- _inst_1: comm_semiring ↝ add_zero_class -/
#check @tactic.ring_exp.mul_p_pf_zero /- _inst_1: comm_semiring ↝ mul_zero_class -/
#check @tactic.ring_exp.mul_p_pf_sum /- _inst_1: comm_semiring ↝ distrib -/
#check @tactic.ring_exp.mul_pf_zero /- _inst_1: comm_semiring ↝ mul_zero_class -/
#check @tactic.ring_exp.mul_pf_sum /- _inst_1: comm_semiring ↝ distrib -/
#check @tactic.ring_exp.pow_e_pf_exp /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.pow_pp_pf_one /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.pow_pf_c_c /- _inst_1: comm_semiring ↝ has_pow -/
#check @tactic.ring_exp.pow_pp_pf_prod /- _inst_1: comm_semiring ↝ comm_monoid -/
#check @tactic.ring_exp.pow_p_pf_one /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.pow_p_pf_zero /- _inst_1: comm_semiring ↝ monoid_with_zero -/
#check @tactic.ring_exp.pow_p_pf_succ /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.pow_p_pf_cons /- _inst_1: comm_semiring ↝ has_pow -/
#check @tactic.ring_exp.pow_pf_zero /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.pow_pf_sum /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.simple_pf_sum_zero /- _inst_1: comm_semiring ↝ add_zero_class -/
#check @tactic.ring_exp.simple_pf_prod_one /- _inst_1: comm_semiring ↝ mul_one_class -/
#check @tactic.ring_exp.simple_pf_var_one /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.simple_pf_exp_one /- _inst_1: comm_semiring ↝ monoid -/
#check @tactic.ring_exp.inverse_pf /- _inst_2: division_ring ↝ has_inv -/
#check @tactic.ring_exp.sub_pf /- _inst_2: ring ↝ sub_neg_monoid -/
#check @tactic.ring_exp.div_pf /- _inst_2: division_ring ↝ div_inv_monoid -/

-- topology/alexandroff.lean
#check @alexandroff.nhds_within_compl_infty_ne_bot /- _inst_2: noncompact_space ↝ filter.ne_bot -/

-- topology/algebra/algebra.lean
#check @continuous_algebra_map_iff_smul /- _inst_6: topological_semiring ↝ has_continuous_mul -/
#check @subalgebra.topological_closure_comap'_homeomorph /- _inst_8: topological_ring ↝ topological_semiring -/

-- topology/algebra/const_mul_action.lean
#check @units.has_continuous_const_smul /- _inst_3: mul_action ↝ has_scalar -/
#check @add_units.has_continuous_const_vadd /- _inst_3: add_action ↝ has_vadd -/
#check @vadd_closure_subset /- _inst_3: add_action ↝ has_vadd -/
#check @smul_closure_subset /- _inst_3: mul_action ↝ has_scalar -/
#check @fintype.properly_discontinuous_smul /- _inst_1: group ↝ monoid -/
#check @fintype.properly_discontinuous_smul /- _inst_3: mul_action ↝ has_scalar -/
#check @fintype.properly_discontinuous_vadd /- _inst_1: add_group ↝ add_monoid -/
#check @fintype.properly_discontinuous_vadd /- _inst_3: add_action ↝ has_vadd -/

-- topology/algebra/continuous_affine_map.lean
#check @continuous_affine_map.coe_smul /- _inst_17: smul_comm_class ↝ has_scalar -/
#check @continuous_affine_map.coe_smul /- _inst_18: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_affine_map.smul_apply /- _inst_17: smul_comm_class ↝ has_scalar -/
#check @continuous_affine_map.smul_apply /- _inst_18: has_continuous_const_smul ↝ has_scalar -/

-- topology/algebra/field.lean
#check @topological_ring.topological_space_units /- _inst_1: semiring ↝ monoid -/
#check @topological_ring.top_monoid_units /- _inst_4: topological_semiring ↝ has_continuous_mul -/
#check @topological_division_ring.induced_units /- _inst_1: division_ring ↝ semiring -/

-- topology/algebra/floor_ring.lean
#check @continuous_on_fract /- _inst_4: topological_add_group ↝ has_continuous_sub -/
#check @tendsto_fract_left' /- _inst_5: topological_add_group ↝ has_continuous_sub -/
#check @tendsto_fract_right' /- _inst_5: topological_add_group ↝ has_continuous_sub -/
#check @continuous_on.comp_fract' /- _inst_4: order_topology ↝ order_closed_topology -/

-- topology/algebra/group.lean
#check @mul_opposite.has_continuous_inv /- _inst_5: group ↝ has_inv -/
#check @add_opposite.has_continuous_neg /- _inst_5: add_group ↝ has_neg -/
#check @is_open.neg /- _inst_3: topological_add_group ↝ has_continuous_neg -/
#check @is_open.inv /- _inst_3: topological_group ↝ has_continuous_inv -/
#check @is_closed.inv /- _inst_3: topological_group ↝ has_continuous_inv -/
#check @is_closed.neg /- _inst_3: topological_add_group ↝ has_continuous_neg -/
#check @neg_mem_connected_component_zero /- _inst_7: topological_add_group ↝ has_continuous_neg -/
#check @inv_mem_connected_component_one /- _inst_7: topological_group ↝ has_continuous_inv -/
#check @nhds_translation_mul_inv /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @nhds_translation_add_neg /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @map_mul_left_nhds /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @map_add_left_nhds /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @quotient_add_group.is_open_map_coe /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @quotient_group.is_open_map_coe /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @topological_group.t1_space /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @topological_add_group.t1_space /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @topological_group.regular_space /- _inst_4: t1_space ↝ t0_space -/
#check @topological_add_group.regular_space /- _inst_4: t1_space ↝ t0_space -/
#check @compact_open_separated_mul_right /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @compact_open_separated_add_right /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @compact_covered_by_mul_left_translates /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @compact_covered_by_add_left_translates /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @separable_locally_compact_group.sigma_compact_space /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @separable_locally_compact_add_group.sigma_compact_space /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @topological_space.positive_compacts.locally_compact_space_of_group /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @topological_space.positive_compacts.locally_compact_space_of_add_group /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @quotient_add_group.has_continuous_const_vadd /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @quotient_group.has_continuous_const_smul /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @quotient_group.continuous_smul₁ /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @quotient_add_group.continuous_smul₁ /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @quotient_group.has_continuous_smul /- _inst_3: topological_group ↝ has_continuous_mul -/
#check @quotient_add_group.has_continuous_vadd /- _inst_3: topological_add_group ↝ has_continuous_add -/

-- topology/algebra/group_with_zero.lean
#check @filter.tendsto.div_const /- _inst_1: group_with_zero ↝ div_inv_monoid -/
#check @continuous_at.div_const /- _inst_1: group_with_zero ↝ div_inv_monoid -/
#check @continuous_on.div_const /- _inst_1: group_with_zero ↝ div_inv_monoid -/
#check @continuous.div_const /- _inst_1: group_with_zero ↝ div_inv_monoid -/

-- topology/algebra/infinite_sum.lean
#check @has_sum.neg /- _inst_3: topological_add_group ↝ has_continuous_neg -/
#check @summable.trans_sub /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @has_sum.update /- _inst_3: topological_add_group ↝ has_continuous_add -/
#check @has_sum.mul_left /- _inst_3: topological_semiring ↝ has_continuous_mul -/
#check @has_sum.mul_right /- _inst_3: topological_semiring ↝ has_continuous_mul -/
#check @has_sum.div_const /- _inst_3: topological_ring ↝ topological_semiring -/
#check @has_sum_mul_left_iff /- _inst_3: topological_ring ↝ topological_semiring -/
#check @has_sum_mul_right_iff /- _inst_3: topological_ring ↝ topological_semiring -/
#check @summable_mul_left_iff /- _inst_3: topological_ring ↝ topological_semiring -/
#check @summable_mul_right_iff /- _inst_3: topological_ring ↝ topological_semiring -/
#check @summable_iff_cauchy_seq_finset /- _inst_1: add_comm_group ↝ add_comm_monoid -/
#check @has_sum_of_is_lub_of_nonneg /- _inst_3: order_topology ↝ Sup_convergence_class -/
#check @has_sum_of_is_lub /- _inst_3: order_topology ↝ Sup_convergence_class -/
#check @summable_sum_mul_antidiagonal_of_summable_mul /- _inst_4: topological_semiring ↝ has_continuous_add -/

-- topology/algebra/module/basic.lean
#check @has_continuous_smul.of_nhds_zero /- _inst_6: topological_ring ↝ has_continuous_sub
#check @is_closed_set_of_map_smul /- _inst_7: module ↝ has_scalar -/
#check @is_closed_set_of_map_smul /- _inst_8: module ↝ has_scalar -/
#check @continuous_linear_map.smul_apply /- _inst_21: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.smul_apply /- _inst_22: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.smul_apply /- _inst_22: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.coe_smul' /- _inst_21: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.coe_smul' /- _inst_22: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.is_scalar_tower /- _inst_21: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.is_scalar_tower /- _inst_22: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.is_scalar_tower /- _inst_24: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.is_scalar_tower /- _inst_25: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.smul_comm_class /- _inst_21: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.smul_comm_class /- _inst_22: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.smul_comm_class /- _inst_24: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.smul_comm_class /- _inst_25: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.smul_right_comp /- _inst_22: has_continuous_mul ↝ has_continuous_smul -/
#check @continuous_linear_map.map_neg /- _inst_1: ring ↝ semiring -/
#check @continuous_linear_map.map_neg /- _inst_2: ring ↝ semiring -/
#check @continuous_linear_map.map_sub /- _inst_1: ring ↝ semiring -/
#check @continuous_linear_map.map_sub /- _inst_2: ring ↝ semiring -/
#check @continuous_linear_map.sub_apply' /- _inst_1: ring ↝ semiring -/
#check @continuous_linear_map.sub_apply' /- _inst_2: ring ↝ semiring -/
#check @continuous_linear_map.sub_apply' /- _inst_4: add_comm_group ↝ add_comm_monoid -/
#check @continuous_linear_map.smul_comp /- _inst_22: smul_comm_class ↝ mul_action -/
#check @continuous_linear_map.smul_comp /- _inst_23: has_continuous_const_smul ↝ mul_action -/
#check @continuous_linear_map.restrict_scalars /- _inst_8: ring ↝ semiring -/
#check @continuous_linear_map.restrict_scalars_add /- _inst_12: topological_add_group ↝ has_continuous_add -/
#check @continuous_linear_map.to_ring_inverse /- _inst_7: add_comm_group ↝ add_comm_monoid -/

-- topology/algebra/module/multilinear.lean
#check @continuous_multilinear_map.smul_apply /- _inst_27: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_multilinear_map.smul_apply /- _inst_28: smul_comm_class ↝ has_scalar -/
#check @continuous_multilinear_map.smul_apply /- _inst_27: has_continuous_const_smul ↝ has_scalar
#check @continuous_multilinear_map.smul_comm_class /- _inst_27: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_multilinear_map.smul_comm_class /- _inst_28: smul_comm_class ↝ has_scalar -/
#check @continuous_multilinear_map.smul_comm_class /- _inst_30: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_multilinear_map.smul_comm_class /- _inst_31: smul_comm_class ↝ has_scalar -/
#check @continuous_multilinear_map.is_scalar_tower /- _inst_27: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_multilinear_map.is_scalar_tower /- _inst_28: smul_comm_class ↝ has_scalar -/
#check @continuous_multilinear_map.is_scalar_tower /- _inst_30: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_multilinear_map.is_scalar_tower /- _inst_31: smul_comm_class ↝ has_scalar -/
#check @continuous_multilinear_map.map_sub /- _inst_2: ring ↝ semiring -/

-- topology/algebra/module/weak_dual.lean
#check @module_weak_bilin /- _inst_2: comm_semiring ↝ semiring -/
#check @module_weak_bilin /- _inst_3: add_comm_group ↝ add_comm_monoid
#check @weak_dual_module /- _inst_10: smul_comm_class ↝ module -/
#check @weak_dual_module /- _inst_11: has_continuous_const_smul ↝ module -/

-- topology/algebra/monoid.lean
#check @add_submonoid.has_continuous_add /- _inst_3: add_monoid ↝ add_zero_class -/
#check @submonoid.has_continuous_mul /- _inst_3: monoid ↝ mul_one_class -/
#check @exists_open_nhds_zero_half /- _inst_3: add_monoid ↝ add_zero_class -/
#check @exists_open_nhds_one_split /- _inst_3: monoid ↝ mul_one_class -/
#check @is_compact.mul /- _inst_3: monoid ↝ has_mul -/
#check @is_compact.add /- _inst_3: add_monoid ↝ has_add -/
#check @submonoid.mem_nhds_one /- _inst_3: comm_monoid ↝ mul_one_class -/
#check @add_submonoid.mem_nhds_zero /- _inst_3: add_comm_monoid ↝ add_zero_class -/
#check @locally_finite.exists_finset_support /- _inst_5: add_comm_monoid ↝ has_zero -/
#check @locally_finite.exists_finset_mul_support /- _inst_5: comm_monoid ↝ has_one -/

-- topology/algebra/mul_action.lean
#check @add_units.has_continuous_vadd /- _inst_5: add_action ↝ has_vadd -/
#check @units.has_continuous_smul /- _inst_5: mul_action ↝ has_scalar -/

-- topology/algebra/nonarchimedean/adic_topology.lean
#check @is_adic_iff /- _inst_2: topological_ring ↝ topological_add_group -/

-- topology/algebra/nonarchimedean/basic.lean
#check @nonarchimedean_ring.left_mul_subset /- _inst_3: nonarchimedean_ring ↝ has_continuous_mul -/

-- topology/algebra/open_subgroup.lean
#check @submodule.is_open_mono /- _inst_1: comm_ring ↝ ring -/
#check @submodule.is_open_mono /- _inst_4: topological_add_group ↝ has_continuous_add -/
#check @ideal.is_open_of_open_subideal /- _inst_3: topological_ring ↝ topological_add_group -/

-- topology/algebra/order/basic.lean
#check @preorder.topology /- _inst_1: preorder ↝ has_lt -/
#check @order_dual.order_topology /- _inst_2: partial_order ↝ preorder -/
#check @is_open_iff_generate_intervals /- _inst_2: partial_order ↝ preorder -/
#check @nhds_eq_order /- _inst_2: partial_order ↝ preorder -/
#check @induced_order_topology' /- _inst_1: partial_order ↝ preorder -/
#check @order_topology.t2_space /- _inst_3: order_topology ↝ t2_space -/
#check @disjoint_nhds_at_top /- _inst_3: order_topology ↝ order_closed_topology -/
#check @tendsto_inv_zero_at_top /- _inst_3: order_topology ↝ order_closed_topology -/
#check @preimage_neg /- _inst_1: add_group ↝ has_involutive_neg -/
#check @filter.map_neg /- _inst_1: add_group ↝ has_involutive_neg -/
#check @map_Sup_of_continuous_at_of_monotone' /- _inst_6: order_topology ↝ order_closed_topology -/
#check @map_cSup_of_continuous_at_of_monotone /- _inst_6: order_topology ↝ order_closed_topology -/

-- topology/algebra/order/compact.lean
#check @is_compact.is_glb_Inf /- _inst_3: order_topology ↝ order_closed_topology -/

-- topology/algebra/order/intermediate_value.lean
#check @is_connected.Ioo_cInf_cSup_subset /- _inst_3: order_topology ↝ order_closed_topology -/
#check @is_preconnected.Ioi_cInf_subset /- _inst_3: order_topology ↝ order_closed_topology -/
#check @is_preconnected.Ioi_cInf_subset /- _inst_3: order_topology ↝ preconnected_space -/
#check @is_preconnected.Ioi_cInf_subset /- _inst_8: densely_ordered ↝ preconnected_space -/

-- topology/algebra/order/liminf_limsup.lean
#check @filter.tendsto.is_cobounded_under_ge /- _inst_4: filter.ne_bot ↝ filter.ne_bot -/
#check @filter.tendsto.is_cobounded_under_le /- _inst_4: filter.ne_bot ↝ filter.ne_bot -/
#check @filter.tendsto.limsup_eq /- _inst_4: filter.ne_bot ↝ filter.ne_bot -/
#check @filter.tendsto.liminf_eq /- _inst_4: filter.ne_bot ↝ filter.ne_bot -/

-- topology/algebra/order/monotone_continuity.lean
#check @strict_mono_on.continuous_at_right_of_exists_between /- _inst_3: order_topology ↝ order_closed_topology -/
#check @strict_mono_on.continuous_at_right_of_exists_between /- _inst_4: linear_order ↝ partial_order -/
#check @continuous_at_right_of_monotone_on_of_exists_between /- _inst_3: order_topology ↝ order_closed_topology -/
#check @continuous_at_right_of_monotone_on_of_exists_between /- _inst_4: linear_order ↝ partial_order -/
#check @order_iso.continuous /- _inst_2: partial_order ↝ preorder -/

-- topology/algebra/order/monotone_convergence.lean
#check @tendsto_of_monotone /- _inst_4: order_topology ↝ Sup_convergence_class -/
#check @tendsto_iff_tendsto_subseq_of_monotone /- _inst_3: nonempty ↝ filter.ne_bot -/
#check @is_lub_of_tendsto_at_top /- _inst_4: nonempty ↝ filter.ne_bot -/
#check @is_lub_of_tendsto_at_top /- _inst_4: nonempty ↝ filter.ne_bot -/
#check @is_lub_of_tendsto_at_top /- _inst_4: nonempty ↝ filter.ne_bot

-- topology/algebra/order/proj_Icc.lean
#check @continuous_proj_Icc /- _inst_4: order_topology ↝ order_closed_topology -/

-- topology/algebra/ring.lean
#check @mul_opposite.has_continuous_add /- _inst_1: non_unital_non_assoc_semiring ↝ has_add -/
#check @mul_opposite.has_continuous_neg /- _inst_1: non_unital_non_assoc_ring ↝ has_neg -/
#check @add_opposite.has_continuous_mul /- _inst_1: non_unital_non_assoc_semiring ↝ has_mul -/
#check @mul_left_continuous /- _inst_3: topological_ring ↝ has_continuous_mul -/
#check @mul_right_continuous /- _inst_3: topological_ring ↝ has_continuous_mul -/
#check @subring.topological_ring /- _inst_3: topological_ring ↝ topological_semiring -/
#check @quotient_ring.is_open_map_coe /- _inst_3: topological_ring ↝ has_continuous_add -/

-- topology/algebra/uniform_field.lean
#check @uniform_space.completion.nontrivial /- _inst_1: field ↝ euclidean_domain -/
#check @hat_inv /- _inst_1: field ↝ has_inv -/
#check @hat_inv_extends /- _inst_3: topological_division_ring ↝ has_continuous_inv₀ -/
#check @coe_inv /- _inst_4: completable_top_field ↝ separated_space -/

-- topology/algebra/uniform_group.lean
#check @tendsto_sub_comap_self /- _inst_3: topological_add_group ↝ has_continuous_sub -/
#check @tendsto_sub_comap_self /- _inst_5: add_comm_group ↝ add_group -/
#check @tendsto_div_comap_self /- _inst_3: topological_group ↝ has_continuous_div -/
#check @tendsto_div_comap_self /- _inst_5: comm_group ↝ group -/

-- topology/algebra/uniform_ring.lean
#check @uniform_space.completion.has_one /- _inst_1: ring ↝ has_one -/
#check @uniform_space.completion.has_mul /- _inst_1: ring ↝ has_mul -/
#check @uniform_space.completion.coe_mul /- _inst_3: topological_ring ↝ has_continuous_mul -/

-- topology/continuous_function/algebra.lean
#check @continuous_map.coe_vadd /- _inst_6: has_continuous_const_vadd ↝ has_vadd -/
#check @continuous_map.coe_smul /- _inst_6: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.smul_apply /- _inst_6: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.vadd_apply /- _inst_6: has_continuous_const_vadd ↝ has_vadd -/
#check @continuous_map.vadd_comp /- _inst_6: has_continuous_const_vadd ↝ has_vadd -/
#check @continuous_map.smul_comp /- _inst_6: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.smul_comm_class /- _inst_6: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.smul_comm_class /- _inst_8: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.vadd_comm_class /- _inst_6: has_continuous_const_vadd ↝ has_vadd -/
#check @continuous_map.vadd_comm_class /- _inst_8: has_continuous_const_vadd ↝ has_vadd -/
#check @continuous_map.is_scalar_tower /- _inst_6: has_continuous_const_smul ↝ has_scalar -/
#check @continuous_map.is_scalar_tower /- _inst_8: has_continuous_const_smul ↝ has_scalar -/
#check @subalgebra.separates_points /- _inst_11: has_continuous_const_smul ↝ algebra -/
#check @algebra_map_apply /- _inst_11: has_continuous_const_smul ↝ algebra -/
#check @continuous_map.inf_eq /- _inst_5: topological_ring ↝ has_continuous_add -/

-- topology/continuous_function/bounded.lean
#check @bounded_continuous_function.equicontinuous_of_continuity_modulus /- _inst_4: metric_space ↝ pseudo_metric_space -/
#check @bounded_continuous_function.dist_le_two_norm' /- _inst_2: normed_group ↝ semi_normed_group -/
#check @bounded_continuous_function.coe_smul /- _inst_7: has_bounded_smul ↝ has_scalar -/
#check @bounded_continuous_function.smul_apply /- _inst_7: has_bounded_smul ↝ has_scalar -/
#check @bounded_continuous_function.star_module /- _inst_2: star_ring ↝ has_star

-- topology/continuous_function/compact.lean
#check @continuous_map.uniform_continuity /- _inst_3: metric_space ↝ pseudo_metric_space -/

-- topology/continuous_function/units.lean
#check @continuous_map.is_unit_iff_forall_ne_zero /- _inst_2: normed_field ↝ normed_division_ring -/

-- topology/instances/ennreal.lean
#check @edist_ne_top_of_mem_ball /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @nhds_eq_nhds_emetric_ball /- _inst_1: emetric_space ↝ pseudo_emetric_space -/

-- topology/metric_space/antilipschitz.lean
#check @antilipschitz_with /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @antilipschitz_with /- _inst_2: pseudo_emetric_space ↝ has_edist -/

-- topology/metric_space/basic.lean
#check @metric.ball /- _inst_1: pseudo_metric_space ↝ has_dist -/
#check @metric.closed_ball /- _inst_1: pseudo_metric_space ↝ has_dist -/
#check @metric.sphere /- _inst_1: pseudo_metric_space ↝ has_dist -/
#check @metric.complete_of_cauchy_seq_tendsto /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space -/
#check @totally_bounded_Icc /- _inst_1: pseudo_metric_space ↝ uniform_space -/
#check @metric.bounded /- _inst_1: pseudo_metric_space ↝ has_dist -/
#check @metric.diam /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space -/
#check @metric.uniform_embedding_iff' /- _inst_3: metric_space ↝ pseudo_metric_space -/

-- topology/metric_space/cau_seq_filter.lean
#check @cau_seq.tendsto_limit /- _inst_1: normed_ring ↝ semi_normed_ring -/
#check @normed_field.is_absolute_value /- _inst_1: normed_field ↝ normed_division_ring -/
#check @cauchy_seq.is_cau_seq /- _inst_1: normed_field ↝ semi_normed_ring -/

-- topology/metric_space/closeds.lean
#check @emetric.nonempty_compacts.second_countable_topology /- _inst_2: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- topology/metric_space/contracting.lean
#check @contracting_with /- _inst_1: emetric_space ↝ pseudo_emetric_space -/
#check @contracting_with.one_sub_K_pos /- _inst_1: metric_space ↝ emetric_space -/

-- topology/metric_space/emetric_space.lean
#check @uniformity_dist_of_mem_uniformity /- _inst_1: linear_order ↝ has_lt -/
#check @emetric.ball /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @emetric.closed_ball /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @emetric.diam /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @emetric_space.to_uniform_space' /- _inst_2: emetric_space ↝ pseudo_emetric_space -/
#check @uniform_embedding_iff' /- _inst_3: emetric_space ↝ pseudo_emetric_space -/
#check @uniformity_edist /- _inst_2: emetric_space ↝ pseudo_emetric_space -/

-- topology/metric_space/hausdorff_dimension.lean
#check @cont_diff_on.dimH_image_le /- _inst_5: finite_dimensional ↝ topological_space.second_countable_topology -/

-- topology/metric_space/hausdorff_distance.lean
#check @emetric.inf_edist /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @metric.inf_dist /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space -/
#check @metric.inf_nndist /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space -/
#check @metric.Hausdorff_dist /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space -/

-- topology/metric_space/holder.lean
#check @holder_with /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @holder_with /- _inst_2: pseudo_emetric_space ↝ has_edist -/
#check @holder_on_with /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @holder_on_with /- _inst_2: pseudo_emetric_space ↝ has_edist -/

-- topology/metric_space/isometry.lean
#check @isometry /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @isometry /- _inst_2: pseudo_emetric_space ↝ has_edist -/

-- topology/metric_space/lipschitz.lean
#check @lipschitz_with /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @lipschitz_with /- _inst_2: pseudo_emetric_space ↝ has_edist -/
#check @lipschitz_on_with /- _inst_1: pseudo_emetric_space ↝ has_edist -/
#check @lipschitz_on_with /- _inst_2: pseudo_emetric_space ↝ has_edist -/

-- topology/metric_space/metric_separated.lean
#check @is_metric_separated /- _inst_1: emetric_space ↝ has_edist -/

-- topology/metric_space/pi_nat.lean
#check @exists_nat_nat_continuous_surjective_of_complete_space /- _inst_3: topological_space.second_countable_topology ↝ topological_space.separable_space -/

-- topology/metric_space/polish.lean
#check @polish_space.has_dist_complete_copy /- _inst_1: metric_space ↝ pseudo_metric_space -/

-- topology/semicontinuous.lean
#check @lower_semicontinuous_within_at /- _inst_2: preorder ↝ has_lt -/
#check @lower_semicontinuous_at /- _inst_2: preorder ↝ has_lt -/
#check @upper_semicontinuous_within_at /- _inst_2: preorder ↝ has_lt -/
#check @upper_semicontinuous_at /- _inst_2: preorder ↝ has_lt -/
#check @continuous_within_at.lower_semicontinuous_within_at /- _inst_5: order_topology ↝ order_closed_topology -/
#check @continuous_at.lower_semicontinuous_at /- _inst_5: order_topology ↝ order_closed_topology -/
#check @continuous_at.comp_lower_semicontinuous_within_at /- _inst_8: order_topology ↝ order_closed_topology -/
#check @continuous_within_at.upper_semicontinuous_within_at /- _inst_5: order_topology ↝ order_closed_topology -/
#check @continuous_at.upper_semicontinuous_at /- _inst_5: order_topology ↝ order_closed_topology -/

-- topology/separation.lean
#check @tendsto_nhds_unique /- _inst_3: filter.ne_bot ↝ filter.ne_bot -/
#check @filter.tendsto.lim_eq /- _inst_3: filter.ne_bot ↝ filter.ne_bot -/

-- topology/sequences.lean
#check @compact_space.tendsto_subseq /- _inst_2: topological_space.first_countable_topology ↝ seq_compact_space -/
#check @compact_space.tendsto_subseq /- _inst_3: compact_space ↝ seq_compact_space -/
#check @seq_compact.lebesgue_number_lemma_of_metric /- _inst_1: metric_space ↝ pseudo_metric_space -/

-- topology/subset_properties.lean
#check @filter.coclosed_compact.filter.ne_bot /- _inst_3: noncompact_space ↝ filter.ne_bot -/
#check @closed_embedding.noncompact_space /- _inst_3: noncompact_space ↝ filter.ne_bot -/

-- topology/support.lean
#check @has_compact_mul_support.mul /- _inst_2: monoid ↝ mul_one_class -/
#check @has_compact_support.add /- _inst_2: add_monoid ↝ add_zero_class -/
#check @has_compact_support.smul_left /- _inst_2: monoid_with_zero ↝ monoid -/

-- topology/uniform_space/abstract_completion.lean
#check @abstract_completion.extend_unique /- _inst_4: separated_space ↝ t2_space -/
#check @abstract_completion.extend_comp_coe /- _inst_4: separated_space ↝ t2_space -/
#check @abstract_completion.extend_map /- _inst_5: separated_space ↝ t2_space -/
#check @abstract_completion.extension₂_coe_coe /- _inst_4: separated_space ↝ t2_space -/

-- topology/uniform_space/basic.lean
#check @uniform_space.is_open_ball /- _inst_1: uniform_space ↝ topological_space -/

-- topology/uniform_space/cauchy.lean
#check @filter.tendsto.cauchy_map /- _inst_2: filter.ne_bot ↝ filter.ne_bot -/
#check @cauchy_seq /- _inst_2: semilattice_sup ↝ preorder -/
#check @filter.tendsto.cauchy_seq /- _inst_3: nonempty ↝ filter.ne_bot -/
#check @cauchy_seq_iff_tendsto /- _inst_2: nonempty ↝ filter.ne_bot -/
#check @cauchy_map_iff_exists_tendsto /- _inst_3: filter.ne_bot ↝ filter.ne_bot -/

-- topology/uniform_space/compact_convergence.lean
#check @continuous_map.compact_conv_nhd /- _inst_2: uniform_space ↝ topological_space -/

-- topology/uniform_space/complete_separated.lean
#check @is_complete.is_closed /- _inst_2: separated_space ↝ t2_space -/
#check @dense_inducing.continuous_extend_of_cauchy /- _inst_5: separated_space ↝ regular_space -/

-- topology/uniform_space/completion.lean
#check @Cauchy.Cauchy_eq /- _inst_1: inhabited ↝ nonempty -/
#check @uniform_space.completion.extension_coe /- _inst_4: separated_space ↝ t2_space -/

-- topology/uniform_space/uniform_embedding.lean
#check @uniformly_extend_of_ind /- _inst_4: separated_space ↝ t2_space -/
#check @uniformly_extend_unique /- _inst_4: separated_space ↝ t2_space -/