/- Checking 100334 declarations (plus 96066 automatically generated ones) in mathlib with 1 linters -/ /- The `explicit_vars_of_eq_iff` linter reports: -/ /- EXPLICIT VARIABLES ON BOTH SIDES OF EQUALITY OR IFF -/ -- algebra/add_torsor.lean #check @eq_vadd_iff_vsub_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p2, g, p1 -/ #check @set.mem_vsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ -- algebra/algebra/basic.lean #check @alg_hom.injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebra/algebra/bilinear.lean #check @algebra.lmul_left_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @algebra.lmul_right_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/algebra/subalgebra.lean #check @subalgebra.mem_to_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @subalgebra.coe_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @subalgebra.coe_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @subalgebra.mem_comap /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, S -/ #check @alg_hom.mem_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ -/ #check @alg_hom.injective_cod_restrict /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @alg_hom.mem_equalizer /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, ψ, ϕ -/ -- algebra/associated.lean #check @associated_zero_iff_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @associates.is_unit_iff_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @associates.prime_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @associates.irreducible_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/big_operators/associated.lean #check @prime.dvd_finset_prod_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ -- algebra/category/Module/abelian.lean #check @Module.exact_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- algebra/category/Module/epi_mono.lean #check @Module.mono_iff_ker_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Module.mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Module.epi_iff_range_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Module.epi_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebra/char_p/algebra.lean #check @algebra.char_p_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- algebra/char_p/basic.lean #check @char_p.int_cast_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @char_p.int_coe_eq_int_coe_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @ring_char.spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, R -/ #check @eq_iff_modeq_int /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @ring_hom.char_p_iff_char_p /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- algebra/char_p/exp_char.lean #check @char_eq_exp_char_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- algebra/continued_fractions/computation/terminates_iff_rat.lean #check @generalized_continued_fraction.terminates_iff_rat /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ -- algebra/covariant_and_contravariant.lean #check @rel_iff_cov /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @covariant_le_iff_contravariant_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, N, M -/ #check @covariant_lt_iff_contravariant_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, N, M -/ #check @covariant_flip_add_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, N -/ #check @covariant_flip_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, N -/ #check @contravariant_flip_add_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, N -/ #check @contravariant_flip_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, N -/ -- algebra/direct_sum/basic.lean #check @direct_sum.add_subgroup_is_internal.to_add_submonoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- algebra/direct_sum/module.lean #check @direct_sum.submodule_is_internal.to_add_submonoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @direct_sum.submodule_is_internal.to_add_subgroup /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- algebra/divisibility.lean #check @is_unit.dvd_mul_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_unit.mul_left_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/free_algebra.lean #check @free_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @free_algebra.algebra_map_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @free_algebra.algebra_map_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @free_algebra.algebra_map_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @free_algebra.ι_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/free_non_unital_non_assoc_algebra.lean #check @free_non_unital_non_assoc_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: F, f, R -/ -- algebra/gcd_monoid/basic.lean #check @associates.dvd_out_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @associates.out_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @dvd_gcd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @gcd_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @gcd_eq_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @gcd_eq_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @lcm_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @lcm_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @lcm_eq_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @lcm_eq_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/gcd_monoid/multiset.lean #check @multiset.lcm_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @multiset.gcd_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- algebra/group/defs.lean #check @semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @add_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @comm_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @add_comm_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @left_cancel_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @add_left_cancel_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @right_cancel_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @add_right_cancel_semigroup.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/group/hom.lean #check @add_monoid_hom.injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.injective_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_monoid_hom.injective_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebra/group/hom_instances.lean #check @add_monoid_hom.map_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebra/group/units.lean #check @add_units.eq_neg_add_iff_add_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @units.eq_inv_mul_iff_mul_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @units.inv_mul_eq_iff_eq_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_units.neg_add_eq_iff_eq_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_units.add_neg_eq_iff_eq_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @units.mul_inv_eq_iff_eq_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @units.is_unit_mul_units /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_units.is_add_unit_add_add_units /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @units.is_unit_units_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_units.is_add_unit_add_units_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/group_power/lemmas.lean #check @abs_add_eq_add_abs_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/homology/complex_shape.lean #check @complex_shape.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/homology/exact.lean #check @category_theory.preadditive.exact_iff_homology_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.mono_iff_exact_zero_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.epi_iff_exact_zero_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebra/homology/homological_complex.lean #check @homological_complex.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/homology/homotopy.lean #check @homotopy.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/indicator_function.lean #check @set.indicator_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @set.mul_indicator_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/invertible.lean #check @nonempty_invertible_iff_is_unit /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/lie/abelian.lean #check @lie_module.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, M, L -/ #check @lie_module.mem_max_triv_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, M, L -/ #check @lie_module.le_max_triv_iff_bracket_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, L, R -/ #check @lie_module.trivial_iff_le_maximal_trivial /- The following varibles are used on both sides of an equality or iff and should be made implicit: N, M, L, R -/ #check @lie_module.is_trivial_iff_max_triv_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, L -/ #check @lie_algebra.is_lie_abelian_iff_center_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: L -/ #check @lie_submodule.lie_abelian_iff_lie_self_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- algebra/lie/cartan_subalgebra.lean #check @lie_subalgebra.mem_normalizer_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, H -/ -- algebra/lie/classical.lean #check @lie_algebra.orthogonal.mem_so /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, R, n -/ -- algebra/lie/free.lean #check @free_lie_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- algebra/lie/ideal_operations.lean #check @lie_submodule.lie_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, N -/ -- algebra/lie/nilpotent.lean #check @lie_module.trivial_iff_lower_central_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, L -/ #check @lie_module.nilpotency_length_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @lie_module.nilpotency_length_eq_succ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, M, L, R -/ -- algebra/lie/quotient.lean #check @lie_submodule.quotient.mk_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @lie_submodule.quotient.map_mk'_eq_bot_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: N', N -/ -- algebra/lie/semisimple.lean #check @lie_algebra.is_semisimple_iff_no_solvable_ideals /- The following varibles are used on both sides of an equality or iff and should be made implicit: L, R -/ #check @lie_algebra.is_semisimple_iff_no_abelian_ideals /- The following varibles are used on both sides of an equality or iff and should be made implicit: L, R -/ #check @lie_algebra.abelian_radical_iff_solvable_is_abelian /- The following varibles are used on both sides of an equality or iff and should be made implicit: L, R -/ -- algebra/lie/skew_adjoint.lean #check @mem_skew_adjoint_matrices_lie_subalgebra /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, J -/ #check @mem_skew_adjoint_matrices_lie_subalgebra_unit_smul /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, J -/ -- algebra/lie/solvable.lean #check @lie_algebra.abelian_iff_derived_one_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @lie_algebra.abelian_iff_derived_succ_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, I -/ #check @lie_ideal.derived_series_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, I -/ #check @lie_algebra.lie_ideal.solvable_iff_le_radical /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, L, R -/ #check @lie_algebra.derived_series_of_derived_length_succ /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, I, L, R -/ #check @lie_algebra.derived_length_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @lie_algebra.abelian_of_solvable_ideal_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- algebra/lie/subalgebra.lean #check @lie_subalgebra.mem_carrier /- The following varibles are used on both sides of an equality or iff and should be made implicit: L' -/ #check @lie_subalgebra.mem_mk_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @lie_subalgebra.mem_coe_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: L' -/ #check @lie_subalgebra.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: L' -/ #check @lie_subalgebra.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, L' -/ #check @lie_subalgebra.coe_zero_iff_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, L' -/ #check @lie_subalgebra.ext_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: L₂', L₁' -/ #check @lie_subalgebra.coe_set_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: L₂', L₁' -/ #check @lie_subalgebra.coe_to_submodule_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: L₂', L₁' -/ #check @lie_hom.mem_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @submodule.exists_lie_subalgebra_coe_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @lie_subalgebra.mem_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, K, f -/ #check @lie_subalgebra.mem_map_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, e, K -/ #check @lie_subalgebra.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: K', K -/ #check @lie_subalgebra.coe_submodule_le_coe_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: K', K -/ #check @lie_subalgebra.mem_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @lie_subalgebra.mem_inf /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, K', K -/ #check @lie_subalgebra.eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @lie_subalgebra.mem_of_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- algebra/lie/submodule.lean #check @lie_submodule.mem_carrier /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @lie_submodule.mem_mk_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @lie_submodule.mem_coe_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @lie_submodule.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @lie_submodule.coe_to_submodule_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: N', N -/ #check @submodule.exists_lie_submodule_coe_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, L -/ #check @lie_subalgebra.mem_to_lie_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @lie_submodule.coe_submodule_le_coe_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: N', N -/ #check @lie_submodule.mem_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @lie_submodule.mem_inf /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, N', N -/ #check @lie_submodule.mem_sup /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, N', N -/ #check @lie_submodule.eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @lie_submodule.subsingleton_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @lie_submodule.nontrivial_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @lie_submodule.nontrivial_iff_ne_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, L, R -/ #check @lie_submodule.lie_span_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @lie_submodule.mem_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: m' -/ #check @lie_ideal.map_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I, f -/ #check @lie_hom.is_ideal_morphism_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_hom.is_ideal_morphism_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_hom.mem_ideal_range_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_hom.le_ker_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, f -/ #check @lie_hom.ker_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_hom.range_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @lie_module_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @lie_module_hom.le_ker_iff_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: M' -/ #check @lie_module_hom.mem_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, f -/ -- algebra/lie/universal_enveloping.lean #check @universal_enveloping_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f, R -/ -- algebra/lie/weights.lean #check @lie_module.mem_pre_weight_space /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, χ, M -/ #check @lie_module.mem_weight_space /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, χ, M -/ #check @lie_algebra.mem_zero_root_subalgebra /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, H, L, R -/ -- algebra/linear_recurrence.lean #check @linear_recurrence.is_sol_iff_mem_sol_space /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, E -/ #check @linear_recurrence.sol_eq_of_eq_init /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, u -/ #check @linear_recurrence.geom_sol_iff_root_char_poly /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, E -/ -- algebra/module/linear_map.lean #check @linear_map.restrict_scalars_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: gₗ, fₗ -/ -- algebra/module/submodule.lean #check @submodule.mem_to_add_submonoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @submodule.mem_carrier /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.smul_mem_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.restrict_scalars_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, V -/ #check @submodule.restrict_scalars_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, R -/ #check @submodule.mem_to_add_subgroup /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.to_add_subgroup_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p', p -/ #check @submodule.neg_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.add_mem_iff_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.add_mem_iff_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.smul_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- algebra/module/submodule_lattice.lean #check @submodule.eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.ne_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.mem_infi /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- algebra/monoid_algebra/grading.lean #check @add_monoid_algebra.mem_grade_by_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, i, f, R -/ #check @add_monoid_algebra.mem_grade_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, m, R -/ #check @add_monoid_algebra.mem_grade_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, m, R -/ -- algebra/opposites.lean #check @mul_opposite.unop_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mul_opposite.op_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mul_opposite.unop_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mul_opposite.op_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_opposite.unop_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mul_opposite.unop_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mul_opposite.op_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @add_opposite.op_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/order/absolute_value.lean #check @absolute_value.map_sub_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/order/lattice_group.lean #check @lattice_ordered_comm_group.le_iff_pos_le_neg_ge /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @lattice_ordered_comm_group.m_le_iff_pos_le_neg_ge /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/order/monoid.lean #check @with_top.zero_lt_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- algebra/order/ring.lean #check @le_iff_exists_nonneg_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @abs_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @dvd_abs /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @abs_dvd_abs /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/order/with_zero.lean #check @div_le_div₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: d, c, b, a -/ -- algebra/pointwise.lean #check @set.mem_finset_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, f, t -/ #check @set.mem_finset_sum /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, f, t -/ #check @set.mem_fintype_sum /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, f -/ #check @set.mem_fintype_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, f -/ #check @smul_mem_smul_set_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, A -/ #check @mem_smul_set_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, A -/ #check @mem_inv_smul_set_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, A -/ #check @finset.mul_nonempty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @finset.add_nonempty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ -- algebra/quadratic_discriminant.lean #check @quadratic_eq_zero_iff_discrim_eq_sq /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @quadratic_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @quadratic_eq_zero_iff_of_discrim_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- algebra/quandle.lean #check @shelf_hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @quandle.conj_swap /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/quaternion.lean #check @quaternion_algebra.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebra/regular/basic.lean #check @mul_is_left_regular_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @mul_is_right_regular_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ -- algebra/regular/smul.lean #check @is_smul_regular.smul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ -- algebra/ring/basic.lean #check @is_unit.neg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @ring_hom.injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ring_hom.injective_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @dvd_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @neg_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @even_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @odd_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @units.inv_eq_self_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ -- algebra/ring/boolean_ring.lean #check @add_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- algebra/squarefree.lean #check @multiplicity.squarefree_iff_multiplicity_le_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- algebra/tropical/basic.lean #check @tropical.trop_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @tropical.untrop_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- algebraic_geometry/AffineScheme.lean #check @algebraic_geometry.mem_AffineScheme /- The following varibles are used on both sides of an equality or iff and should be made implicit: X -/ -- algebraic_geometry/Gamma_Spec_adjunction.lean #check @algebraic_geometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, r, X -/ #check @algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_app_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, r, X -/ -- algebraic_geometry/Scheme.lean #check @algebraic_geometry.Scheme.mem_basic_open /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, X -/ #check @algebraic_geometry.Scheme.mem_basic_open_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, X -/ -- algebraic_geometry/gluing.lean #check @algebraic_geometry.Scheme.glue_data.ι_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, j, i, D -/ #check @algebraic_geometry.Scheme.glue_data.is_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: U, D -/ -- algebraic_geometry/prime_spectrum/basic.lean #check @prime_spectrum.mem_zero_locus /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, x -/ #check @prime_spectrum.mem_vanishing_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, t -/ #check @prime_spectrum.subset_zero_locus_iff_le_vanishing_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, t -/ #check @prime_spectrum.subset_zero_locus_iff_subset_vanishing_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, t, R -/ #check @prime_spectrum.zero_locus_subset_zero_locus_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I -/ #check @prime_spectrum.zero_locus_subset_zero_locus_singleton_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @prime_spectrum.is_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: U -/ #check @prime_spectrum.is_closed_iff_zero_locus /- The following varibles are used on both sides of an equality or iff and should be made implicit: Z -/ #check @prime_spectrum.is_closed_iff_zero_locus_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: Z -/ #check @prime_spectrum.is_closed_iff_zero_locus_radical_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: Z -/ #check @prime_spectrum.is_closed_singleton_iff_is_maximal /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @prime_spectrum.is_irreducible_zero_locus_iff_of_radical /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @prime_spectrum.is_irreducible_zero_locus_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @prime_spectrum.mem_basic_open /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @prime_spectrum.basic_open_le_basic_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @prime_spectrum.basic_open_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @prime_spectrum.as_ideal_le_as_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @prime_spectrum.as_ideal_lt_as_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @prime_spectrum.le_iff_mem_closure /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @prime_spectrum.le_iff_specializes /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @local_ring.is_local_ring_hom_iff_comap_closed_point /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- algebraic_geometry/properties.lean #check @algebraic_geometry.affine_is_reduced_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @algebraic_geometry.basic_open_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @algebraic_geometry.is_integral_iff_is_irreducible_and_is_reduced /- The following varibles are used on both sides of an equality or iff and should be made implicit: X -/ #check @algebraic_geometry.affine_is_integral_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- algebraic_geometry/ringed_space.lean #check @algebraic_geometry.RingedSpace.mem_basic_open /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, X -/ #check @algebraic_geometry.RingedSpace.mem_top_basic_open /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, X -/ -- analysis/analytic/basic.lean #check @formal_multilinear_series.radius_eq_top_iff_summable_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- analysis/analytic/composition.lean #check @formal_multilinear_series.mem_comp_partial_sum_source_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, N, M, m -/ #check @composition.sigma_composition_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: j, i -/ #check @composition.sigma_pi_composition_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, u -/ -- analysis/asymptotics/superpolynomial_decay.lean #check @asymptotics.superpolynomial_decay_iff_abs_tendsto_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_iff_superpolynomial_decay_abs /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_mul_const_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_const_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_iff_abs_is_bounded_under /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_iff_zpow_tendsto_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_param_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_mul_param_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_param_pow_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_mul_param_pow_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_iff_norm_tendsto_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_iff_superpolynomial_decay_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, k, l -/ #check @asymptotics.superpolynomial_decay_iff_is_O /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @asymptotics.superpolynomial_decay_iff_is_o /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/box_integral/box/basic.lean #check @box_integral.box.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @box_integral.box.mem_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @box_integral.box.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I -/ -- analysis/box_integral/partition/basic.lean #check @box_integral.prepartition.mem_boxes /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_Union /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_bUnion /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_restrict /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_restrict' /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.bUnion_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.le_bUnion_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.distortion_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ -- analysis/box_integral/partition/filter.lean #check @box_integral.integration_params.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- analysis/box_integral/partition/tagged.lean #check @box_integral.tagged_prepartition.mem_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.tagged_prepartition.mem_Union /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.tagged_prepartition.is_partition_iff_Union_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.tagged_prepartition.mem_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.mem_bUnion_tagged /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ #check @box_integral.prepartition.forall_bUnion_tagged /- The following varibles are used on both sides of an equality or iff and should be made implicit: πi, π, p -/ #check @box_integral.tagged_prepartition.forall_mem_single /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @box_integral.tagged_prepartition.distortion_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: π -/ -- analysis/calculus/fderiv.lean #check @continuous_linear_equiv.comp_has_fderiv_within_at_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: iso -/ #check @continuous_linear_equiv.comp_has_fderiv_at_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: iso -/ #check @linear_isometry_equiv.comp_has_fderiv_within_at_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: iso -/ #check @linear_isometry_equiv.comp_has_fderiv_at_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: iso -/ -- analysis/calculus/tangent_cone.lean #check @unique_diff_within_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s, 𝕜 -/ -- analysis/complex/basic.lean #check @complex.has_sum_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, f -/ -- analysis/complex/roots_of_unity.lean #check @complex.is_primitive_root_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, ζ -/ #check @complex.mem_roots_of_unity /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n -/ -- analysis/convex/basic.lean #check @mem_segment_translate /- The following varibles are used on both sides of an equality or iff and should be made implicit: 𝕜 -/ #check @mem_open_segment_translate /- The following varibles are used on both sides of an equality or iff and should be made implicit: 𝕜 -/ -- analysis/convex/cone.lean #check @convex_cone.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @convex_cone.mem_inf /- The following varibles are used on both sides of an equality or iff and should be made implicit: T, S -/ #check @convex_cone.smul_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @convex_cone.pointed_iff_not_blunt /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @convex_cone.blunt_iff_not_pointed /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @convex_cone.salient_iff_not_flat /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @mem_inner_dual_cone /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, y -/ -- analysis/convex/hull.lean #check @convex.convex_remove_iff_not_mem_convex_hull_remove /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- analysis/convex/independent.lean #check @convex_independent.mem_convex_hull_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, s -/ -- analysis/convex/simplicial_complex/basic.lean #check @geometry.simplicial_complex.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- analysis/inner_product_space/adjoint.lean #check @continuous_linear_map.eq_adjoint_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @linear_map.eq_adjoint_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @linear_map.eq_adjoint_iff_basis /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @linear_map.eq_adjoint_iff_basis_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @linear_map.eq_adjoint_iff_basis_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ -- analysis/inner_product_space/basic.lean #check @norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @real_inner_add_sub_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @abs_inner_div_norm_mul_norm_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @abs_real_inner_div_norm_mul_norm_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @abs_inner_eq_norm_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @real_inner_div_norm_mul_norm_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @real_inner_div_norm_mul_norm_eq_neg_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @orthogonal_family.summable_iff_norm_sq_summable /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submodule.mem_orthogonal /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, K -/ #check @submodule.mem_orthogonal' /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, K -/ #check @submodule.orthogonal_eq_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @inner_product_space.is_self_adjoint_iff_bilin_form /- The following varibles are used on both sides of an equality or iff and should be made implicit: T -/ -- analysis/inner_product_space/conformal_linear_map.lean #check @is_conformal_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f' -/ -- analysis/inner_product_space/projection.lean #check @norm_eq_infi_iff_real_inner_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @norm_eq_infi_iff_inner_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @reflection_eq_self_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- analysis/normed/group/basic.lean #check @mem_sphere_iff_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, w, v -/ #check @add_monoid_hom.isometry_iff_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/normed/group/hom.lean #check @normed_group_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, f -/ #check @normed_group_hom.mem_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, f -/ #check @normed_group_hom.isometry_iff_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/normed/group/quotient.lean #check @quotient_norm_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, S -/ -- analysis/normed_space/continuous_affine_map.lean #check @continuous_affine_map.cont_linear_eq_zero_iff_exists_const /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/normed_space/dual.lean #check @normed_space.eq_zero_iff_forall_dual_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- analysis/normed_space/multilinear.lean #check @continuous_multilinear_map.op_norm_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/normed_space/operator_norm.lean #check @continuous_linear_map.isometry_iff_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_linear_equiv.has_sum /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @continuous_linear_equiv.tsum_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @continuous_linear_map.op_norm_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- analysis/normed_space/pointwise.lean #check @set_smul_mem_nhds_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- analysis/normed_space/weak_dual.lean #check @normed_space.dual.to_weak_dual_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y', x' -/ #check @weak_dual.to_normed_dual_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y', x' -/ -- analysis/seminorm.lean #check @seminorm.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @seminorm.lt_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @seminorm.mem_ball /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @seminorm.mem_ball_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- analysis/special_functions/polynomials.lean #check @polynomial.tendsto_at_top_iff_leading_coeff_nonneg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.tendsto_at_bot_iff_leading_coeff_nonpos /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.abs_is_bounded_under_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.abs_tendsto_at_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.tendsto_nhds_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.div_tendsto_zero_iff_degree_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: Q, P -/ -- analysis/special_functions/pow.lean #check @complex.cpow_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- analysis/special_functions/trigonometric/basic.lean #check @real.cos_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- category_theory/abelian/exact.lean #check @category_theory.abelian.exact_iff_image_eq_kernel /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.abelian.exact_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.abelian.exact_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.abelian.mono_iff_kernel_ι_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.abelian.epi_iff_cokernel_π_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/abelian/pseudoelements.lean #check @category_theory.abelian.pseudoelement.pseudo_zero_aux /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.abelian.pseudoelement.pseudo_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @category_theory.abelian.pseudoelement.eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/adjunction/basic.lean #check @category_theory.adjunction.hom_equiv_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f, adj -/ #check @category_theory.adjunction.eq_hom_equiv_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f, adj -/ -- category_theory/adjunction/evaluation.lean #check @category_theory.nat_trans.mono_iff_app_mono /- The following varibles are used on both sides of an equality or iff and should be made implicit: η, D -/ #check @category_theory.nat_trans.epi_iff_app_epi /- The following varibles are used on both sides of an equality or iff and should be made implicit: η, D -/ -- category_theory/arrow.lean #check @category_theory.arrow.mk_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @category_theory.arrow.lift_struct.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/bicategory/basic.lean #check @category_theory.bicategory.whisker_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: θ, η -/ #check @category_theory.bicategory.whisker_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: θ, η -/ -- category_theory/closed/cartesian.lean #check @category_theory.cartesian_closed.curry_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.cartesian_closed.eq_curry_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- category_theory/comma.lean #check @category_theory.comma_morphism.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/differential_object.lean #check @category_theory.differential_object.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/endomorphism.lean #check @category_theory.is_unit_iff_is_iso /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/enriched/basic.lean #check @category_theory.graded_nat_trans.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/equivalence.lean #check @category_theory.equivalence.cancel_unit_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.equivalence.cancel_unit_inv_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f, e -/ #check @category_theory.equivalence.cancel_counit_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f, e -/ #check @category_theory.equivalence.cancel_counit_inv_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.equivalence.cancel_unit_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ #check @category_theory.equivalence.cancel_counit_inv_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ #check @category_theory.equivalence.cancel_unit_right_assoc' /- The following varibles are used on both sides of an equality or iff and should be made implicit: h', g', f', h, g, f -/ #check @category_theory.equivalence.cancel_counit_inv_right_assoc' /- The following varibles are used on both sides of an equality or iff and should be made implicit: h', g', f', h, g, f -/ #check @category_theory.equivalence.functor_map_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.equivalence.inverse_map_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- category_theory/essentially_small.lean #check @category_theory.essentially_small_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: C -/ -- category_theory/flat_functors.lean #check @category_theory.flat_iff_Lan_flat /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- category_theory/isomorphism.lean #check @category_theory.iso.inv_comp_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.eq_inv_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.comp_inv_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.eq_comp_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.inv_eq_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.iso.hom_comp_eq_id /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.comp_hom_eq_id /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.iso.hom_eq_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: β, α -/ #check @category_theory.is_iso.inv_comp_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.is_iso.eq_inv_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.is_iso.comp_inv_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.is_iso.eq_comp_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @category_theory.hom_comp_eq_id /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @category_theory.comp_hom_eq_id /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @category_theory.iso.cancel_iso_hom_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', g -/ #check @category_theory.iso.cancel_iso_inv_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', g -/ #check @category_theory.iso.cancel_iso_hom_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.iso.cancel_iso_inv_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.iso.cancel_iso_hom_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ #check @category_theory.iso.cancel_iso_inv_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ -- category_theory/lifting_properties.lean #check @category_theory.right_lifting_property_initial_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i -/ -- category_theory/limits/concrete_category.lean #check @category_theory.limits.concrete.is_colimit_rep_eq_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, F -/ #check @category_theory.limits.concrete.colimit_rep_eq_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, F -/ -- category_theory/limits/cones.lean #check @category_theory.limits.cone_morphism.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.limits.cocone_morphism.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/limits/shapes/images.lean #check @category_theory.limits.image_map.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/limits/shapes/types.lean #check @category_theory.limits.types.type_equalizer_iff_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/limits/types.lean #check @category_theory.limits.types.limit_ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, F -/ #check @category_theory.limits.types.filtered_colimit.colimit_eq_iff_aux /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @category_theory.limits.types.filtered_colimit.is_colimit_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @category_theory.limits.types.filtered_colimit.colimit_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- category_theory/monad/algebra.lean #check @category_theory.monad.algebra.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.comonad.coalgebra.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monad/basic.lean #check @category_theory.monad_hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.comonad_hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monoidal/Mod.lean #check @Mod.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monoidal/Mon_.lean #check @Mon_.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monoidal/category.lean #check @category_theory.monoidal_category.tensor_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.monoidal_category.tensor_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- category_theory/monoidal/center.lean #check @category_theory.center.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monoidal/natural_transformation.lean #check @category_theory.monoidal_nat_trans.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/monoidal/opposite.lean #check @category_theory.monoidal_opposite.op_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.monoidal_opposite.unop_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/natural_isomorphism.lean #check @category_theory.nat_iso.cancel_nat_iso_hom_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', g -/ #check @category_theory.nat_iso.cancel_nat_iso_inv_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', g -/ #check @category_theory.nat_iso.cancel_nat_iso_hom_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.nat_iso.cancel_nat_iso_inv_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f -/ #check @category_theory.nat_iso.cancel_nat_iso_hom_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ #check @category_theory.nat_iso.cancel_nat_iso_inv_right_assoc /- The following varibles are used on both sides of an equality or iff and should be made implicit: g', f', g, f -/ -- category_theory/natural_transformation.lean #check @category_theory.nat_trans.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/preadditive/default.lean #check @category_theory.preadditive.mono_iff_cancel_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.preadditive.epi_iff_cancel_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/preadditive/schur.lean #check @category_theory.is_iso_iff_nonzero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @has_scalar.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @module.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @mul_action.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @distrib_mul_action.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.finrank_hom_simple_simple_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: Y, X -/ #check @category_theory.finrank_hom_simple_simple_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: Y, X -/ -- category_theory/quotient.lean #check @category_theory.quotient.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.quotient.functor_map_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f', f, r -/ -- category_theory/sites/closed.lean #check @category_theory.grothendieck_topology.covers_iff_mem_of_closed /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.grothendieck_topology.is_closed_iff_close_eq_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, J₁ -/ #check @category_theory.grothendieck_topology.close_eq_top_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, J₁ -/ #check @category_theory.grothendieck_topology.closed_iff_closed /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, J₁ -/ -- category_theory/sites/grothendieck.lean #check @category_theory.grothendieck_topology.mem_sieves_iff_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: J -/ #check @category_theory.grothendieck_topology.intersection_covering_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: J -/ #check @category_theory.grothendieck_topology.covers_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, S, J -/ #check @category_theory.grothendieck_topology.covering_iff_covers_id /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, J -/ #check @category_theory.grothendieck_topology.bot_covers /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, S -/ #check @category_theory.grothendieck_topology.cover.arrow.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.grothendieck_topology.cover.relation.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.grothendieck_topology.cover.coe_pullback /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, g, f -/ -- category_theory/sites/induced_topology.lean #check @category_theory.locally_cover_dense.pushforward_cover_iff_cover_pullback /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- category_theory/sites/pretopology.lean #check @category_theory.pretopology.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.pretopology.mem_to_grothendieck /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, X, K, C -/ -- category_theory/sites/sheaf.lean #check @category_theory.Sheaf.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.is_sheaf_iff_is_sheaf_of_type /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, J -/ #check @category_theory.presheaf.is_sheaf_iff_multifork /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, J -/ #check @category_theory.presheaf.is_sheaf_iff_multiequalizer /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, J -/ #check @category_theory.presheaf.is_sheaf_iff_is_sheaf' /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, J -/ #check @category_theory.presheaf.is_sheaf_iff_is_sheaf_forget /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, J -/ -- category_theory/sites/sheaf_of_types.lean #check @category_theory.presieve.pullback_compatible_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @category_theory.presieve.compatible_iff_sieve_compatible /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @category_theory.presieve.extension_iff_amalgamation /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, x -/ #check @category_theory.presieve.is_sheaf_for_iff_generate /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @category_theory.presieve.is_sheaf_pretopology /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @category_theory.equalizer.sieve.compatible_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S, P -/ #check @category_theory.equalizer.sieve.equalizer_sheaf_condition /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, P -/ #check @category_theory.equalizer.presieve.compatible_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, R, P -/ #check @category_theory.equalizer.presieve.sheaf_condition /- The following varibles are used on both sides of an equality or iff and should be made implicit: R, P -/ #check @category_theory.SheafOfTypes.hom.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/sites/sheafification.lean #check @category_theory.grothendieck_topology.plus.eq_mk_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/sites/sieves.lean #check @category_theory.presieve.singleton_eq_iff_domain /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.presieve.functor_pullback_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, R, F -/ #check @category_theory.sieve.Inf_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.sieve.Sup_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.sieve.inter_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.sieve.union_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.sieve.sets_iff_generate /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, R -/ #check @category_theory.sieve.pullback_eq_top_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- category_theory/subobject/factor_thru.lean #check @category_theory.mono_over.factors_congr /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ #check @category_theory.subobject.mk_factors_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @category_theory.subobject.factors_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, P -/ -- category_theory/subobject/lattice.lean #check @category_theory.subobject.is_iso_iff_mk_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.subobject.is_iso_arrow_iff_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @category_theory.subobject.bot_factors_iff_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.subobject.inf_factors /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.subobject.finset_inf_factors /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.subobject.symm_apply_mem_iff_mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s, e -/ -- category_theory/subobject/limits.lean #check @category_theory.limits.equalizer_subobject_factors_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: h, g, f -/ #check @category_theory.limits.kernel_subobject_factors_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: h, f -/ -- category_theory/subobject/well_powered.lean #check @category_theory.essentially_small_mono_over_iff_small_subobject /- The following varibles are used on both sides of an equality or iff and should be made implicit: X -/ -- category_theory/triangulated/basic.lean #check @category_theory.triangulated.triangle_morphism.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- category_theory/types.lean #check @category_theory.hom_of_element_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @category_theory.mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.epi_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @category_theory.is_iso_iff_bijective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- combinatorics/colex.lean #check @colex.eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.lt_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.hom_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.hom_fin_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.hom_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.hom_fin_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.sdiff_lt_sdiff_iff_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.sdiff_le_sdiff_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.sum_two_pow_lt_iff_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @colex.sum_two_pow_le_iff_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ -- combinatorics/composition.lean #check @composition.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @composition_as_set.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @composition.mem_range_embedding_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @composition.mem_range_embedding_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @composition_as_set.mem_boundaries_iff_exists_blocks_sum_take_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ -- combinatorics/derangements/basic.lean #check @derangements.equiv.remove_none.mem_fiber /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, a -/ -- combinatorics/double_counting.lean #check @finset.mem_bipartite_below /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @finset.mem_bipartite_above /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- combinatorics/hall/basic.lean #check @finset.all_card_le_bUnion_card_iff_exists_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: t -/ #check @fintype.all_card_le_rel_image_card_iff_exists_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @fintype.all_card_le_filter_rel_iff_exists_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- combinatorics/hall/finite.lean #check @finset.all_card_le_bUnion_card_iff_exists_injective' /- The following varibles are used on both sides of an equality or iff and should be made implicit: t -/ -- combinatorics/hindman.lean #check @ultrafilter.eventually_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, V, U -/ #check @ultrafilter.eventually_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, V, U -/ -- combinatorics/partition.lean #check @nat.partition.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- combinatorics/quiver/connected_component.lean #check @quiver.weakly_connected_component.eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- combinatorics/quiver/subquiver.lean #check @quiver.total.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- combinatorics/simple_graph/adj_matrix.lean #check @matrix.is_adj_matrix.apply_ne_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: j, i -/ #check @matrix.is_adj_matrix.apply_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: j, i -/ -- combinatorics/simple_graph/basic.lean #check @simple_graph.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @simple_graph.from_rel_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, r -/ #check @simple_graph.adj_comm /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, u, G -/ #check @simple_graph.sup_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, y, x -/ #check @simple_graph.inf_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, y, x -/ #check @simple_graph.compl_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G -/ #check @simple_graph.sdiff_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, y, x -/ #check @simple_graph.top_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ #check @simple_graph.mem_support /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mem_edge_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.adj_iff_exists_edge /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.adj_iff_exists_edge_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mk_mem_incidence_set_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mk_mem_incidence_set_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mk_mem_incidence_set_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.edge_mem_incidence_set_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mem_edge_finset /- The following varibles are used on both sides of an equality or iff and should be made implicit: e, G -/ #check @simple_graph.mem_neighbor_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G -/ #check @simple_graph.mem_neighbor_set' /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G -/ #check @simple_graph.mem_incidence_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G -/ #check @simple_graph.mem_incidence_iff_neighbor /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.mem_common_neighbors /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @simple_graph.delete_edges_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, s, G -/ #check @simple_graph.mem_neighbor_finset /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G -/ #check @simple_graph.degree_pos_iff_exists_adj /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, G -/ #check @simple_graph.mem_incidence_finset /- The following varibles are used on both sides of an equality or iff and should be made implicit: e, v, G -/ -- combinatorics/simple_graph/coloring.lean #check @simple_graph.colorable_iff_exists_bdd_nat_coloring /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- combinatorics/simple_graph/connectivity.lean #check @simple_graph.walk.mem_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.mem_tail_support_append_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p', p -/ #check @simple_graph.walk.mem_support_append_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p', p -/ #check @simple_graph.walk.is_trail_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.is_path_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.is_cycle_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.cons_is_trail_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.reverse_is_trail_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.cons_is_path_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @simple_graph.walk.is_path_reverse_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- combinatorics/simple_graph/degree_sum.lean #check @simple_graph.dart.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @simple_graph.dart_edge_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: d₂, d₁ -/ -- combinatorics/simple_graph/matching.lean #check @simple_graph.subgraph.is_perfect_matching_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ -- combinatorics/simple_graph/subgraph.lean #check @simple_graph.subgraph.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @simple_graph.subgraph.adj_comm /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G' -/ #check @simple_graph.subgraph.mem_support /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @simple_graph.subgraph.mem_neighbor_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v, G' -/ -- computability/DFA.lean #check @DFA.mem_accepts /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, M -/ -- computability/NFA.lean #check @NFA.mem_step_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, S, s, M -/ -- computability/halting.lean #check @computable_pred.rice₂ /- The following varibles are used on both sides of an equality or iff and should be made implicit: C -/ -- computability/language.lean #check @language.mem_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @language.mem_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, m, l -/ #check @language.mem_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, m, l -/ #check @language.mem_star /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, l -/ #check @language.le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, l -/ -- computability/primrec.lean #check @primrec.of_equiv_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- computability/reduce.lean #check @many_one_equiv_to_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ -- computability/regular_expressions.lean #check @regular_expression.one_rmatch_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @regular_expression.char_rmatch_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, a -/ #check @regular_expression.add_rmatch_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, Q, P -/ #check @regular_expression.mul_rmatch_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, Q, P -/ #check @regular_expression.star_rmatch_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, P -/ #check @regular_expression.rmatch_iff_matches /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, P -/ -- computability/turing_machine.lean #check @turing.TM2to1.supports_run /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, S -/ #check @turing.TM2to1.tr_eval_dom /- The following varibles are used on both sides of an equality or iff and should be made implicit: L, k, M -/ -- control/functor/multivariate.lean #check @mvfunctor.exists_iff_exists_of_mono /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @mvfunctor.liftp_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @mvfunctor.liftr_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ #check @mvfunctor.liftp_last_pred_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @mvfunctor.liftr_last_rel_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, rr -/ -- control/lawful_fix.lean #check @part.fix.mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, f -/ -- control/traversable/instances.lean #check @list.mem_traverse /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, l -/ -- data/analysis/filter.lean #check @cfilter.mem_to_filter_sets /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @filter.realizer.tendsto_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- data/analysis/topology.lean #check @ctop.mem_nhds_to_topsp /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- data/bool/basic.lean #check @bool.coe_to_bool /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/buffer/parser/basic.lean #check @parser.fail_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, cb, p -/ #check @parser.success_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, cb, p -/ -- data/complex/exponential.lean #check @real.exp_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/dfinsupp/basic.lean #check @dfinsupp.single_eq_single_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: xj, xi, j, i -/ #check @dfinsupp.mem_support_to_fun /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, f -/ #check @add_submonoid.mem_supr_iff_exists_dfinsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_supr_iff_exists_dfinsupp' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_bsupr_iff_exists_dfinsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S, p -/ -- data/dfinsupp/order.lean #check @dfinsupp.add_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- data/equiv/basic.lean #check @equiv.apply_eq_iff_eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @equiv.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @equiv.injective_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.comp_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.surjective_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.comp_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.bijective_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.comp_bijective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- data/equiv/module.lean #check @linear_equiv.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @linear_equiv.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @linear_equiv.restrict_scalars_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- data/equiv/mul_add.lean #check @mul_equiv.apply_eq_iff_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @add_equiv.apply_eq_iff_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @mul_equiv.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @add_equiv.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @add_equiv.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @mul_equiv.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- data/equiv/option.lean #check @equiv.option_symm_apply_none_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @equiv.some_remove_none_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- data/equiv/ring.lean #check @ring_equiv.coe_ring_hom_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- data/equiv/set.lean #check @equiv.subset_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, e -/ #check @equiv.subset_image' /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, e -/ #check @equiv.eq_image_iff_symm_image_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, e -/ #check @equiv.preimage_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @equiv.image_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @equiv.image_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @equiv.preimage_eq_iff_eq_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, e -/ #check @equiv.eq_preimage_iff_image_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, e -/ -- data/fin/basic.lean #check @fin.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @fin.eq_iff_veq /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @fin.ne_iff_vne /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @fin.pos_iff_ne_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @fin.succ_eq_last_succ /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ #check @fin.cast_succ_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @fin.cast_succ_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @fin.succ_above_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, p -/ #check @fin.lt_succ_above_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, p -/ -- data/fin_enum.lean #check @fin_enum.finset.mem_enum /- The following varibles are used on both sides of an equality or iff and should be made implicit: xs, s -/ -- data/finmap.lean #check @finmap.mem_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @finmap.mem_list_to_finmap /- The following varibles are used on both sides of an equality or iff and should be made implicit: xs, a -/ #check @finmap.disjoint.symm_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @finmap.disjoint_union_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, y, x -/ #check @finmap.disjoint_union_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, y, x -/ -- data/finset/basic.lean #check @finset.not_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @finset.nonempty_coe_sort /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.singleton_iff_unique_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.union_eq_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @finset.inter_eq_left_iff_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @finset.inter_eq_right_iff_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @finset.attach_nonempty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.attach_eq_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.sdiff_eq_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: s₂, s₁ -/ #check @finset.exists_mem_insert /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, s, a -/ #check @finset.forall_mem_insert /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, s, a -/ #check @multiset.to_finset_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: m2, m1 -/ #check @list.to_finset_eq_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @finset.fiber_nonempty_iff_mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, s, f -/ #check @finset.mem_to_list /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.disjoint_self_iff_empty /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.disjoint_bUnion_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, f, s -/ #check @finset.disjoint_bUnion_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, t, s -/ -- data/finset/card.lean #check @finset.fiber_card_ne_zero_iff_mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, f, s -/ -- data/finset/fold.lean #check @finset.le_fold_min /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.fold_min_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.lt_fold_min /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.fold_min_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.fold_max_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.le_fold_max /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.fold_max_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @finset.lt_fold_max /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ -- data/finset/lattice.lean #check @finset.sup_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, f -/ #check @finset.inf_eq_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, f -/ #check @finset.sup'_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.sup'_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.le_sup'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.lt_sup'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.le_inf'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.lt_inf'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.inf'_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.inf'_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @finset.le_min'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.max'_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.max'_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.lt_min'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- data/finset/prod.lean #check @finset.mem_diag /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ #check @finset.mem_off_diag /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ -- data/finset/sigma.lean #check @finset.mem_sigma_lift /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, b, a, f -/ #check @finset.mk_mem_sigma_lift /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, b, a, i, f -/ -- data/finsupp/basic.lean #check @finsupp.mem_support_single /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a', a -/ #check @finsupp.single_eq_single_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b₂, b₁, a₂, a₁ -/ #check @finsupp.mem_split_support_iff_nonzero /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, l -/ -- data/finsupp/multiset.lean #check @finsupp.mem_to_multiset /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, f -/ -- data/finsupp/order.lean #check @finsupp.add_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @finsupp.le_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @finsupp.le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- data/fintype/basic.lean #check @finset.compl_ne_univ_iff_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.card_eq_iff_eq_univ /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.card_lt_iff_ne_univ /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @finset.card_compl_lt_iff_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @fintype.bijective_iff_injective_and_card /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @fintype.bijective_iff_surjective_and_card /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @set_fintype_card_eq_univ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- data/fintype/list.lean #check @multiset.mem_lists_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, s -/ -- data/hash_map.lean #check @bucket_array.mem_as_list /- The following varibles are used on both sides of an equality or iff and should be made implicit: data -/ #check @hash_map.valid.contains_aux_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @hash_map.find_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, m -/ #check @hash_map.contains_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, m -/ #check @hash_map.mem_insert /- The following varibles are used on both sides of an equality or iff and should be made implicit: b', a', b, a, m -/ #check @hash_map.mem_erase /- The following varibles are used on both sides of an equality or iff and should be made implicit: b', a', a, m -/ -- data/int/basic.lean #check @int.dvd_iff_mod_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @int.exists_lt_and_lt_iff_not_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @int.lt_div_iff_mul_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @int.mem_to_nat' /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, a -/ -- data/int/parity.lean #check @int.even_coe_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @int.odd_coe_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/int/sqrt.lean #check @int.exists_mul_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/lazy_list/basic.lean #check @lazy_list.mem_cons /- The following varibles are used on both sides of an equality or iff and should be made implicit: ys, y, x -/ -- data/list/alist.lean #check @alist.mem_insert /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- data/list/basic.lean #check @list.exists_mem_cons_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, a, p -/ #check @list.mem_pure /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @list.update_nth_eq_nil /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @list.attach_eq_nil /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @list.mem_filter_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, f -/ #check @list.mem_map_swap /- The following varibles are used on both sides of an equality or iff and should be made implicit: xs, y, x -/ -- data/list/big_operators.lean #check @list.prod_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @list.sum_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ -- data/list/chain.lean #check @list.chain_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, ᾰ, R -/ #check @list.chain_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @list.chain'_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- data/list/count.lean #check @list.countp_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @list.length_filter_lt_length_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, p -/ -- data/list/forall2.lean #check @list.forall₂_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, ᾰ, R -/ #check @list.forall₂_and_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, l -/ -- data/list/infix.lean #check @list.infix_iff_prefix_suffix /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁ -/ #check @list.mem_inits /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @list.mem_tails /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ -- data/list/join.lean #check @list.eq_iff_join_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: L', L -/ -- data/list/lattice.lean #check @list.bag_inter_nil_iff_inter_nil /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁ -/ -- data/list/nodup.lean #check @list.nodup.ne_singleton_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/list/of_fn.lean #check @list.mem_of_fn /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, f -/ -- data/list/pairwise.lean #check @list.pairwise_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, R -/ #check @list.pairwise_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @list.pairwise_filter_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @list.pairwise_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @list.forall_mem_pw_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, a -/ -- data/list/zip.lean #check @list.nth_zip_with_eq_some /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, z, l₂, l₁, f -/ #check @list.nth_zip_eq_some /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, z, l₂, l₁ -/ -- data/multiset/basic.lean #check @multiset.coe_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @multiset.mem_to_list /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, a -/ #check @multiset.mem_filter_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, f -/ #check @multiset.rel_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, ᾰ, r -/ #check @multiset.coe_disjoint /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁ -/ -- data/multiset/pi.lean #check @multiset.mem_pi /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, t, m -/ -- data/mv_polynomial/basic.lean #check @mv_polynomial.C_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, r, R -/ #check @mv_polynomial.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @mv_polynomial.C_dvd_iff_dvd_coeff /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ, r -/ #check @mv_polynomial.C_dvd_iff_map_hom_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ -/ #check @mv_polynomial.map_map_range_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ, g, f -/ -- data/mv_polynomial/variables.lean #check @mv_polynomial.mem_vars /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ -- data/nat/basic.lean #check @nat.add_pos_iff_pos_or_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.exists_lt_and_lt_iff_not_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @nat.find_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.find_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.le_find_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.lt_find_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/nat/digits.lean #check @nat.dvd_iff_dvd_digits_sum /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, b -/ #check @nat.three_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.nine_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.dvd_iff_dvd_of_digits /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, b -/ #check @nat.eleven_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/nat/enat.lean #check @enat.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @enat.lt_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @enat.le_coe_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @enat.lt_coe_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @enat.coe_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n -/ #check @enat.coe_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n -/ #check @enat.eq_top_iff_forall_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @enat.eq_top_iff_forall_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @enat.lt_find_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, P -/ #check @enat.find_eq_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ -- data/nat/factorization.lean #check @nat.factorization_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/nat/gcd.lean #check @nat.coprime_add_mul_right_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_add_mul_left_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_mul_right_add_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_mul_left_add_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_add_mul_right_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_add_mul_left_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_mul_right_add_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_mul_left_add_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @nat.coprime_pow_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @nat.coprime_pow_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @nat.coprime_zero_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.coprime_zero_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.coprime_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/nat/lattice.lean #check @nat.Inf_upward_closed_eq_succ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ -- data/nat/nth.lean #check @nat.count_le_iff_le_nth /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @nat.lt_nth_iff_count_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/nat/prime.lean #check @irreducible_iff_nat_prime /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @nat.two_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.min_fac_eq_two_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.factors_eq_nil /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @nat.mem_factors_mul_of_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @nat.factors_mul_of_coprime /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/nat/sqrt.lean #check @nat.exists_mul_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @nat.exists_mul_self' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/nat/totient.lean #check @nat.prime_iff_card_units /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/nat/with_bot.lean #check @nat.with_bot.lt_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/num/lemmas.lean #check @num.dvd_to_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @pos_num.cmp_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @num.cmp_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @znum.dvd_to_int /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ -- data/opposite.lean #check @opposite.op_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @opposite.unop_inj_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- data/option/basic.lean #check @option.orelse_eq_some /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, o', o -/ #check @option.orelse_eq_some' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, o', o -/ #check @option.orelse_eq_none /- The following varibles are used on both sides of an equality or iff and should be made implicit: o', o -/ #check @option.orelse_eq_none' /- The following varibles are used on both sides of an equality or iff and should be made implicit: o', o -/ -- data/part.lean #check @part.of_option_dom /- The following varibles are used on both sides of an equality or iff and should be made implicit: o -/ #check @part.mem_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @part.bind_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, f, x -/ #check @part.mem_restrict /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, o, p -/ -- data/pequiv.lean #check @pequiv.mem_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @pequiv.eq_some_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @pequiv.mem_trans /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, a, g, f -/ #check @pequiv.trans_eq_some /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, a, g, f -/ #check @pequiv.trans_eq_none /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, g, f -/ #check @pequiv.mem_single_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b₂, b₁, a₂, a₁ -/ -- data/pfun.lean #check @pfun.mem_dom /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @pfun.mem_restrict /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @pfun.mem_res /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, s, f -/ #check @pfun.dom_iff_graph /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @pfun.mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, y, f -/ #check @pfun.mem_preimage /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s, f -/ #check @pfun.mem_core /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, x, f -/ #check @pfun.mem_core_res /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, t, s, f -/ -- data/pfunctor/multivariate/basic.lean #check @mvpfunctor.liftp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @mvpfunctor.liftp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, a, p -/ #check @mvpfunctor.liftr_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ -- data/pfunctor/univariate/M.lean #check @pfunctor.M.agree_iff_agree' /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- data/pfunctor/univariate/basic.lean #check @pfunctor.liftp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @pfunctor.liftp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, a, p -/ #check @pfunctor.liftr_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ -- data/pi.lean #check @pi.single_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, f -/ -- data/pnat/basic.lean #check @pnat.mk_le_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, n -/ #check @pnat.mk_lt_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, n -/ #check @pnat.coe_le_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, n -/ #check @pnat.coe_lt_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, n -/ #check @pnat.bit0_le_bit0 /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, n -/ #check @pnat.bit0_le_bit1 /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, n -/ #check @pnat.bit1_le_bit0 /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, n -/ #check @pnat.bit1_le_bit1 /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, n -/ #check @pnat.dvd_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ -- data/pnat/factors.lean #check @pnat.count_factor_multiset /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, p, m -/ -- data/pnat/xgcd.lean #check @pnat.xgcd_type.is_special_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ #check @pnat.xgcd_type.is_reduced_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ #check @pnat.xgcd_type.flip_is_reduced /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ #check @pnat.xgcd_type.flip_is_special /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ -- data/polynomial/basic.lean #check @polynomial.forall_iff_forall_finsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.exists_iff_exists_finsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @polynomial.monomial_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t -/ -- data/polynomial/coeff.lean #check @polynomial.C_dvd_iff_dvd_coeff /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ, r -/ -- data/polynomial/degree/definitions.lean #check @polynomial.degree_le_iff_coeff_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, f -/ #check @polynomial.degree_lt_iff_coeff_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, f -/ -- data/polynomial/derivative.lean #check @polynomial.mem_support_derivative /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, p -/ -- data/polynomial/eval.lean #check @polynomial.mem_map_srange /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @polynomial.mem_map_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @polynomial.is_root_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p, s -/ -- data/polynomial/lifts.lean #check @polynomial.mem_lifts /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @polynomial.lifts_iff_set_range /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @polynomial.lifts_iff_ring_hom_srange /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @polynomial.lifts_iff_coeff_lifts /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @polynomial.lifts_iff_lifts_ring /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f -/ #check @polynomial.mem_lifts_iff_mem_alg /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, R -/ -- data/polynomial/mirror.lean #check @polynomial.mirror_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/prod.lean #check @prod.lex_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, r -/ -- data/qpf/multivariate/basic.lean #check @mvqpf.liftp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @mvqpf.liftr_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ #check @mvqpf.mem_supp /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, i, x -/ #check @mvqpf.has_good_supp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @mvqpf.liftp_iff_of_is_uniform /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, x -/ -- data/qpf/univariate/basic.lean #check @qpf.liftp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @qpf.liftp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @qpf.liftr_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ #check @qpf.mem_supp /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, x -/ #check @qpf.has_good_supp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @qpf.liftp_iff_of_is_uniform /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, x -/ -- data/rat/basic.lean #check @rat.denom_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @rat.coe_int_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ #check @rat.denom_div_cast_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ -- data/rat/order.lean #check @rat.mk_nonneg /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- data/rat/sqrt.lean #check @rat.exists_mul_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/rbmap/default.lean #check @rbmap.find_entry_correct /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, k -/ #check @rbmap.find_correct /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, k -/ #check @rbmap.constains_correct /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, k -/ -- data/rbtree/main.lean #check @rbtree.find_correct /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, a -/ #check @rbtree.find_correct_of_total /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, a -/ #check @rbtree.find_correct_exact /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, a -/ #check @rbtree.contains_correct /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, a -/ -- data/real/cau_seq_completion.lean #check @cau_seq.lim_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- data/real/ennreal.lean #check @ennreal.to_nnreal_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @ennreal.to_real_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- data/real/ereal.lean #check @ereal.eq_top_iff_forall_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @ereal.eq_bot_iff_forall_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @ereal.neg_eq_neg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- data/real/irrational.lean #check @irrational_iff_ne_rational /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @irrational_sqrt_rat_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q -/ -- data/real/nnreal.lean #check @nnreal.coe_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @nnreal.coe_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @nnreal.lt_iff_exists_rat_btwn /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- data/rel.lean #check @rel.inv_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r -/ #check @rel.mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, y, r -/ #check @rel.mem_preimage /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, x, r -/ #check @rel.mem_core /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, x, r -/ #check @rel.image_subset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, r -/ -- data/semiquot.lean #check @semiquot.mem_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, q, f -/ #check @semiquot.mem_bind /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, f, q -/ -- data/seq/computation.lean #check @computation.terminates_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @computation.terminates_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @computation.terminates_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @computation.promises_congr /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @computation.lift_rel.swap /- The following varibles are used on both sides of an equality or iff and should be made implicit: cb, ca, R -/ #check @computation.lift_eq_iff_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: c₂, c₁ -/ #check @computation.lift_rel_return_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: cb, a, R -/ #check @computation.lift_rel_return_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, ca, R -/ #check @computation.lift_rel_return /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, R -/ #check @computation.lift_rel_think_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: cb, ca, R -/ #check @computation.lift_rel_think_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: cb, ca, R -/ #check @computation.lift_rel_aux.ret_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: cb, a, R -/ #check @computation.lift_rel_aux.ret_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: ca, b, R -/ -- data/seq/wseq.lean #check @wseq.productive_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @wseq.head_terminates_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @wseq.mem_think /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, s -/ #check @wseq.mem_cons_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, s -/ #check @wseq.lift_rel_cons /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, b, a, R -/ #check @wseq.lift_rel_think_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, R -/ #check @wseq.lift_rel_think_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, R -/ #check @wseq.mem_congr /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- data/set/basic.lean #check @set.nonempty_coe_sort /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @set.ne_univ_iff_exists_not_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @set.mem_union /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, x -/ #check @set.mem_inter_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, x -/ #check @set.mem_compl_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ #check @set.inter_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @set.mem_diff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @set.mem_powerset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, x -/ #check @set.mem_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, s, f -/ #check @set.mem_compl_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, t -/ #check @set.exists_image_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, x, f -/ #check @set.subsingleton_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @set.range_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, f -/ #check @subtype.preimage_val_eq_preimage_val_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, t, s -/ #check @subtype.exists_set_subtype /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- data/set/finite.lean #check @set.subset_iff_to_finset_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ -- data/set/function.lean #check @set.maps_image_to /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s, g, f -/ #check @set.maps_univ_to /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, f -/ #check @set.maps_range_to /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, g, f -/ #check @set.eq_on_piecewise /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @set.injective_piecewise_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- data/set/intervals/unordered_interval.lean #check @set.bdd_below_bdd_above_iff_subset_interval /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- data/set/pairwise.lean #check @symmetric.pairwise_on /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @pairwise_disjoint_on /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @set.pairwise_iff_exists_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, s -/ #check @set.pairwise_eq_iff_exists_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, s -/ #check @pairwise_subtype_iff_pairwise_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, s -/ -- data/setoid/basic.lean #check @setoid.comm' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @setoid.injective_iff_ker_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @setoid.comap_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, r, f -/ #check @quot.subsingleton_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- data/setoid/partition.lean #check @setoid.rel_iff_exists_classes /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @indexed_partition.proj_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: hs -/ -- data/sym/basic.lean #check @sym.cons_inj_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: s', s -/ #check @sym.cons_inj_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: a', a -/ -- data/sym/sym2.lean #check @sym2.is_diag_iff_proj_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ #check @sym2.is_diag_iff_mem_range_diag /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ #check @sym2.to_rel_prop /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, s -/ #check @sym2.rel_bool_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- data/vector3.lean #check @exists_vector_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @exists_vector_succ /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @vector_ex_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @vector_all_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @vector_allp_cons /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, x, p -/ #check @vector_allp_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, p -/ -- data/zmod/basic.lean #check @zmod.int_coe_eq_int_coe_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @zmod.int_coe_eq_int_coe_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @zmod.nat_coe_eq_nat_coe_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @zmod.nat_coe_eq_nat_coe_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b, a -/ #check @zmod.int_coe_zmod_eq_zero_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @zmod.nat_coe_zmod_eq_zero_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @zmod.eq_iff_modeq_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @zmod.le_div_two_iff_lt_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: n -/ #check @zmod.val_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @zmod.val_min_abs_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- deprecated/subgroup.lean #check @is_add_group_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @is_group_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @is_group_hom.one_iff_ker_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_add_group_hom.zero_iff_ker_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_add_group_hom.zero_iff_ker_neg' /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_group_hom.one_iff_ker_inv' /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_group_hom.inv_iff_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_add_group_hom.neg_iff_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_group_hom.inv_iff_ker' /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @is_add_group_hom.neg_iff_ker' /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- dynamics/circle/rotation_number/translation_number.lean #check @circle_deg1_lift.strict_mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.continuous_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.iterate_pos_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.iterate_pos_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.iterate_pos_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.le_iterate_pos_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.lt_iterate_pos_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.translation_number_eq_int_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @circle_deg1_lift.translation_number_eq_rat_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- dynamics/flow.lean #check @is_invariant_iff_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, ϕ -/ #check @flow.is_invariant_iff_image_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, ϕ -/ -- dynamics/minimal.lean #check @is_minimal_iff_closed_vadd_invariant /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @is_minimal_iff_closed_smul_invariant /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ -- dynamics/omega_limit.lean #check @mem_omega_limit_iff_frequently /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, s, ϕ, f -/ #check @mem_omega_limit_iff_frequently₂ /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, s, ϕ, f -/ #check @mem_omega_limit_singleton_iff_map_cluster_point /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, ϕ, f -/ -- field_theory/adjoin.lean #check @intermediate_field.adjoin_subset_adjoin_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @intermediate_field.adjoin_simple.is_integral_gen /- The following varibles are used on both sides of an equality or iff and should be made implicit: α, F -/ -- field_theory/finite/basic.lean #check @finite_field.forall_pow_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, K -/ -- field_theory/finite/polynomial.lean #check @mv_polynomial.C_dvd_iff_zmod /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ, n -/ -- field_theory/galois.lean #check @intermediate_field.le_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: K, H -/ -- field_theory/intermediate_field.lean #check @intermediate_field.mem_mk /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ #check @intermediate_field.mem_to_subalgebra /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ #check @intermediate_field.mem_to_subfield /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ #check @intermediate_field.coe_is_integral_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- field_theory/is_alg_closed/basic.lean #check @is_alg_closure_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: K, k -/ -- field_theory/perfect_closure.lean #check @perfect_closure.r_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, ᾰ, p, K -/ #check @perfect_closure.eq_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, p, K -/ #check @perfect_closure.nat_cast_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, K -/ #check @perfect_closure.eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, p, K -/ -- field_theory/ratfunc.lean #check @ratfunc.algebra_map_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ -- field_theory/separable.lean #check @polynomial.separable_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @polynomial.separable_def' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @polynomial.separable_C /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- field_theory/splitting_field.lean #check @polynomial.splits_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: j, i -/ #check @polynomial.splits_id_iff_splits /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ #check @polynomial.splits_mul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ #check @polynomial.splits_prod_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ #check @polynomial.splits_iff_exists_multiset /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ -- field_theory/subfield.lean #check @subfield.mem_to_subring /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ -- geometry/euclidean/basic.lean #check @inner_product_geometry.inner_eq_zero_iff_angle_eq_pi_div_two /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @inner_product_geometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @euclidean_geometry.dist_smul_vadd_eq_dist /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, p₂, p₁ -/ #check @euclidean_geometry.reflection_eq_self_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @euclidean_geometry.reflection_eq_iff_orthogonal_projection_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, s₂, s₁ -/ #check @euclidean_geometry.cospherical_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: ps -/ -- geometry/euclidean/circumcenter.lean #check @euclidean_geometry.dist_eq_iff_dist_orthogonal_projection_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p3 -/ #check @euclidean_geometry.dist_set_eq_iff_dist_orthogonal_projection_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @euclidean_geometry.exists_dist_eq_iff_exists_dist_orthogonal_projection_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- geometry/euclidean/monge_point.lean #check @affine.simplex.affine_span_insert_singleton_eq_altitude_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, s -/ -- geometry/euclidean/triangle.lean #check @inner_product_geometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @inner_product_geometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two /- The following varibles are used on both sides of an equality or iff and should be made implicit: p3, p2, p1 -/ -- geometry/manifold/basic_smooth_bundle.lean #check @basic_smooth_bundle_core.mem_atlas_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, Z -/ #check @basic_smooth_bundle_core.mem_chart_source_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p, Z -/ #check @basic_smooth_bundle_core.mem_chart_target_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p, Z -/ -- geometry/manifold/charted_space.lean #check @closed_under_restriction_iff_id_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ -- geometry/manifold/diffeomorph.lean #check @diffeomorph.times_cont_mdiff_within_at_comp_diffeomorph_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ #check @diffeomorph.times_cont_mdiff_on_comp_diffeomorph_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ #check @diffeomorph.times_cont_mdiff_at_comp_diffeomorph_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ -- geometry/manifold/mfderiv.lean #check @filter.eventually_eq.mdifferentiable_within_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I', I -/ -- group_theory/commuting_probability.lean #check @comm_prob_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ -- group_theory/congruence.lean #check @add_con.eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @con.eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @add_con.ker_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @con.ker_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- group_theory/coset.lean #check @mem_left_coset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mem_left_add_coset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mem_right_add_coset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @mem_right_coset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @normal_iff_eq_cosets /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @normal_iff_eq_add_cosets /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @left_coset_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @left_add_coset_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @right_add_coset_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @right_coset_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- group_theory/finiteness.lean #check @add_submonoid.fg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @submonoid.fg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @submonoid.fg_iff_add_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @add_submonoid.fg_iff_mul_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @monoid.fg_iff_submonoid_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @add_monoid.fg_iff_add_submonoid_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @add_subgroup.fg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @subgroup.fg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @add_subgroup.fg_iff_add_submonoid.fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @subgroup.fg_iff_submonoid_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @subgroup.fg_iff_add_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @add_subgroup.fg_iff_mul_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ -- group_theory/free_abelian_group_finsupp.lean #check @free_abelian_group.mem_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, x -/ #check @free_abelian_group.not_mem_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, x -/ -- group_theory/free_product.lean #check @free_product.word.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @free_product.word.pair.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- group_theory/general_commutator.lean #check @general_commutator_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: K, H₂, H₁ -/ -- group_theory/group_action/basic.lean #check @add_action.mem_fixed_points /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @mul_action.mem_fixed_points /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @add_action.mem_fixed_by /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @mul_action.mem_fixed_by /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @add_action.mem_fixed_points' /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @mul_action.mem_fixed_points' /- The following varibles are used on both sides of an equality or iff and should be made implicit: β -/ #check @mul_action.mem_stabilizer_submonoid_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @add_action.mem_stabilizer_add_submonoid_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- group_theory/group_action/conj_act.lean #check @conj_act.forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- group_theory/group_action/group.lean #check @vadd_eq_iff_eq_neg_vadd /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @smul_eq_iff_eq_inv_smul /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ -- group_theory/group_action/sub_mul_action.lean #check @sub_mul_action.smul_mem_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @sub_mul_action.neg_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @sub_mul_action.smul_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- group_theory/monoid_localization.lean #check @submonoid.localization_map.mul_inv_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, w, y -/ #check @add_submonoid.localization_map.add_neg_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, w, y -/ #check @add_submonoid.localization_map.add_neg_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, w, y -/ #check @submonoid.localization_map.mul_inv_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, w, y -/ #check @submonoid.localization_map.eq_mk'_iff_mul_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_submonoid.localization_map.eq_mk'_iff_add_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submonoid.localization_map.mk'_eq_iff_eq_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_submonoid.localization_map.mk'_eq_iff_eq_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_submonoid.localization_map.mk'_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submonoid.localization_map.mk'_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_submonoid.localization_map.lift_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, z, f -/ #check @submonoid.localization_map.lift_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, z, f -/ #check @add_submonoid.localization_map.lift_spec_add /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, w, z, f -/ #check @submonoid.localization_map.lift_spec_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, w, z, f -/ #check @submonoid.localization_map.lift_mk'_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, v, x -/ #check @add_submonoid.localization_map.lift_mk'_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, v, x -/ #check @add_submonoid.localization_map.lift_injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submonoid.localization_map.lift_injective_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submonoid.localization_map.map_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, z, f -/ #check @add_submonoid.localization_map.map_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, z, f -/ #check @submonoid.localization_map.of_mul_equiv_of_localizations_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_submonoid.localization_map.of_add_equiv_of_localizations_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- group_theory/nilpotent.lean #check @mem_upper_central_series_step /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, H -/ #check @mem_upper_central_series_succ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n, G -/ #check @nilpotent_iff_finite_ascending_central_series /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @nilpotent_iff_finite_descending_central_series /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @mem_lower_central_series_succ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, n -/ -- group_theory/order_of_element.lean #check @is_periodic_pt_mul_iff_pow_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_periodic_pt_add_iff_nsmul_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_of_fin_add_order_iff_nsmul_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_of_fin_order_iff_pow_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @mem_multiples_iff_mem_range_add_order_of' /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @mem_powers_iff_mem_range_order_of' /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- group_theory/perm/basic.lean #check @equiv.perm.mem_iff_of_subtype_apply_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- group_theory/perm/cycle_type.lean #check @equiv.perm.vectors_prod_eq_one.mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, G -/ -- group_theory/perm/cycles.lean #check @equiv.perm.same_cycle_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @equiv.perm.cycle_of_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- group_theory/perm/list.lean #check @list.form_perm_eq_head_iff_eq_last /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, l -/ #check @list.form_perm_apply_mem_eq_self_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @list.form_perm_apply_mem_ne_self_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @list.form_perm_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ -- group_theory/perm/sign.lean #check @equiv.perm.perm_maps_to_inl_iff_maps_to_inr /- The following varibles are used on both sides of an equality or iff and should be made implicit: σ -/ -- group_theory/perm/support.lean #check @equiv.perm.support_swap_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- group_theory/quotient_group.lean #check @quotient_group.eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @quotient_add_group.eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- group_theory/semidirect_product.lean #check @semidirect_product.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- group_theory/solvable.lean #check @is_solvable_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ -- group_theory/subgroup/basic.lean #check @add_subgroup.mem_to_add_submonoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, K -/ #check @subgroup.mem_to_submonoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, K -/ #check @subgroup.inv_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.neg_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.div_mem_comm_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.sub_mem_comm_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.exists_neg_mem_iff_exists_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @subgroup.exists_inv_mem_iff_exists_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @subgroup.mul_mem_cancel_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.add_mem_cancel_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.add_mem_cancel_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.mul_mem_cancel_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.eq_bot_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.eq_bot_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.nontrivial_iff_exists_ne_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.nontrivial_iff_exists_ne_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.card_le_one_iff_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.card_nonpos_iff_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.one_lt_card_iff_ne_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.pos_card_iff_ne_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.closure_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @subgroup.closure_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @add_subgroup.closure_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, G -/ #check @subgroup.closure_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, G -/ #check @add_monoid_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_monoid_hom.eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_monoid_hom.ker_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.ker_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @add_subgroup.map_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.map_eq_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @add_subgroup.map_eq_bot_iff_of_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @subgroup.map_eq_bot_iff_of_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ -- group_theory/subgroup/pointwise.lean #check @subgroup.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, a, m -/ #check @subgroup.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subgroup.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_subgroup.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, a, m -/ #check @add_subgroup.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_subgroup.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ -- group_theory/submonoid/basic.lean #check @add_submonoid.closure_singleton_le_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, m -/ #check @submonoid.closure_singleton_le_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, m -/ #check @add_submonoid.mem_supr /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submonoid.mem_supr /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @is_add_unit.mem_add_submonoid_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @is_unit.mem_submonoid_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- group_theory/submonoid/center.lean #check @set.mem_center_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @set.mem_add_center /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ -- group_theory/submonoid/inverses.lean #check @submonoid.from_left_inv_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, S -/ #check @add_submonoid.from_left_neg_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a, S -/ -- group_theory/submonoid/membership.lean #check @submonoid.mem_powers_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, x -/ #check @add_submonoid.mem_multiples_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, x -/ -- group_theory/submonoid/operations.lean #check @add_monoid_hom.mem_mker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @monoid_hom.mem_mker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submonoid.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @add_submonoid.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @add_submonoid.eq_bot_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @submonoid.eq_bot_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @add_submonoid.nontrivial_iff_exists_ne_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @submonoid.nontrivial_iff_exists_ne_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- group_theory/submonoid/pointwise.lean #check @add_submonoid.neg_le_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: T, S -/ #check @submonoid.inv_le_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: T, S -/ #check @add_submonoid.neg_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: T, S -/ #check @submonoid.inv_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: T, S -/ #check @submonoid.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, a, m -/ #check @submonoid.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @submonoid.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @submonoid.mem_closure_inv /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_closure_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, a, m -/ #check @add_submonoid.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @add_submonoid.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ -- group_theory/sylow.lean #check @subgroup.sylow_mem_fixed_points_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ -- linear_algebra/affine_space/affine_equiv.lean #check @affine_equiv.apply_eq_iff_eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- linear_algebra/affine_space/affine_map.lean #check @affine_map.linear_eq_zero_iff_exists_const /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @affine_map.injective_iff_linear_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @affine_map.surjective_iff_linear_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/affine_space/affine_subspace.lean #check @span_points_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @affine_subspace.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p, P, k -/ #check @affine_subspace.mem_direction_iff_eq_vsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @affine_subspace.vadd_mem_iff_mem_direction /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @affine_subspace.mem_direction_iff_eq_vsub_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @affine_subspace.mem_direction_iff_eq_vsub_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @affine_subspace.vsub_right_mem_direction_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: p2 -/ #check @affine_subspace.vsub_left_mem_direction_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: p2 -/ #check @affine_subspace.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s₂, s₁ -/ #check @affine_subspace.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ #check @affine_subspace.le_def' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ #check @affine_subspace.lt_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ #check @affine_subspace.not_le_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ #check @affine_subspace.lt_iff_le_and_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ #check @affine_subspace.mem_affine_span_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: p2, p1 -/ #check @affine_subspace.affine_span_eq_top_iff_vector_span_eq_top_of_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, V, k -/ #check @affine_subspace.affine_span_eq_top_iff_vector_span_eq_top_of_nontrivial /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, V, k -/ #check @affine_subspace.mem_inf_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1, p -/ #check @affine_span_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @affine_subspace.mem_affine_span_insert_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, p2 -/ -- linear_algebra/affine_space/basis.lean #check @affine_basis.is_unit_to_matrix_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- linear_algebra/affine_space/combination.lean #check @finset.eq_weighted_vsub_subset_iff_eq_weighted_vsub_subtype /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @finset.eq_affine_combination_subset_iff_eq_affine_combination_subtype /- The following varibles are used on both sides of an equality or iff and should be made implicit: V, k -/ #check @mem_vector_span_iff_eq_weighted_vsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @mem_affine_span_iff_eq_affine_combination /- The following varibles are used on both sides of an equality or iff and should be made implicit: V, k -/ #check @mem_affine_span_iff_eq_weighted_vsub_of_point_vadd /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p, V, k -/ -- linear_algebra/affine_space/finite_dimensional.lean #check @affine_independent_iff_finrank_vector_span_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_iff_le_finrank_vector_span /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_iff_not_finrank_vector_span_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @finrank_vector_span_le_iff_not_affine_independent /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @collinear_iff_dim_le_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, k -/ #check @collinear_iff_finrank_le_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, k -/ #check @collinear_iff_of_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @collinear_iff_exists_forall_eq_smul_vadd /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, k -/ #check @affine_independent_iff_not_collinear /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @collinear_iff_not_affine_independent /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ -- linear_algebra/affine_space/independent.lean #check @affine_independent_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_iff_of_fintype /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_iff_linear_independent_vsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_set_iff_linear_independent_vsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @linear_independent_set_iff_affine_independent_vadd_union_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @affine_independent_iff_indicator_eq_of_affine_combination_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent_iff_eq_of_fintype_affine_combination_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, k -/ #check @affine_independent.mem_affine_span_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, i -/ #check @affine.simplex.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s2, s1 -/ -- linear_algebra/alternating.lean #check @alternating_map.comp_linear_map_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: g₂, g₁ -/ #check @alternating_map.comp_linear_equiv_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/basic.lean #check @submodule.comap_le_comap_iff_of_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @submodule.map_le_map_iff_of_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @submodule.map_span_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: N, s, f -/ #check @linear_map.map_span_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: N, s, f -/ #check @submodule.mem_supr_of_directed /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @submodule.mem_supr_of_chain /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, a -/ #check @submodule.span_singleton_eq_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @submodule.span_singleton_le_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, m -/ #check @submodule.mem_supr /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @linear_map.range_le_bot_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @linear_map.map_le_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @submodule.mem_map_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- linear_algebra/bilinear_form.lean #check @bilin_form.comp_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: B₂, B₁ -/ #check @bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f, F -/ #check @bilin_form.mem_is_pair_self_adjoint_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, F₂, B₂ -/ #check @bilin_form.is_pair_self_adjoint_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, F₃, B₃ -/ #check @bilin_form.is_skew_adjoint_iff_neg_self_adjoint /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, B₁ -/ #check @bilin_form.mem_self_adjoint_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, B₂ -/ #check @bilin_form.mem_skew_adjoint_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, B₃ -/ #check @is_adjoint_pair_to_bilin' /- The following varibles are used on both sides of an equality or iff and should be made implicit: A', A, J₃, J -/ #check @is_adjoint_pair_to_bilin /- The following varibles are used on both sides of an equality or iff and should be made implicit: A', A, J₃, J -/ #check @matrix.is_adjoint_pair_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, A', A, J -/ #check @mem_pair_self_adjoint_matrices_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, J₃, J -/ #check @mem_self_adjoint_matrices_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, J -/ #check @mem_skew_adjoint_matrices_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, J -/ #check @bilin_form.is_Ortho.nondegenerate_iff_not_is_ortho_basis_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: B -/ #check @bilin_form.is_adjoint_pair_iff_eq_of_nondegenerate /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ, ψ, B -/ -- linear_algebra/clifford_algebra/basic.lean #check @clifford_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- linear_algebra/determinant.lean #check @alternating_map.map_basis_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @alternating_map.map_basis_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/dfinsupp.lean #check @submodule.mem_supr_iff_exists_dfinsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @submodule.mem_supr_iff_exists_dfinsupp' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @submodule.mem_bsupr_iff_exists_dfinsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S, p -/ #check @complete_lattice.independent_iff_forall_dfinsupp /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @complete_lattice.independent_iff_dfinsupp_lsum_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @complete_lattice.independent_iff_dfinsupp_sum_add_hom_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- linear_algebra/dimension.lean #check @dim_submodule_le_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @dim_submodule_le_one_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- linear_algebra/dual.lean #check @submodule.mem_dual_annihilator /- The following varibles are used on both sides of an equality or iff and should be made implicit: φ -/ #check @submodule.mem_dual_annihilator_comap_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- linear_algebra/eigenspace.lean #check @module.End.mem_generalized_eigenspace /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, k, μ, f -/ #check @module.End.mem_maximal_generalized_eigenspace /- The following varibles are used on both sides of an equality or iff and should be made implicit: m, μ, f -/ -- linear_algebra/exterior_algebra/basic.lean #check @exterior_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f, R -/ #check @exterior_algebra.algebra_map_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @exterior_algebra.algebra_map_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @exterior_algebra.algebra_map_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @exterior_algebra.ι_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @exterior_algebra.ι_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @exterior_algebra.ι_eq_algebra_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, x -/ -- linear_algebra/finite_dimensional.lean #check @submodule.fg_iff_finite_dimensional /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @linear_map.is_unit_iff_ker_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @linear_map.is_unit_iff_range_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/finsupp.lean #check @finsupp.mem_supported /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @finsupp.mem_supported' /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @finsupp.mem_span_iff_total /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s, R -/ #check @finsupp.mem_span_image_iff_total /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- linear_algebra/free_module/basic.lean #check @module.free_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, R -/ #check @module.free_iff_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: M, R -/ -- linear_algebra/general_linear_group.lean #check @matrix.general_linear_group.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ #check @matrix.mem_GL_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- linear_algebra/invariant_basis_number.lean #check @strong_rank_condition_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @strong_rank_condition_iff_succ /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- linear_algebra/linear_independent.lean #check @linear_independent_unique_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ -- linear_algebra/matrix/is_diag.lean #check @matrix.is_diag_iff_exists_diagonal /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- linear_algebra/matrix/nonsingular_inverse.lean #check @matrix.is_unit_iff_is_unit_det /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- linear_algebra/matrix/orthogonal.lean #check @matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ -- linear_algebra/multilinear/basic.lean #check @multilinear_map.comp_linear_map_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: g₂, g₁ -/ #check @multilinear_map.comp_linear_equiv_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @multilinear_map.dom_dom_congr_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- linear_algebra/orientation.lean #check @equiv_iff_same_ray /- The following varibles are used on both sides of an equality or iff and should be made implicit: v₂, v₁ -/ #check @ray_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @ray_vector.equiv_neg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v₂, v₁, R -/ #check @same_ray_smul_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @same_ray_smul_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @same_ray_neg_smul_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @same_ray_neg_smul_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @basis.orientation_eq_iff_det_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: e₂, e₁ -/ #check @basis.orientation_ne_iff_eq_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, e -/ #check @basis.orientation_comp_linear_equiv_eq_iff_det_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @basis.orientation_comp_linear_equiv_eq_neg_iff_det_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @same_ray_iff_mem_orbit /- The following varibles are used on both sides of an equality or iff and should be made implicit: v₂, v₁, R -/ #check @orientation.ne_iff_eq_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: x₂, x₁ -/ #check @orientation.map_eq_iff_det_pos /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @orientation.map_eq_neg_iff_det_neg /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/pi.lean #check @linear_map.pi_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- linear_algebra/projection.lean #check @submodule.prod_equiv_of_is_compl_symm_apply_fst_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: q -/ #check @submodule.prod_equiv_of_is_compl_symm_apply_snd_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- linear_algebra/quadratic_form/basic.lean #check @quadratic_form.not_anisotropic_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: Q -/ -- linear_algebra/quotient.lean #check @submodule.quotient.eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.quotient.mk_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @submodule.map_mkq_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: p', p -/ -- linear_algebra/special_linear_group.lean #check @matrix.special_linear_group.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ -- linear_algebra/tensor_algebra/basic.lean #check @tensor_algebra.lift_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @tensor_algebra.algebra_map_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @tensor_algebra.algebra_map_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @tensor_algebra.algebra_map_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @tensor_algebra.ι_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @tensor_algebra.ι_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @tensor_algebra.ι_eq_algebra_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, x -/ -- linear_algebra/unitary_group.lean #check @matrix.unitary_group.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A -/ -- logic/basic.lean #check @and_and_and_comm /- The following varibles are used on both sides of an equality or iff and should be made implicit: d, c, b, a -/ #check @not_xor /- The following varibles are used on both sides of an equality or iff and should be made implicit: Q, P -/ #check @xor_iff_not_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: Q, P -/ #check @exists_true_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @forall_true_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- logic/embedding.lean #check @function.embedding.apply_eq_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- logic/function/basic.lean #check @function.injective.of_comp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @function.injective.of_comp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @function.surjective.of_comp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @function.surjective.of_comp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @function.bijective_iff_exists_unique /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @function.bijective.of_comp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @function.bijective.of_comp_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ #check @function.forall_update_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f -/ #check @function.exists_update_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f -/ #check @eq_rec_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- logic/nontrivial.lean #check @subtype.nontrivial_iff_exists_ne /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- logic/relation.lean #check @symmetric.iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @relation.refl_trans_gen.cases_tail_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, a, r -/ #check @relation.refl_gen_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, a, r -/ #check @relation.trans_gen_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: ᾰ, a, r -/ -- logic/unique.lean #check @unique.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- measure_theory/covering/vitali_family.lean #check @vitali_family.mem_filter_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @vitali_family.eventually_filter_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ #check @vitali_family.frequently_filter_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: v -/ -- measure_theory/decomposition/jordan.lean #check @measure_theory.jordan_decomposition.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @measure_theory.signed_measure.absolutely_continuous_ennreal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ #check @measure_theory.signed_measure.total_variation_absolutely_continuous_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ #check @measure_theory.signed_measure.mutually_singular_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @measure_theory.signed_measure.mutually_singular_ennreal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ #check @measure_theory.signed_measure.total_variation_mutually_singular_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ -- measure_theory/decomposition/lebesgue.lean #check @measure_theory.signed_measure.not_have_lebesgue_decomposition_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ -- measure_theory/decomposition/radon_nikodym.lean #check @measure_theory.signed_measure.absolutely_continuous_iff_with_densityᵥ_rn_deriv_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, s -/ -- measure_theory/function/ae_eq_of_integral.lean #check @measure_theory.ae_const_le_iff_forall_lt_measure_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, f -/ -- measure_theory/function/l1_space.lean #check @measure_theory.has_finite_integral_iff_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @measure_theory.has_finite_integral_iff_edist /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @measure_theory.has_finite_integral_norm_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @measure_theory.has_finite_integral_smul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @measure_theory.integrable_map_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @measure_theory.integrable_smul_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @measure_theory.integrable.to_L1_eq_to_L1_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ -- measure_theory/function/lp_order.lean #check @measure_theory.Lp.coe_fn_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @measure_theory.Lp.coe_fn_nonneg /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- measure_theory/function/lp_space.lean #check @measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f_lim, f -/ #check @measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp /- The following varibles are used on both sides of an equality or iff and should be made implicit: f_lim, f -/ #check @measure_theory.Lp.tendsto_Lp_iff_tendsto_ℒp'' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f_lim, f -/ #check @measure_theory.Lp.cauchy_seq_Lp_iff_cauchy_seq_ℒp /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- measure_theory/function/simple_func_dense.lean #check @measure_theory.Lp.simple_func.coe_fn_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @measure_theory.Lp.simple_func.coe_fn_nonneg /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- measure_theory/function/strongly_measurable.lean #check @measure_theory.ae_fin_strongly_measurable_iff_ae_measurable /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ -/ -- measure_theory/integral/integrable_on.lean #check @measure_theory.integrable_on_map_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- measure_theory/integral/lebesgue.lean #check @measure_theory.simple_func.preimage_eq_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, f -/ -- measure_theory/measurable_space.lean #check @measurable_set.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, a -/ -- measure_theory/measurable_space_def.lean #check @measurable_space.generate_from_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ -- measure_theory/measure/complex.lean #check @measure_theory.complex_measure.absolutely_continuous_ennreal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ, c -/ -- measure_theory/measure/content.lean #check @measure_theory.content.outer_measure_caratheodory /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, μ -/ -- measure_theory/measure/measure_space.lean #check @measure_theory.sub_ae_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: g, f -/ #check @measure_theory.spanning_sets_index_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ -/ #check @measurable_equiv.map_apply_eq_iff_map_symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @ae_measurable_map_equiv_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- measure_theory/measure/outer_measure.lean #check @measure_theory.outer_measure.Union_null_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.bUnion_null_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.sUnion_null_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.univ_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.is_caratheodory_iff_le' /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.is_caratheodory_compl_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.is_caratheodory_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.outer_measure.is_caratheodory_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: m -/ #check @measure_theory.induced_outer_measure_caratheodory /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- measure_theory/measure/vector_measure.lean #check @measure_theory.vector_measure.ext_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ #check @measure_theory.vector_measure.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ #check @measure_theory.vector_measure.restrict_le_restrict_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ #check @measure_theory.vector_measure.le_restrict_univ_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ #check @measure_theory.vector_measure.neg_le_neg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: w, v -/ -- measure_theory/pi_system.lean #check @measurable_space.dynkin_system.has_compl_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: d -/ -- measure_theory/probability_mass_function/basic.lean #check @pmf.mem_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, p -/ #check @pmf.apply_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, p -/ #check @pmf.mem_support_pure_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a', a -/ #check @pmf.mem_support_bind_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, f, p -/ #check @pmf.to_outer_measure_apply_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p -/ -- measure_theory/probability_mass_function/constructions.lean #check @pmf.mem_support_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, p, f -/ #check @pmf.mem_support_seq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, p, q -/ #check @pmf.mem_support_of_finset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_of_fintype_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_of_multiset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_uniform_of_finset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_normalize_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_filter_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.filter_apply_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.filter_apply_ne_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @pmf.mem_support_bernoulli_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @pmf.mem_support_bind_on_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, f -/ #check @pmf.bind_on_support_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, f -/ -- model_theory/basic.lean #check @first_order.language.embedding.map_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, r -/ #check @first_order.language.equiv.map_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, r -/ -- number_theory/ADE_inequality.lean #check @ADE_inequality.classification /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, q, p -/ -- number_theory/class_number/finite.lean #check @class_group.mem_finset_approx /- The following varibles are used on both sides of an equality or iff and should be made implicit: adm, bS -/ -- number_theory/class_number/function_field.lean #check @function_field.class_number_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F, Fq -/ -- number_theory/cyclotomic/basic.lean #check @is_cyclotomic_extension_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A, S -/ #check @is_cyclotomic_extension.iff_adjoin_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A, S -/ #check @is_cyclotomic_extension.iff_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: B, A, n -/ -- number_theory/dioph.lean #check @int.eq_nat_abs_iff_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @list_all_cons /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, x, p -/ #check @list_all_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, p -/ #check @list_all_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @poly.sumsq_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, x -/ #check @dioph.inject_dummies_lem /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, p -/ #check @dioph.dioph_fn_vec /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @dioph.dioph_pfun_vec /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- number_theory/divisors.lean #check @nat.mem_divisors_prime_pow /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @nat.mem_proper_divisors_prime_pow /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ -- number_theory/function_field.lean #check @function_field_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- number_theory/lucas_lehmer.lean #check @lucas_lehmer.residue_eq_zero_iff_s_mod_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- number_theory/number_field.lean #check @number_field.mem_ring_of_integers /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, K -/ -- number_theory/padics/padic_integers.lean #check @padic_int.coe_int_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: z2, z1 -/ #check @padic_int.norm_int_lt_one_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @padic_int.norm_le_pow_iff_le_valuation /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic_int.mem_span_pow_iff_le_valuation /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic_int.norm_le_pow_iff_mem_span_pow /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic_int.norm_le_pow_iff_norm_lt_pow_add_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic_int.norm_lt_pow_iff_norm_le_pow_sub_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic_int.norm_lt_one_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @padic_int.pow_p_dvd_int_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, n -/ -- number_theory/padics/padic_norm.lean #check @padic_val_rat.padic_val_rat_le_padic_val_rat_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- number_theory/padics/padic_numbers.lean #check @padic_seq.norm_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @padic_seq.eq_zero_iff_equiv_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @padic_seq.ne_zero_iff_nequiv_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @padic.mk_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @padic_norm_e.zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: q -/ #check @padic_norm_e.norm_int_lt_one_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ #check @padic_norm_e.norm_int_le_pow_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, k -/ #check @padic.norm_le_pow_iff_norm_lt_pow_add_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ #check @padic.norm_lt_pow_iff_norm_le_pow_sub_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, x -/ -- number_theory/pell.lean #check @pell.is_pell_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: a1 -/ #check @pell.is_pell_norm /- The following varibles are used on both sides of an equality or iff and should be made implicit: a1 -/ #check @pell.is_pell_conj /- The following varibles are used on both sides of an equality or iff and should be made implicit: a1 -/ #check @pell.y_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, m -/ -- number_theory/quadratic_reciprocity.lean #check @zmod.euler_criterion_units /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @zmod.euler_criterion /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @zmod.legendre_sym_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, a -/ #check @zmod.legendre_sym_eq_one_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @zmod.exists_sq_eq_two_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @zmod.exists_sq_eq_prime_iff_of_mod_four_eq_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @zmod.exists_sq_eq_prime_iff_of_mod_four_eq_three /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ -- number_theory/zsqrtd/basic.lean #check @zsqrtd.coe_int_dvd_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, z -/ #check @zsqrtd.is_unit_iff_norm_is_unit /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ #check @zsqrtd.norm_eq_one_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ #check @zsqrtd.norm_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ #check @zsqrtd.norm_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- number_theory/zsqrtd/gaussian_int.lean #check @gaussian_int.prime_iff_mod_four_eq_three_of_nat_prime /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- order/atoms.lean #check @order_iso.is_atom_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @order_iso.is_coatom_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- order/basic.lean #check @has_le.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- order/bounds.lean #check @is_lub_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @is_glb_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @order_iso.is_lub_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @order_iso.is_glb_image /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @order_iso.is_lub_preimage /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @order_iso.is_glb_preimage /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- order/closure.lean #check @closure_operator.le_closure_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, c -/ #check @closure_operator.mem_closed_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, c -/ #check @closure_operator.mem_closed_iff_closure_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, c -/ #check @closure_operator.closure_le_closed_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @lower_adjoint.le_closure_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, l -/ #check @lower_adjoint.mem_closed_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, l -/ #check @lower_adjoint.mem_closed_iff_closure_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, l -/ #check @lower_adjoint.closure_le_closed_iff_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @lower_adjoint.le_iff_subset /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, s -/ #check @lower_adjoint.mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s -/ -- order/compactly_generated.lean #check @complete_lattice.is_compact_element_iff_le_of_directed_Sup_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, α -/ #check @complete_lattice.is_Sup_finite_compact_iff_all_elements_compact /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @complete_lattice.well_founded_iff_is_Sup_finite_compact /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @complete_lattice.is_sup_closed_compact_iff_well_founded /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- order/compare.lean #check @ordering.compares_iff_of_compares_impl /- The following varibles are used on both sides of an equality or iff and should be made implicit: o -/ #check @ordering.or_else_eq_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: o₂, o₁ -/ #check @cmp_eq_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @cmp_eq_eq_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @cmp_eq_gt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- order/complete_lattice.lean #check @supr_eq_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @infi_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @unary_relation_Sup_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @binary_relation_Sup_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @complete_lattice.set_independent_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- order/filter/at_top_bot.lean #check @filter.tendsto_const_mul_pow_at_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, c -/ #check @filter.tendsto_neg_const_mul_pow_at_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, c -/ -- order/filter/bases.lean #check @filter_basis.mem_filter_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B -/ -- order/filter/basic.lean #check @filter.bInter_finset_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: is -/ #check @finset.Inter_mem_sets /- The following varibles are used on both sides of an equality or iff and should be made implicit: is -/ #check @filter.mem_infi_of_fintype /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.mem_infi_of_directed /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.mem_infi_finite /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.mem_infi_finite' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.eventually_all_finset /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @finset.eventually_all /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @filter.frequently_true_iff_ne_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @filter.mem_traverse_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, fs -/ -- order/filter/partial.lean #check @filter.mem_rmap /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, l, r -/ #check @filter.rtendsto_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, r -/ #check @filter.rtendsto_iff_le_rcomap /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, r -/ #check @filter.mem_rcomap' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, l, r -/ #check @filter.rtendsto'_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, r -/ #check @filter.tendsto_iff_rtendsto /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, l₂, l₁ -/ #check @filter.tendsto_iff_rtendsto' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, l₂, l₁ -/ #check @filter.mem_pmap /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, l, f -/ #check @filter.ptendsto_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, f -/ #check @filter.ptendsto_iff_rtendsto /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, l₂, l₁ -/ #check @filter.tendsto_iff_ptendsto /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, s, l₂, l₁ -/ #check @filter.tendsto_iff_ptendsto_univ /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, l₂, l₁ -/ #check @filter.ptendsto'_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, f -/ -- order/filter/pointwise.lean #check @filter.mem_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.mem_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- order/filter/ultrafilter.lean #check @ultrafilter.diff_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ultrafilter.mem_comap /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ #check @filter.tendsto_iff_ultrafilter /- The following varibles are used on both sides of an equality or iff and should be made implicit: l₂, l₁, f -/ -- order/fixed_points.lean #check @order_hom.next_fixed_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @order_hom.le_prev_fixed_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- order/galois_connection.lean #check @galois_connection.exists_eq_u /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @galois_connection.exists_eq_l /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ -- order/hom/basic.lean #check @order_iso.apply_eq_iff_eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, e -/ #check @order_iso.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @order_iso.le_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @order_iso.symm_apply_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- order/hom/lattice.lean #check @order_hom.iterate_sup_le_sup_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- order/ideal.lean #check @order.is_ideal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @order.ideal.is_proper_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @order.ideal.is_maximal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- order/jordan_holder.lean #check @composition_series.inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- order/lexicographic.lean #check @prod.lex.le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @prod.lex.lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- order/liminf_limsup.lean #check @filter.is_bounded_principal /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @filter.is_cobounded_principal /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- order/omega_complete_partial_order.lean #check @omega_complete_partial_order.chain.mem_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ #check @omega_complete_partial_order.ωSup_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, c -/ #check @part.mem_ωSup /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, x -/ #check @omega_complete_partial_order.continuous_hom.forall_forall_merge /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, c₁, c₀ -/ #check @omega_complete_partial_order.continuous_hom.forall_forall_merge' /- The following varibles are used on both sides of an equality or iff and should be made implicit: z, c₁, c₀ -/ -- order/order_iso_nat.lean #check @well_founded.monotone_chain_condition /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- order/pfilter.lean #check @order.pfilter.mem_coe /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- order/prime_ideal.lean #check @order.ideal.is_prime_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @order.pfilter.is_prime_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- order/rel_classes.lean #check @comm_of /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @not_bounded_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @not_unbounded_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- order/rel_iso.lean #check @rel_iso.rel_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @rel_iso.symm_apply_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @subrel_val /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, r -/ -- order/succ_pred.lean #check @succ_order.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @pred_order.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- order/symm_diff.lean #check @symm_diff_eq_sup /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @symm_diff_right_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, b -/ #check @symm_diff_left_inj /- The following varibles are used on both sides of an equality or iff and should be made implicit: c, a -/ #check @symm_diff_eq_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: b -/ #check @symm_diff_eq_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @symm_diff_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @symm_diff_eq_top_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- order/well_founded.lean #check @well_founded.lt_succ_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y -/ -- order/well_founded_set.lean #check @set.partially_well_ordered_on.iff_forall_not_is_bad_seq /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, r -/ -- probability_theory/independence.lean #check @probability_theory.indep_set_iff_indep_sets_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ -/ #check @probability_theory.indep_set_iff_measure_inter_eq_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: μ -/ -- probability_theory/stopping.lean #check @measure_theory.is_stopping_time.measurable_set /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- ring_theory/adjoin/basic.lean #check @algebra.adjoin_to_submodule_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- ring_theory/adjoin/fg.lean #check @subalgebra.fg_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- ring_theory/algebraic.lean #check @subalgebra.is_algebraic_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @is_algebraic_iff_is_integral /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @is_algebraic_iff_is_integral' /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ -- ring_theory/algebraic_independent.lean #check @algebraic_independent_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, R -/ #check @algebraic_independent.option_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- ring_theory/coprime/basic.lean #check @is_coprime.neg_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @is_coprime.neg_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @is_coprime.neg_neg_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- ring_theory/dedekind_domain.lean #check @is_dedekind_domain_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @fractional_ideal.mul_inv_cancel_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @fractional_ideal.mul_inv_cancel_iff_is_unit /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @fractional_ideal.invertible_iff_generator_nonzero /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, K -/ -- ring_theory/discrete_valuation_ring.lean #check @discrete_valuation_ring.irreducible_iff_uniformizer /- The following varibles are used on both sides of an equality or iff and should be made implicit: ϖ -/ #check @discrete_valuation_ring.iff_pid_with_one_nonzero_prime /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- ring_theory/fractional_ideal.lean #check @fractional_ideal.coe_ideal_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @fractional_ideal.mem_canonical_equiv_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: P', P, S -/ #check @fractional_ideal.is_principal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/graded_algebra/basic.lean #check @graded_algebra.mem_support_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: i, r, 𝒜 -/ -- ring_theory/hahn_series.lean #check @hahn_series.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @hahn_series.mem_support /- The following varibles are used on both sides of an equality or iff and should be made implicit: a, x -/ -- ring_theory/ideal/basic.lean #check @ideal.eq_top_iff_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.ne_top_iff_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.unit_mul_mem_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.span_eq_top_iff_finite /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @ideal.mem_pi /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, ι, I -/ #check @ideal.mul_unit_mem_iff_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.neg_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.add_mem_iff_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.add_mem_iff_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/ideal/local_ring.lean #check @local_ring.mem_maximal_ideal /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_unit_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- ring_theory/ideal/operations.lean #check @submodule.mem_annihilator_span /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, s -/ #check @submodule.mem_annihilator_span_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: r, g -/ #check @ideal.eq_span_singleton_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I -/ #check @ideal.span_singleton_mul_eq_span_singleton_mul /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I -/ #check @ideal.is_prime.multiset_prod_map_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ideal.mem_map_iff_of_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ideal.comap_le_iff_le_map /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ring_hom.mem_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ring_hom.injective_iff_ker_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ring_hom.ker_eq_bot_iff_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ideal.map_eq_bot_iff_le_ker /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ideal.map_eq_iff_sup_ker_eq_of_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ideal.bot_quotient_is_maximal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/ideal/prod.lean #check @ideal.mem_prod /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, I -/ #check @ideal.ideal_prod_prime /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/ideal/quotient.lean #check @ideal.quotient.is_domain_iff_prime /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @ideal.quotient.maximal_ideal_iff_is_field_quotient /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/int/basic.lean #check @int.nonneg_iff_normalize_eq_self /- The following varibles are used on both sides of an equality or iff and should be made implicit: z -/ -- ring_theory/integral_closure.lean #check @mem_integral_closure_iff_mem_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, R -/ #check @is_integral_quotient_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- ring_theory/jacobson.lean #check @ideal.disjoint_powers_iff_not_mem /- The following varibles are used on both sides of an equality or iff and should be made implicit: y -/ #check @ideal.is_maximal_iff_is_maximal_disjoint /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, S -/ -- ring_theory/laurent_series.lean #check @laurent_series.power_series_part_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- ring_theory/local_properties.lean #check @ring_hom.of_localization_span_iff_finite /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ -- ring_theory/localization.lean #check @is_localization.map_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @is_localization.lift_mk'_spec /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, v, x -/ #check @is_localization.is_localization_iff_of_alg_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @is_localization.is_localization_iff_of_ring_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: M -/ #check @is_localization.is_localization_iff_of_base_ring_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, M -/ #check @is_localization.mem_inv_submonoid_iff_exists_mk' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, M -/ #check @is_localization.mem_map_algebra_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @is_localization.is_prime_iff_is_prime_disjoint /- The following varibles are used on both sides of an equality or iff and should be made implicit: J, S -/ #check @is_localization.localization_localization_eq_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @is_localization.mem_coe_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: I, S -/ #check @is_localization.coe_submodule_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ #check @is_localization.at_prime.is_unit_to_map_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_localization.at_prime.to_map_mem_maximal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @is_localization.at_prime.is_unit_mk'_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, I -/ #check @is_localization.at_prime.mk'_mem_maximal_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, I -/ #check @is_fraction_ring.coe_submodule_is_principal /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @is_fraction_ring.is_fraction_ring_iff_of_base_ring_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- ring_theory/mv_polynomial/basic.lean #check @mv_polynomial.mem_restrict_total_degree /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, m, σ -/ #check @mv_polynomial.mem_restrict_degree /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, p, σ -/ #check @mv_polynomial.mem_restrict_degree_iff_sup /- The following varibles are used on both sides of an equality or iff and should be made implicit: n, p, σ -/ -- ring_theory/nilpotent.lean #check @algebra.is_nilpotent_lmul_left_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @algebra.is_nilpotent_lmul_right_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- ring_theory/noetherian.lean #check @submodule.fg_iff_add_submonoid_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @submodule.fg_iff_add_subgroup_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ #check @submodule.fg_top /- The following varibles are used on both sides of an equality or iff and should be made implicit: N -/ #check @submodule.fg_iff_compact /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @is_noetherian_ring_iff_ideal_fg /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ -- ring_theory/nullstellensatz.lean #check @mv_polynomial.mem_vanishing_ideal_singleton_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, x -/ #check @mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: I -/ -- ring_theory/polynomial/basic.lean #check @polynomial.monic_to_subring /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @ideal.mem_of_polynomial /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @ideal.mem_leading_coeff_nth /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n, I -/ #check @ideal.mem_leading_coeff_nth_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, I -/ #check @ideal.mem_leading_coeff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, I -/ #check @polynomial.linear_independent_powers_iff_aeval /- The following varibles are used on both sides of an equality or iff and should be made implicit: v, f -/ -- ring_theory/polynomial/cyclotomic/basic.lean #check @is_root_of_unity_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: R -/ #check @polynomial.eq_cyclotomic_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: P -/ -- ring_theory/polynomial/gauss_lemma.lean #check @polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ -- ring_theory/polynomial/homogeneous.lean #check @mv_polynomial.mem_homogeneous_submodule /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, n -/ -- ring_theory/polynomial/symmetric.lean #check @mv_polynomial.mem_symmetric_subalgebra /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- ring_theory/principal_ideal_domain.lean #check @submodule.is_principal.mem_iff_eq_smul_generator /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @submodule.is_principal.eq_bot_iff_generator_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @submodule.is_principal.mem_iff_generator_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @gcd_dvd_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ #check @gcd_is_unit_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- ring_theory/roots_of_unity.lean #check @mem_roots_of_unity /- The following varibles are used on both sides of an equality or iff and should be made implicit: ζ, k -/ #check @is_primitive_root.iff_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: k, ζ -/ #check @is_primitive_root.pow_eq_one_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @is_primitive_root.pow_iff_coprime /- The following varibles are used on both sides of an equality or iff and should be made implicit: i -/ #check @is_primitive_root.zpow_eq_one_iff_dvd /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ #check @is_primitive_root.coe_subgroup_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: H -/ #check @is_primitive_root.zpow_eq_one_iff_dvd₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: l -/ -- ring_theory/subring/basic.lean #check @subring.coe_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @subring.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @units.mem_pos_subgroup /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ -- ring_theory/subring/pointwise.lean #check @subring.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, r, m -/ #check @subring.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subring.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subring.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ -- ring_theory/subsemiring/basic.lean #check @subsemiring.eq_top_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: A -/ #check @mem_pos_monoid /- The following varibles are used on both sides of an equality or iff and should be made implicit: u -/ -- ring_theory/subsemiring/pointwise.lean #check @subsemiring.mem_smul_pointwise_iff_exists /- The following varibles are used on both sides of an equality or iff and should be made implicit: S, r, m -/ #check @subsemiring.smul_mem_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ #check @subsemiring.mem_inv_pointwise_smul_iff₀ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, S -/ -- ring_theory/unique_factorization_domain.lean #check @irreducible_iff_prime_of_exists_unique_irreducible_factors /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @associates.factor_set.prod_eq_zero_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- ring_theory/valuation/basic.lean #check @valuation.mem_supp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, v -/ #check @add_valuation.mem_supp_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, v -/ -- ring_theory/witt_vector/truncated.lean #check @witt_vector.mem_ker_truncate /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, n -/ -- set_theory/cardinal.lean #check @cardinal.le_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: β, α -/ #check @cardinal.prod_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @cardinal.prod_ne_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @cardinal.lift_sup_le_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, f -/ #check @cardinal.mk_set_le_omega /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- set_theory/cardinal_ordinal.lean #check @cardinal.countable_iff_lt_aleph_one /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @cardinal.bit0_ne_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @cardinal.zero_lt_bit0 /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @cardinal.one_le_bit0 /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ #check @cardinal.one_lt_bit1 /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- set_theory/cofinality.lean #check @order.le_cof /- The following varibles are used on both sides of an equality or iff and should be made implicit: c -/ -- set_theory/game/domineering.lean #check @pgame.domineering.mem_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @pgame.domineering.mem_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- set_theory/game/impartial.lean #check @pgame.impartial.not_first_wins /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.not_first_loses /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.equiv_iff_sum_first_loses /- The following varibles are used on both sides of an equality or iff and should be made implicit: H, G -/ #check @pgame.impartial.first_loses_symm /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.first_wins_symm /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.first_loses_symm' /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.first_wins_symm' /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.no_good_left_moves_iff_first_loses /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.no_good_right_moves_iff_first_loses /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.good_left_move_iff_first_wins /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ #check @pgame.impartial.good_right_move_iff_first_wins /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ -- set_theory/game/nim.lean #check @pgame.nim.sum_first_loses_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: O₂, O₁ -/ #check @pgame.nim.sum_first_wins_iff_neq /- The following varibles are used on both sides of an equality or iff and should be made implicit: O₂, O₁ -/ #check @pgame.nim.equiv_iff_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: O₂, O₁ -/ #check @pgame.equiv_nim_iff_grundy_value_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: O, G -/ #check @pgame.equiv_iff_grundy_value_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: H, G -/ #check @pgame.equiv_zero_iff_grundy_value /- The following varibles are used on both sides of an equality or iff and should be made implicit: G -/ -- set_theory/ordinal.lean #check @initial_seg.init_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @principal_seg.down' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @principal_seg.init_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.typein_lt_typein /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @ordinal.typein_le_typein /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- set_theory/ordinal_arithmetic.lean #check @ordinal.lift_is_limit /- The following varibles are used on both sides of an equality or iff and should be made implicit: o -/ #check @ordinal.lt_bsup /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.sup_succ_le_lsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.sup_succ_eq_lsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.sup_eq_lsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.bsup_succ_le_blsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.bsup_succ_eq_blsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.bsup_eq_blsub /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @ordinal.eq_enum_ord /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- set_theory/zfc.lean #check @pSet.equiv.ext /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @Set.subset_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @Set.eq_empty /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ #check @Class.to_Set_of_Set /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, p -/ #check @Class.mem_hom_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, x -/ #check @Class.mem_hom_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @Class.subset_hom /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- tactic/converter/binders.lean #check @exists_elim_eq_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, a -/ #check @exists_elim_eq_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, a -/ #check @forall_comm /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ #check @forall_elim_eq_left /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, a -/ #check @forall_elim_eq_right /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, a -/ -- tactic/ext.lean #check @ulift.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @has_zero.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- tactic/finish.lean #check @auto.classical.implies_iff_not_or /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ -- tactic/omega/nat/form.lean #check @omega.nat.preform.holds_constant /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- tactic/omega/nat/sub_elim.lean #check @omega.nat.sub_subst_equiv /- The following varibles are used on both sides of an equality or iff and should be made implicit: p -/ -- tactic/push_neg.lean #check @push_neg.classical.implies_iff_not_or /- The following varibles are used on both sides of an equality or iff and should be made implicit: q, p -/ #check @push_neg.not_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- tactic/zify.lean #check @int.coe_nat_ne_coe_nat_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: b, a -/ -- testing/slim_check/functions.lean #check @slim_check.injective_function.list.apply_id_zip_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: y -/ #check @slim_check.injective_function.apply_id_mem_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x -/ -- topology/algebra/algebra.lean #check @continuous_algebra_map_iff_smul /- The following varibles are used on both sides of an equality or iff and should be made implicit: A, R -/ -- topology/algebra/infinite_sum.lean #check @finset.has_sum_compl_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @has_sum_nat_add_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ -- topology/algebra/module/basic.lean #check @continuous_linear_map.pi_eq_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_linear_equiv.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @continuous_linear_equiv.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ -- topology/algebra/module/weak_dual.lean #check @weak_dual.tendsto_iff_forall_eval_tendsto /- The following varibles are used on both sides of an equality or iff and should be made implicit: E, 𝕜 -/ -- topology/algebra/ordered/basic.lean #check @tendsto_zero_iff_abs_tendsto_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/algebra/ring.lean #check @ring_topology.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- topology/algebra/uniform_filter_basis.lean #check @add_group_filter_basis.cauchy_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: B -/ -- topology/algebra/uniform_group.lean #check @group_separation_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @topological_add_group.tendsto_uniformly_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f, F -/ #check @topological_group.tendsto_uniformly_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f, F -/ #check @topological_group.tendsto_uniformly_on_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p, f, F -/ #check @topological_add_group.tendsto_uniformly_on_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p, f, F -/ #check @topological_group.tendsto_locally_uniformly_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f, F -/ #check @topological_add_group.tendsto_locally_uniformly_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, f, F -/ #check @topological_add_group.tendsto_locally_uniformly_on_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p, f, F -/ #check @topological_group.tendsto_locally_uniformly_on_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, p, f, F -/ -- topology/basic.lean #check @closure_empty_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @all_mem_nhds /- The following varibles are used on both sides of an equality or iff and should be made implicit: P, x -/ #check @all_mem_nhds_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, f, x -/ #check @map_cluster_pt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: u, F, x -/ #check @is_open_singleton_iff_nhds_eq_pure /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- topology/category/CompHaus/default.lean #check @CompHaus.epi_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @CompHaus.mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/category/Compactum.lean #check @Compactum.is_closed_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- topology/category/Profinite/default.lean #check @Profinite.epi_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Profinite.mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/category/Top/basic.lean #check @Top.open_embedding_iff_comp_is_iso /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Top.open_embedding_iff_is_iso_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: g -/ -- topology/category/Top/epi_mono.lean #check @Top.epi_iff_surjective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Top.mono_iff_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/category/Top/limits.lean #check @Top.colimit_is_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: U, F -/ #check @Top.coequalizer_is_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: U, F -/ -- topology/compact_open.lean #check @continuous_map.tendsto_compact_open_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: f, F -/ #check @continuous_map.exists_tendsto_compact_open_iff_forall /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- topology/constructions.lean #check @mem_nhds_subtype /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, a, s -/ #check @set_pi_mem_nhds_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: a -/ -- topology/continuous_function/bounded.lean #check @bounded_continuous_function.forall_coe_zero_iff_zero /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/continuous_function/compact.lean #check @continuous_map.norm_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_map.norm_le_of_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_map.norm_lt_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_map.norm_lt_iff_of_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/continuous_on.lean #check @tendsto_nhds_within_iff_subtype /- The following varibles are used on both sides of an equality or iff and should be made implicit: l, f -/ #check @continuous_within_at_univ /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @continuous_within_at_iff_continuous_at_restrict /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_within_at_iff_ptendsto_res /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/discrete_quotient.lean #check @discrete_quotient.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- topology/fiber_bundle.lean #check @topological_fiber_bundle.pretrivialization.mem_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @topological_fiber_bundle.pretrivialization.mem_target /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @topological_fiber_bundle.trivialization.mem_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @topological_fiber_bundle.trivialization.mem_target /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @topological_fiber_bundle_core.mem_triv_change_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, j, i, Z -/ #check @topological_fiber_bundle_core.mem_local_triv_as_local_equiv_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, Z -/ #check @topological_fiber_bundle_core.mem_local_triv_as_local_equiv_target /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, Z -/ #check @topological_fiber_bundle_core.mem_local_triv_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, Z -/ #check @topological_fiber_bundle_core.mem_local_triv_target /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, Z -/ -- topology/gluing.lean #check @Top.glue_data.is_open_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: U, D -/ #check @Top.glue_data.ι_eq_iff_rel /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x, j, i, D -/ -- topology/homeomorph.lean #check @homeomorph.comp_continuous_on_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, f -/ #check @homeomorph.comp_continuous_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f -/ #check @homeomorph.comp_continuous_at_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, f, h -/ #check @homeomorph.comp_continuous_within_at_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, s, f -/ -- topology/homotopy/equiv.lean #check @continuous_map.homotopy_equiv.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- topology/instances/ennreal.lean #check @ennreal.has_sum_iff_tendsto_nat /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ #check @has_sum_iff_tendsto_nat_of_nonneg /- The following varibles are used on both sides of an equality or iff and should be made implicit: r -/ -- topology/instances/nnreal.lean #check @nnreal.has_sum_nat_add_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: k -/ -- topology/local_homeomorph.lean #check @local_homeomorph.eq_on_source_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: e', e -/ -- topology/locally_constant/basic.lean #check @is_locally_constant.iff_exists_open /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @is_locally_constant.iff_eventually_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @is_locally_constant.iff_continuous /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @is_locally_constant.iff_continuous_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/maps.lean #check @open_embedding_iff_open_embedding_compose /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/metric_space/completion.lean #check @metric.completion.mem_uniformity_dist /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- topology/metric_space/hausdorff_distance.lean #check @metric.mem_thickening_iff_exists_edist_lt /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, E -/ #check @metric.mem_thickening_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: x, E -/ -- topology/metric_space/isometry.lean #check @isometric.symm_apply_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ #check @isometric.eq_symm_apply /- The following varibles are used on both sides of an equality or iff and should be made implicit: h -/ -- topology/opens.lean #check @topological_space.opens.not_nonempty_iff_eq_bot /- The following varibles are used on both sides of an equality or iff and should be made implicit: U -/ #check @topological_space.opens.ne_bot_iff_nonempty /- The following varibles are used on both sides of an equality or iff and should be made implicit: U -/ -- topology/order.lean #check @le_iff_nhds /- The following varibles are used on both sides of an equality or iff and should be made implicit: t', t -/ #check @le_nhds_adjoint_iff' /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, f, a -/ #check @le_nhds_adjoint_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, f, a -/ #check @mem_nhds_induced /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, a, f -/ #check @induced_iff_nhds_eq /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/separation.lean #check @separated.comm /- The following varibles are used on both sides of an equality or iff and should be made implicit: t, s -/ #check @t0_space_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @t0_space_iff_distinguishable /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @indistinguishable_iff_closed /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @indistinguishable_iff_closure /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @subtype_indistinguishable_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @t0_space_iff_or_not_mem_closure /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ #check @is_open_iff_ultrafilter' /- The following varibles are used on both sides of an equality or iff and should be made implicit: U -/ #check @is_preirreducible_iff_subsingleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ #check @is_irreducible_iff_singleton /- The following varibles are used on both sides of an equality or iff and should be made implicit: S -/ -- topology/sheaves/forget.lean #check @Top.presheaf.is_sheaf_iff_is_sheaf_comp /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- topology/sheaves/sheaf_condition/opens_le_cover.lean #check @Top.presheaf.is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- topology/sheaves/sheaf_condition/pairwise_intersections.lean #check @Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @Top.presheaf.is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- topology/sheaves/sheaf_condition/sites.lean #check @Top.presheaf.is_sheaf_sites_iff_is_sheaf_spaces /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @Top.opens.cover_dense_iff_is_basis /- The following varibles are used on both sides of an equality or iff and should be made implicit: B -/ -- topology/sheaves/sheaf_condition/unique_gluing.lean #check @Top.presheaf.compatible_iff_left_res_eq_right_res /- The following varibles are used on both sides of an equality or iff and should be made implicit: sf, U, F -/ #check @Top.presheaf.is_gluing_iff_eq_res /- The following varibles are used on both sides of an equality or iff and should be made implicit: s, sf, U, F -/ #check @Top.presheaf.is_sheaf_iff_is_sheaf_unique_gluing_types /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ #check @Top.presheaf.is_sheaf_iff_is_sheaf_unique_gluing /- The following varibles are used on both sides of an equality or iff and should be made implicit: F -/ -- topology/sheaves/stalks.lean #check @Top.presheaf.app_injective_iff_stalk_functor_map_injective /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @Top.presheaf.is_iso_iff_stalk_functor_map_iso /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/shrinking_lemma.lean #check @shrinking_lemma.partial_refinement.ext_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ -- topology/sober.lean #check @specializes_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @indistinguishable_iff_specializes_and /- The following varibles are used on both sides of an equality or iff and should be made implicit: y, x -/ #check @quasi_sober_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- topology/subset_properties.lean #check @compact_exhaustion.mem_iff_find_le /- The following varibles are used on both sides of an equality or iff and should be made implicit: K -/ #check @irreducible_space_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- topology/uniform_space/absolute_value.lean #check @is_absolute_value.mem_uniformity /- The following varibles are used on both sides of an equality or iff and should be made implicit: abv -/ -- topology/uniform_space/basic.lean #check @uniform_continuous₂_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @uniform_continuous₂_curry /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ -- topology/uniform_space/compact_convergence.lean #check @continuous_map.mem_compact_convergence_nhd_filter /- The following varibles are used on both sides of an equality or iff and should be made implicit: Y, f -/ #check @continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on' /- The following varibles are used on both sides of an equality or iff and should be made implicit: f -/ #check @continuous_map.mem_compact_convergence_uniformity /- The following varibles are used on both sides of an equality or iff and should be made implicit: X -/ #check @continuous_map.mem_compact_convergence_entourage_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: X -/ -- topology/uniform_space/completion.lean #check @uniform_space.completion.nonempty_completion_iff /- The following varibles are used on both sides of an equality or iff and should be made implicit: α -/ -- topology/uniform_space/separation.lean #check @is_separated_def /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ #check @is_separated_def' /- The following varibles are used on both sides of an equality or iff and should be made implicit: s -/ -- topology/vector_bundle.lean #check @topological_vector_bundle.trivialization.mem_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: e -/ #check @topological_vector_bundle_core.mem_triv_change_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, j, i, Z -/ #check @topological_vector_bundle_core.mem_local_triv_source /- The following varibles are used on both sides of an equality or iff and should be made implicit: p, i, Z -/