simp_nonconfl_lint_b1bfe5f.lean

/- Checking 33119 declarations (plus 35667 automatically generated ones) in mathlib (only in imported files) -/

/- OK: No unused arguments. -/
/- OK: All declarations correctly marked as def/lemma. -/
/- OK: No declarations have a duplicate namespace. -/
/- OK: Not using ≥/> in declarations. -/
/- OK: All instance priorities are good. -/
/- OK: No definitions are missing documentation.. -/
/- OK: No types have missing inhabited instances. -/
/- OK: All instances are applicable. -/
/- OK: All declarations have correct type-class arguments. -/
/- OK: No dangerous instances. -/
/- OK: No time-class searches timed out. -/
/- OK: No invalid `has_coe` instances. -/
/- OK: No uses of `inhabited` arguments should be replaced with `nonempty`. -/
/- OK: All left-hand sides of simp lemmas are in simp-normal form. -/
/- OK: No left-hand sides of a simp lemma has a variable as head symbol. -/
/- The `simp_nonconfl` linter reports: -/
/- SIMP SET IS NOT CONFLUENT.
Some pairs of unjoinable simp lemmas have been found.: -/
-- algebra/archimedean.lean
#print rat.cast_round /- timeout -/

-- algebra/associated.lean
#print unit_mul_dvd_iff /- timeout -/
#print associates.mk_zero_eq /- timeout -/

-- algebra/big_operators.lean
#print finset.prod_sum_elim /- timeout -/

-- algebra/category/CommRing/adjunctions.lean
#print CommRing.free_obj_coe /- timeout -/

-- algebra/category/CommRing/colimits.lean
#print CommRing.colimits.cocone_naturality /- timeout -/

-- algebra/category/Group/adjunctions.lean
#print AddCommGroup.free_obj_coe /- timeout -/

-- algebra/category/Group/basic.lean
#print category_theory.iso.AddCommGroup_iso_to_add_equiv_to_fun /- unjoinable pair with category_theory.iso.AddCommGroup_iso_to_add_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.AddCommGroup_iso_to_add_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4


unjoinable pair with category_theory.iso.AddCommGroup_iso_to_add_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.AddCommGroup_iso_to_add_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4
 -/
#print category_theory.iso.CommGroup_iso_to_mul_equiv_inv_fun /- unjoinable pair with category_theory.iso.CommGroup_iso_to_mul_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.CommGroup_iso_to_mul_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4


unjoinable pair with category_theory.iso.CommGroup_iso_to_mul_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.CommGroup_iso_to_mul_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4
 -/
#print category_theory.iso.AddGroup_iso_to_add_equiv_to_fun /- unjoinable pair with category_theory.iso.AddGroup_iso_to_add_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.AddGroup_iso_to_add_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4


unjoinable pair with category_theory.iso.AddGroup_iso_to_add_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.AddGroup_iso_to_add_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4
 -/
#print category_theory.iso.Group_iso_to_mul_equiv_to_fun /- unjoinable pair with category_theory.iso.Group_iso_to_mul_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.Group_iso_to_mul_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4


unjoinable pair with category_theory.iso.Group_iso_to_mul_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.Group_iso_to_mul_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4
 -/
#print category_theory.iso.Group_iso_to_mul_equiv_inv_fun /- unjoinable pair with category_theory.iso.Group_iso_to_mul_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.Group_iso_to_mul_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4


unjoinable pair with category_theory.iso.Group_iso_to_mul_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.Group_iso_to_mul_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4
 -/
#print category_theory.iso.AddCommGroup_iso_to_add_equiv_inv_fun /- unjoinable pair with category_theory.iso.AddCommGroup_iso_to_add_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.AddCommGroup_iso_to_add_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4


unjoinable pair with category_theory.iso.AddCommGroup_iso_to_add_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.AddCommGroup_iso_to_add_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4
 -/
#print category_theory.iso.CommGroup_iso_to_mul_equiv_to_fun /- unjoinable pair with category_theory.iso.CommGroup_iso_to_mul_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.CommGroup_iso_to_mul_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4


unjoinable pair with category_theory.iso.CommGroup_iso_to_mul_equiv_to_fun:
⇑(?m_2.hom) ?m_3
↑
(category_theory.iso.CommGroup_iso_to_mul_equiv ?m_3).to_fun ?m_4
↓
⇑(?m_3.hom) ?m_4
 -/
#print category_theory.iso.AddGroup_iso_to_add_equiv_inv_fun /- unjoinable pair with category_theory.iso.AddGroup_iso_to_add_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.AddGroup_iso_to_add_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4


unjoinable pair with category_theory.iso.AddGroup_iso_to_add_equiv_inv_fun:
⇑(?m_2.inv) ?m_3
↑
(category_theory.iso.AddGroup_iso_to_add_equiv ?m_3).inv_fun ?m_4
↓
⇑(?m_3.inv) ?m_4
 -/

-- algebra/category/Group/colimits.lean
#print AddCommGroup.colimits.cocone_naturality /- timeout -/

-- algebra/category/Module/basic.lean
#print category_theory.iso.to_linear_equiv_inv_fun /- unjoinable pair with category_theory.iso.to_linear_equiv_inv_fun:
(category_theory.iso.to_linear_equiv ?m_4).inv_fun ?m_5
↑
(category_theory.iso.to_linear_equiv ?m_4).inv_fun ?m_5
↓
⇑(?m_4.inv) ?m_5


unjoinable pair with category_theory.iso.to_linear_equiv_inv_fun:
(category_theory.iso.to_linear_equiv ?m_4).inv_fun ?m_5
↑
(category_theory.iso.to_linear_equiv ?m_4).inv_fun ?m_5
↓
⇑(?m_4.inv) ?m_5
 -/
#print category_theory.iso.to_linear_equiv_to_fun /- unjoinable pair with category_theory.iso.to_linear_equiv_to_fun:
(category_theory.iso.to_linear_equiv ?m_4).to_fun ?m_5
↑
(category_theory.iso.to_linear_equiv ?m_4).to_fun ?m_5
↓
⇑(?m_4.hom) ?m_5


unjoinable pair with category_theory.iso.to_linear_equiv_to_fun:
(category_theory.iso.to_linear_equiv ?m_4).to_fun ?m_5
↑
(category_theory.iso.to_linear_equiv ?m_4).to_fun ?m_5
↓
⇑(?m_4.hom) ?m_5
 -/

-- algebra/category/Mon/colimits.lean
#print Mon.colimits.cocone_naturality /- timeout -/

-- algebra/char_zero.lean
#print nat.cast_inj /- timeout -/
#print nat.cast_eq_zero /- timeout -/
#print half_add_self /- timeout -/
#print add_halves' /- timeout -/

-- algebra/commute.lean
#print commute.units_inv_right_iff /- timeout -/
#print commute.units_inv_left_iff /- timeout -/
#print commute.pow_pow_self /- timeout -/
#print commute.units_coe_iff /- timeout -/
#print commute.cast_nat_right /- timeout -/
#print commute.cast_nat_left /- timeout -/
#print commute.cast_int_left /- timeout -/
#print set.mem_centralizer /- timeout -/

-- algebra/continued_fractions/basic.lean
#print generalized_continued_fraction.coe_to_generalized_continued_fraction /- timeout -/
#print simple_continued_fraction.coe_to_generalized_continued_fraction /- timeout -/
#print continued_fraction.coe_to_simple_continued_fraction /- timeout -/
#print continued_fraction.coe_to_generalized_continued_fraction /- timeout -/

-- algebra/direct_limit.lean
#print ring.direct_limit.of_add /- timeout -/
#print ring.direct_limit.lift_mul /- timeout -/

-- algebra/euclidean_domain.lean
#print euclidean_domain.mod_eq_zero /- timeout -/
#print euclidean_domain.lcm_dvd_iff /- timeout -/
#print euclidean_domain.lcm_eq_zero_iff /- timeout -/

-- algebra/field.lean
#print units.inv_eq_inv /- timeout -/
#print units.mk0_val /- timeout -/
#print inv_eq_zero /- timeout -/

-- algebra/field_power.lean
#print fpow_of_nat /- timeout -/
#print cast_fpow /- timeout -/

-- algebra/floor.lean
#print floor_add_int /- timeout -/
#print floor_add_fract /- timeout -/
#print fract_add_floor /- timeout -/
#print fract_floor /- timeout -/
#print ceil_coe /- timeout -/
#print ceil_add_int /- timeout -/

-- algebra/free.lean
#print free_magma.map_mul' /- timeout -/
#print free_magma.mul_seq /- timeout -/
#print free_magma.traverse_mul /- timeout -/
#print free_magma.traverse_mul' /- timeout -/
#print free_magma.mul_map_seq /- unjoinable pair with id.map_eq:
has_mul.mul ?m_2 <*> ?m_3
↑
has_mul.mul <$> ?m_2 <*> ?m_3
↓
?m_2 * ?m_3


unjoinable pair with id.map_eq:
has_mul.mul ?m_2 <*> ?m_3
↑
has_mul.mul <$> ?m_2 <*> ?m_3
↓
?m_2 * ?m_3
 -/
#print magma.free_semigroup.map_mul /- timeout -/
#print free_semigroup.map_mul /- timeout -/
#print free_semigroup.map_mul' /- timeout -/
#print free_semigroup.mul_seq /- timeout -/
#print free_semigroup.traverse_mul /- timeout -/
#print free_semigroup.traverse_mul' /- timeout -/
#print free_semigroup.mul_map_seq /- unjoinable pair with id.map_eq:
has_mul.mul ?m_2 <*> ?m_3
↑
has_mul.mul <$> ?m_2 <*> ?m_3
↓
?m_2 * ?m_3


unjoinable pair with id.map_eq:
has_mul.mul ?m_2 <*> ?m_3
↑
has_mul.mul <$> ?m_2 <*> ?m_3
↓
?m_2 * ?m_3
 -/

-- algebra/gcd_domain.lean
#print gcd_eq_zero_iff /- timeout -/
#print gcd_mul_left /- timeout -/
#print gcd_mul_right /- timeout -/
#print lcm_eq_zero_iff /- timeout -/
#print lcm_units_coe_left /- timeout -/
#print lcm_units_coe_right /- timeout -/
#print lcm_eq_one_iff /- timeout -/
#print lcm_mul_left /- timeout -/
#print lcm_mul_right /- timeout -/

-- algebra/group/basic.lean
#print mul_left_inj /- timeout -/
#print add_left_inj /- timeout -/
#print add_right_inj /- timeout -/
#print inv_inj' /- timeout -/
#print neg_eq_zero /- timeout -/
#print inv_eq_one /- timeout -/
#print sub_left_inj /- timeout -/
#print sub_right_inj /- timeout -/
#print add_add_neg_cancel'_right /- timeout -/

-- algebra/group/conj.lean
#print conj_mul /- timeout -/

-- algebra/group/is_unit.lean
#print is_add_unit_add_unit /- timeout -/
#print units.is_unit_mul_units /- timeout -/
#print add_units.is_add_unit_add_add_units /- timeout -/
#print is_add_unit.coe_lift_right /- timeout -/
#print is_unit.coe_lift_right /- timeout -/

-- algebra/group/units.lean
#print units.coe_mul /- timeout -/
#print add_units.coe_add /- timeout -/
#print add_units.coe_zero /- timeout -/
#print units.coe_one /- timeout -/
#print add_units.neg_add /- timeout -/
#print units.inv_mul /- timeout -/
#print add_units.add_neg /- timeout -/
#print units.mul_inv /- timeout -/
#print units.mul_inv_cancel_left /- timeout -/
#print add_units.neg_add_cancel_left /- timeout -/
#print units.inv_mul_cancel_left /- timeout -/
#print units.mul_inv_cancel_right /- timeout -/
#print add_units.add_neg_cancel_right /- timeout -/
#print units.inv_mul_cancel_right /- timeout -/
#print add_units.neg_add_cancel_right /- timeout -/
#print add_units.add_left_inj /- timeout -/
#print units.mul_left_inj /- timeout -/
#print units.mul_right_inj /- timeout -/
#print add_units.add_right_inj /- timeout -/
#print divp_mul_cancel /- timeout -/
#print mul_divp_cancel /- timeout -/
#print divp_right_inj /- timeout -/

-- algebra/group/units_hom.lean
#print add_units.coe_map /- timeout -/
#print units.coe_lift_right /- timeout -/

-- algebra/group/with_one.lean
#print with_zero.add_coe /- timeout -/
#print with_one.mul_coe /- timeout -/
#print with_zero.mul_coe /- timeout -/
#print with_zero.inv_coe /- timeout -/

-- algebra/group_power.lean
#print units.coe_pow /- timeout -/
#print gpow_coe_nat /- timeout -/
#print gsmul_coe_nat /- timeout -/
#print gpow_neg /- unjoinable pair with neg_neg:
?m_2 ^ ?m_3
↑
?m_2 ^ - -?m_3
↓
(?m_2 ^ -?m_3)⁻¹
 -/
#print with_bot.coe_smul /- timeout -/
#print nat.cast_pow /- timeout -/

-- algebra/lie_algebra.lean
#print gsmul_lie /- timeout -/
#print lie_gsmul /- timeout -/

-- algebra/module.lean
#print linear_map.to_fun_eq_coe /- unjoinable pair with linear_map.to_fun_eq_coe:
⇑?m_6
↑
?m_9.to_fun
↓
⇑?m_9
 -/
#print submodule.zero_mem /- timeout -/
#print submodule.coe_add /- timeout -/
#print submodule.coe_zero /- timeout -/

-- algebra/opposites.lean
#print opposite.op_add /- timeout -/
#print opposite.op_mul /- timeout -/
#print opposite.unop_mul /- timeout -/

-- algebra/order.lean
#print not_lt /- timeout -/
#print not_le /- timeout -/

-- algebra/order_functions.lean
#print min_le_iff /- timeout -/
#print le_max_iff /- timeout -/

-- algebra/ordered_field.lean
#print inv_pos' /- timeout -/

-- algebra/ordered_group.lean
#print units.coe_le_coe /- timeout -/
#print units.coe_lt_coe /- timeout -/
#print with_top.zero_lt_top /- timeout -/
#print with_top.zero_lt_coe /- timeout -/
#print with_bot.coe_zero /- timeout -/
#print with_bot.coe_add /- timeout -/
#print add_eq_zero_iff /- timeout -/
#print add_le_add_iff_left /- timeout -/
#print add_le_add_iff_right /- timeout -/
#print add_lt_add_iff_left /- timeout -/
#print add_lt_add_iff_right /- timeout -/
#print le_add_iff_nonneg_right /- timeout -/
#print le_add_iff_nonneg_left /- timeout -/
#print neg_nonneg /- timeout -/
#print neg_lt_neg_iff /- timeout -/
#print sub_lt_sub_iff_left /- timeout -/
#print sub_nonpos /- timeout -/
#print neg_add_le_iff_le_add /- timeout -/
#print add_neg_le_iff_le_add' /- timeout -/
#print lt_neg_add_iff_add_lt /- timeout -/
#print neg_add_lt_iff_lt_add /- timeout -/

-- algebra/ordered_ring.lean
#print with_top.coe_eq_zero /- timeout -/
#print with_top.zero_eq_coe /- timeout -/
#print with_top.coe_zero /- timeout -/
#print with_top.top_mul_top /- timeout -/
#print with_top.mul_eq_top_iff /- timeout -/
#print with_top.coe_nat /- timeout -/

-- algebra/pi_instances.lean
#print prod.mk_mul_mk /- timeout -/
#print prod.fst_sub /- timeout -/
#print prod.snd_sub /- timeout -/
#print prod.inr_eq_inr /- timeout -/
#print prod.inr_eq_inl /- timeout -/

-- algebra/pointwise.lean
#print set.pointwise_mul_empty /- timeout -/
#print set.empty_pointwise_mul /- timeout -/

-- algebra/punit_instances.lean
#print punit.Sup_eq /- timeout -/
#print punit.le /- timeout -/

-- algebra/ring.lean
#print ite_mul /- timeout -/
#print units.coe_neg /- timeout -/
#print dvd_add_self_right /- timeout -/
#print mul_eq_zero /- timeout -/
#print zero_eq_mul /- timeout -/
#print units.coe_dvd /- timeout -/
#print units.dvd_coe_mul /- timeout -/
#print units.coe_mul_dvd /- timeout -/

-- algebra/semiconj.lean
#print semiconj_by.units_inv_right_iff /- timeout -/
#print semiconj_by.units_inv_symm_left_iff /- timeout -/
#print semiconj_by.units_coe_iff /- timeout -/

-- algebraic_geometry/presheafed_space.lean
#print algebraic_geometry.PresheafedSpace.mk_coe /- timeout -/
#print algebraic_geometry.PresheafedSpace.hom_mk_coe /- timeout -/
#print algebraic_geometry.PresheafedSpace.id_coe /- timeout -/
#print algebraic_geometry.PresheafedSpace.comp_coe /- timeout -/
#print category_theory.functor.map_presheaf_obj_X /- timeout -/

-- algebraic_geometry/prime_spectrum.lean
#print prime_spectrum.mem_zero_locus /- timeout -/
#print prime_spectrum.zero_locus_span /- timeout -/

-- analysis/complex/basic.lean
#print complex.norm_rat /- timeout -/
#print complex.norm_nat /- timeout -/
#print complex.norm_int /- timeout -/

-- analysis/complex/exponential.lean
#print real.angle.coe_add /- timeout -/
#print real.angle.coe_neg /- timeout -/
#print real.angle.coe_sub /- timeout -/
#print real.angle.coe_gsmul /- timeout -/
#print real.angle.coe_two_pi /- timeout -/
#print complex.cos_pi_div_two /- timeout -/
#print complex.sin_pi /- timeout -/
#print complex.cos_pi /- timeout -/
#print complex.sin_two_pi /- timeout -/
#print complex.abs_cpow_real /- timeout -/
#print complex.abs_cpow_inv_nat /- timeout -/
#print nnreal.coe_rpow /- timeout -/
#print nnreal.rpow_eq_zero_iff /- timeout -/
#print nnreal.rpow_nat_cast /- timeout -/

-- analysis/normed_space/basic.lean
#print norm_nonneg /- timeout -/
#print coe_nnnorm /- timeout -/
#print normed_field.norm_prod /- timeout -/
#print rat.norm_cast_real /- timeout -/

-- analysis/normed_space/multilinear.lean
#print continuous_linear_map.curry_uncurry_left /- unjoinable pair with continuous_linear_map.curry_uncurry_left:
continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left ?m_5)
↑
continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left ?m_5)
↓
?m_1


unjoinable pair with continuous_multilinear_map.uncurry_curry_left:
continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5))
↑
continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5))
↓
continuous_multilinear_map.curry_left ?m_5
 -/
#print continuous_multilinear_map.uncurry_curry_left /- unjoinable pair with continuous_multilinear_map.uncurry_curry_left:
continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5)
↑
continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5)
↓
?m_1


unjoinable pair with continuous_linear_map.curry_uncurry_left:
continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left ?m_5))
↑
continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left (continuous_linear_map.uncurry_left ?m_5))
↓
continuous_linear_map.uncurry_left ?m_5
 -/
#print continuous_linear_map.uncurry_left_norm /- unjoinable pair with continuous_multilinear_map.uncurry_curry_left:
∥continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5)∥
↑
∥continuous_linear_map.uncurry_left (continuous_multilinear_map.curry_left ?m_5)∥
↓
∥continuous_multilinear_map.curry_left ?m_5∥
 -/
#print continuous_multilinear_map.uncurry_curry_right /- unjoinable pair with continuous_multilinear_map.uncurry_curry_right:
continuous_multilinear_map.uncurry_right (continuous_multilinear_map.curry_right ?m_5)
↑
continuous_multilinear_map.uncurry_right (continuous_multilinear_map.curry_right ?m_5)
↓
?m_1
 -/

-- analysis/normed_space/operator_norm.lean
#print linear_map.mk_continuous_coe /- timeout -/
#print continuous_linear_map.restrict_scalars_coe_eq_coe /- timeout -/

-- category/fold.lean
#print traversable.mfoldr_map /- timeout -/

-- category_theory/adjunction/basic.lean
#print category_theory.adjunction.core_unit_counit.right_triangle /- timeout -/
#print category_theory.adjunction.left_triangle_components_assoc /- timeout -/
#print category_theory.adjunction.left_triangle_components /- timeout -/
#print category_theory.adjunction.right_triangle_components_assoc /- timeout -/
#print category_theory.adjunction.right_triangle_components /- timeout -/
#print category_theory.adjunction.counit_naturality /- timeout -/
#print category_theory.adjunction.counit_naturality_assoc /- timeout -/
#print category_theory.adjunction.unit_naturality /- timeout -/
#print category_theory.adjunction.unit_naturality_assoc /- timeout -/

-- category_theory/adjunction/limits.lean
#print category_theory.adjunction.functoriality_unit_app_hom /- timeout -/
#print category_theory.adjunction.functoriality_counit'_app_hom /- timeout -/
#print category_theory.adjunction.cocones_iso_component_inv_app /- timeout -/
#print category_theory.adjunction.cones_iso_component_hom_app /- timeout -/

-- category_theory/comma.lean
#print category_theory.comma_morphism.w /- timeout -/
#print category_theory.comma.fst_obj /- timeout -/
#print category_theory.comma.map_left_obj_left /- timeout -/
#print category_theory.comma.map_left_obj_right /- unjoinable pair with category_theory.comma.map_left_obj_right:
((category_theory.comma.map_left ?m_5 ?m_7).obj ?m_8).right
↑
((category_theory.comma.map_left ?m_5 ?m_7).obj ?m_8).right
↓
?m_6.right
 -/
#print category_theory.comma.map_left_map_left /- unjoinable pair with category_theory.comma.map_left_map_left:
((category_theory.comma.map_left ?m_5 ?m_7).map ?m_10).left
↑
((category_theory.comma.map_left ?m_5 ?m_7).map ?m_10).left
↓
?m_8.left
 -/
#print category_theory.comma.map_left_map_right /- unjoinable pair with category_theory.comma.map_left_map_right:
((category_theory.comma.map_left ?m_5 ?m_7).map ?m_10).right
↑
((category_theory.comma.map_left ?m_5 ?m_7).map ?m_10).right
↓
?m_8.right
 -/
#print category_theory.comma.map_left_id_hom_app_right /- timeout -/
#print category_theory.comma.map_left_id_inv_app_right /- timeout -/
#print category_theory.comma.map_left_comp_hom_app_left /- timeout -/
#print category_theory.comma.map_left_comp_inv_app_left /- timeout -/
#print category_theory.comma.map_right_obj_left /- timeout -/
#print category_theory.comma.map_right_obj_right /- timeout -/
#print category_theory.comma.map_right_map_left /- unjoinable pair with category_theory.comma.map_right_map_left:
((category_theory.comma.map_right ?m_4 ?m_7).map ?m_10).left
↑
((category_theory.comma.map_right ?m_4 ?m_7).map ?m_10).left
↓
?m_8.left
 -/
#print category_theory.comma.map_right_map_right /- timeout -/
#print category_theory.comma.map_right_comp_hom_app_right /- timeout -/
#print category_theory.comma.map_right_comp_inv_app_right /- timeout -/
#print category_theory.over.w_assoc /- timeout -/
#print category_theory.over.w /- timeout -/
#print category_theory.over.map_obj_left /- unjoinable pair with category_theory.over.map_obj_left:
((category_theory.over.map ?m_4).obj ?m_5).left
↑
((category_theory.over.map ?m_4).obj ?m_5).left
↓
?m_3.left
 -/
#print category_theory.over.map_map_left /- unjoinable pair with category_theory.over.map_map_left:
((category_theory.over.map ?m_4).map ?m_7).left
↑
((category_theory.over.map ?m_4).map ?m_7).left
↓
?m_5.left
 -/
#print category_theory.over.iterated_slice_forward_map /- timeout -/
#print category_theory.under.w /- timeout -/
#print category_theory.under.forget_obj /- timeout -/
#print category_theory.under.map_obj_right /- timeout -/
#print category_theory.under.map_map_right /- unjoinable pair with category_theory.under.map_map_right:
((category_theory.under.map ?m_4).map ?m_7).right
↑
((category_theory.under.map ?m_4).map ?m_7).right
↓
?m_5.right
 -/

-- category_theory/const.lean
#print category_theory.functor.const.obj_obj /- timeout -/
#print category_theory.functor.const.obj_map /- timeout -/
#print category_theory.functor.const.op_obj_op_hom_app /- timeout -/
#print category_theory.functor.const.op_obj_op_inv_app /- timeout -/
#print category_theory.functor.const.op_obj_unop_inv_app /- timeout -/
#print category_theory.functor.const_comp_inv_app /- timeout -/
#print category_theory.functor.const_comp_hom_app /- timeout -/

-- category_theory/currying.lean
#print category_theory.uncurry.obj_obj /- timeout -/
#print category_theory.uncurry.map_app /- timeout -/
#print category_theory.curry.obj_obj_obj /- timeout -/
#print category_theory.curry.map_app_app /- timeout -/

-- category_theory/discrete_category.lean
#print category_theory.functor.of_function_obj /- timeout -/

-- category_theory/elements.lean
#print category_theory.category_of_elements.π_obj /- timeout -/

-- category_theory/epi_mono.lean
#print category_theory.split_epi.id_assoc /- timeout -/

-- category_theory/eq_to_hom.lean
#print category_theory.eq_to_hom_trans /- timeout -/
#print category_theory.eq_to_hom_trans_assoc /- timeout -/

-- category_theory/equivalence.lean
#print category_theory.equivalence.functor_unit_comp /- timeout -/
#print category_theory.equivalence.counit_inv_functor_comp /- timeout -/
#print category_theory.equivalence.unit_inverse_comp /- timeout -/
#print category_theory.equivalence.inverse_counit_inv_comp /- timeout -/
#print category_theory.equivalence.fun_inv_map /- timeout -/
#print category_theory.equivalence.inv_fun_map /- timeout -/
#print category_theory.equivalence.fun_inv_id_assoc_inv_app /- timeout -/
#print category_theory.equivalence.inv_fun_id_assoc_hom_app /- timeout -/
#print category_theory.is_equivalence.functor_unit_comp /- timeout -/

-- category_theory/full_subcategory.lean
#print category_theory.induced_functor.hom /- timeout -/
#print category_theory.full_subcategory_inclusion.obj /- timeout -/

-- category_theory/functor.lean
#print category_theory.functor.map_id /- timeout -/
#print category_theory.functor.map_comp /- timeout -/
#print category_theory.functor.comp_obj /- timeout -/

-- category_theory/functor_category.lean
#print category_theory.nat_trans.id_app /- timeout -/
#print category_theory.functor.flip_obj_obj /- timeout -/
#print category_theory.functor.flip_map_app /- timeout -/

-- category_theory/isomorphism.lean
#print category_theory.iso.inv_hom_id /- timeout -/
#print category_theory.iso.inv_hom_id_assoc /- timeout -/
#print category_theory.is_iso.inv_hom_id_assoc /- timeout -/

-- category_theory/limits/cones.lean
#print category_theory.limits.cone.w /- timeout -/
#print category_theory.limits.cocone.w /- timeout -/
#print category_theory.limits.cones.postcompose_map_hom /- unjoinable pair with category_theory.limits.cones.postcompose_map_hom:
((category_theory.limits.cones.postcompose ?m_5).map ?m_8).hom
↑
((category_theory.limits.cones.postcompose ?m_5).map ?m_8).hom
↓
?m_6.hom
 -/
#print category_theory.limits.cones.postcompose_obj_X /- unjoinable pair with category_theory.limits.cones.postcompose_obj_X:
((category_theory.limits.cones.postcompose ?m_5).obj ?m_6).X
↑
((category_theory.limits.cones.postcompose ?m_5).obj ?m_6).X
↓
?m_4.X
 -/
#print category_theory.limits.cones.functoriality_obj_X /- timeout -/
#print category_theory.limits.cocones.precompose_obj_X /- timeout -/
#print category_theory.limits.cocones.precompose_map_hom /- unjoinable pair with category_theory.limits.cocones.precompose_map_hom:
((category_theory.limits.cocones.precompose ?m_5).map ?m_8).hom
↑
((category_theory.limits.cocones.precompose ?m_5).map ?m_8).hom
↓
?m_6.hom
 -/
#print category_theory.limits.cocones.functoriality_obj_X /- timeout -/
#print category_theory.functor.map_cocone_ι /- timeout -/
#print category_theory.limits.cone_of_cocone_left_op_π_app /- timeout -/
#print category_theory.limits.cocone_of_cone_left_op_ι_app /- timeout -/

-- category_theory/limits/functor_category.lean
#print category_theory.limits.cone.functor_w /- timeout -/
#print category_theory.limits.cocone.functor_w /- timeout -/
#print category_theory.limits.functor_category_limit_cone_π_app_app /- timeout -/
#print category_theory.limits.functor_category_colimit_cocone_ι_app_app /- timeout -/

-- category_theory/limits/limits.lean
#print category_theory.limits.is_limit.fac /- timeout -/
#print category_theory.limits.is_colimit.fac /- timeout -/
#print category_theory.limits.limit.lift_π_assoc /- timeout -/
#print category_theory.limits.limit.lift_π /- timeout -/
#print category_theory.limits.limit.hom_iso_hom /- timeout -/
#print category_theory.limits.limit.lift_pre /- timeout -/
#print category_theory.limits.limit.post_π /- timeout -/
#print category_theory.limits.limit.lift_post /- timeout -/
#print category_theory.limits.limit.post_post /- timeout -/
#print category_theory.limits.limit.lift_map /- timeout -/
#print category_theory.limits.colimit.ι_desc /- timeout -/
#print category_theory.limits.colimit.hom_iso_hom /- timeout -/
#print category_theory.limits.colimit.ι_pre_assoc /- timeout -/
#print category_theory.limits.colimit.ι_pre /- timeout -/
#print category_theory.limits.colimit.ι_post /- timeout -/
#print category_theory.limits.colimit.ι_post_assoc /- timeout -/
#print category_theory.limits.colimit.post_desc /- timeout -/
#print category_theory.limits.colimit.post_post /- timeout -/
#print category_theory.limits.colimit.ι_map_assoc /- timeout -/
#print category_theory.limits.colimit.ι_map /- timeout -/
#print category_theory.limits.colimit.map_desc /- timeout -/

-- category_theory/limits/over.lean
#print category_theory.functor.to_cone_π_app /- timeout -/
#print category_theory.under.limit_π_app /- timeout -/

-- category_theory/limits/shapes/binary_products.lean
#print category_theory.limits.pair_obj_right /- timeout -/
#print category_theory.limits.binary_cofan.mk_ι_app_left /- timeout -/
#print category_theory.limits.prod.symmetry' /- unjoinable pair with category_theory.limits.prod.symmetry':
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫
  category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
↑
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫
  category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
↓
𝟙 (?m_2 ⨯ ?m_3)


unjoinable pair with category_theory.limits.prod.symmetry':
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫
  category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
↑
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫
  category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
↓
𝟙 (?m_2 ⨯ ?m_3)
 -/
#print category_theory.limits.coprod.symmetry' /- timeout -/

-- category_theory/limits/shapes/equalizers.lean
#print category_theory.limits.parallel_pair_obj_one /- timeout -/
#print category_theory.limits.parallel_pair_functor_obj /- timeout -/
#print category_theory.limits.cone_parallel_pair_left /- timeout -/
#print category_theory.limits.cone_parallel_pair_right /- timeout -/
#print category_theory.limits.cocone_parallel_pair_left /- timeout -/
#print category_theory.limits.cocone_parallel_pair_right /- timeout -/
#print category_theory.limits.cone.of_fork_π /- timeout -/
#print category_theory.limits.cocone_parallel_pair_self_ι_app_one /- timeout -/
#print category_theory.limits.cocone_of_split_epi_ι_app_one /- timeout -/
#print category_theory.limits.cocone_of_split_epi_ι_app_zero /- timeout -/

-- category_theory/limits/shapes/images.lean
#print category_theory.limits.mono_factorisation.fac /- timeout -/
#print category_theory.limits.mono_factorisation.fac_assoc /- timeout -/
#print category_theory.limits.image.fac_assoc /- timeout -/
#print category_theory.limits.image.lift_fac /- timeout -/
#print category_theory.limits.image_mono_iso_source_inv_ι /- timeout -/
#print category_theory.limits.image_mono_iso_source_hom_self_assoc /- timeout -/

-- category_theory/limits/shapes/kernels.lean
#print category_theory.limits.kernel_fork.condition_assoc /- timeout -/
#print category_theory.limits.kernel_fork.app_one /- timeout -/
#print category_theory.limits.cokernel_cofork.condition /- timeout -/
#print category_theory.limits.cokernel_cofork.condition_assoc /- timeout -/
#print category_theory.limits.cokernel_cofork.app_zero /- timeout -/

-- category_theory/limits/shapes/pullbacks.lean
#print category_theory.limits.span_right /- timeout -/
#print category_theory.limits.cospan_one /- timeout -/
#print category_theory.limits.span_zero /- timeout -/
#print category_theory.limits.pullback_cone.mk_π_app_one /- timeout -/
#print category_theory.limits.pushout_cocone.mk_ι_app_right /- timeout -/
#print category_theory.limits.cone.of_pullback_cone_π /- timeout -/

-- category_theory/limits/shapes/zero.lean
#print category_theory.limits.has_zero_morphisms.zero_comp_assoc /- timeout -/

-- category_theory/monad/adjunction.lean
#print category_theory.adjunction.monad_η_app /- timeout -/
#print category_theory.monad.comparison_map_f /- timeout -/

-- category_theory/monad/algebra.lean
#print category_theory.comonad.coalgebra.hom.h /- timeout -/
#print category_theory.monad.algebra.EilenbergMoore_to_category_struct_comp /- timeout -/
#print category_theory.comonad.coalgebra.EilenbergMoore_to_category_struct_comp /- timeout -/
#print category_theory.comonad.cofree_obj_A /- timeout -/

-- category_theory/monad/basic.lean
#print category_theory.monad.left_unit /- timeout -/
#print category_theory.monad.right_unit /- timeout -/
#print category_theory.comonad.left_counit /- timeout -/

-- category_theory/monoidal/category.lean
#print category_theory.monoidal_category.triangle /- timeout -/
#print category_theory.monoidal_category.tensor_left_iff /- timeout -/
#print category_theory.monoidal_category.tensor_right_iff /- timeout -/
#print category_theory.monoidal_category.left_unitor_tensor_inv /- timeout -/
#print category_theory.monoidal_category.right_unitor_tensor /- timeout -/
#print category_theory.monoidal_category.right_unitor_tensor_inv /- timeout -/
#print category_theory.monoidal_category.triangle_assoc_comp_right /- timeout -/
#print category_theory.monoidal_category.triangle_assoc_comp_right_inv /- timeout -/
#print category_theory.monoidal_category.left_assoc_tensor_obj /- timeout -/
#print category_theory.monoidal_category.left_assoc_tensor_map /- timeout -/

-- category_theory/monoidal/functor.lean
#print category_theory.lax_monoidal_functor.μ_natural /- timeout -/
#print category_theory.lax_monoidal_functor.associativity /- timeout -/

-- category_theory/natural_isomorphism.lean
#print category_theory.nat_iso.inv_hom_id_app /- timeout -/

-- category_theory/natural_transformation.lean
#print category_theory.nat_trans.naturality /- timeout -/
#print category_theory.nat_trans.id_app' /- timeout -/

-- category_theory/opposites.lean
#print category_theory.unop_comp /- timeout -/
#print category_theory.functor.op_obj /- timeout -/
#print category_theory.functor.unop_obj /- timeout -/
#print category_theory.functor.op_hom.obj /- timeout -/
#print category_theory.functor.op_inv.obj /- timeout -/
#print category_theory.functor.op_inv.map_app /- timeout -/
#print category_theory.functor.right_op_obj /- timeout -/
#print category_theory.nat_trans.unop_app /- timeout -/

-- category_theory/products/associator.lean
#print category_theory.prod.associator_map /- timeout -/
#print category_theory.prod.associator_obj /- timeout -/

-- category_theory/products/basic.lean
#print category_theory.prod.inl_obj /- timeout -/
#print category_theory.prod.fst_obj /- timeout -/
#print category_theory.prod.symmetry_inv_app /- timeout -/
#print category_theory.evaluation_obj_map /- timeout -/
#print category_theory.evaluation_obj_obj /- timeout -/
#print category_theory.evaluation_uncurried_obj /- timeout -/
#print category_theory.functor.prod_obj /- timeout -/

-- category_theory/products/bifunctor.lean
#print category_theory.bifunctor.map_id_comp /- timeout -/
#print category_theory.bifunctor.map_comp_id /- timeout -/
#print category_theory.bifunctor.diagonal /- timeout -/
#print category_theory.bifunctor.diagonal' /- timeout -/

-- category_theory/sums/associator.lean
#print category_theory.sum.associator_obj_inl_inl /- timeout -/
#print category_theory.sum.associator_obj_inl_inr /- timeout -/
#print category_theory.sum.inverse_associator_obj_inl /- timeout -/

-- category_theory/sums/basic.lean
#print category_theory.functor.sum_obj_inl /- timeout -/
#print category_theory.functor.sum_map_inl /- timeout -/

-- category_theory/types.lean
#print category_theory.functor_to_types.comp /- timeout -/
#print category_theory.ulift_functor_map /- unjoinable pair with category_theory.functor_to_types.map_id:
{down := ?m_2.down}
↑
category_theory.ulift_functor.map (𝟙 ?m_1) ?m_2
↓
{down := ?m_2.down}


unjoinable pair with category_theory.functor_to_types.map_id:
category_theory.ulift_functor.map id ?m_2
↑
category_theory.ulift_functor.map (𝟙 ?m_1) ?m_2
↓
{down := ?m_2.down}
 -/
#print category_theory.of_type_functor_obj /- unjoinable pair with category_theory.of_type_functor_obj:
(category_theory.of_type_functor ?m_1).obj
↑
(category_theory.of_type_functor ?m_1).obj
↓
?m_1
 -/
#print category_theory.of_type_functor_map /- timeout -/
#print equiv_iso_iso_hom /- timeout -/

-- category_theory/whiskering.lean
#print category_theory.whiskering_left_map_app_app /- timeout -/
#print category_theory.whiskering_left_obj_obj /- timeout -/
#print category_theory.whiskering_right_map_app_app /- timeout -/
#print category_theory.whiskering_right_obj_obj /- timeout -/

-- category_theory/yoneda.lean
#print category_theory.yoneda_obj_obj /- timeout -/
#print category_theory.coyoneda_map_app /- timeout -/
#print category_theory.yoneda_sections /- timeout -/

-- computability/partrec.lean
#print nat.mem_rfind /- timeout -/

-- computability/turing_machine.lean
#print turing.tape.write_self /- timeout -/
#print turing.tape.map_write /- unjoinable pair with turing.tape.write_self:
turing.tape.map ?m_3 ?m_4
↑
turing.tape.map ?m_3 (turing.tape.write ?m_4.fst ?m_4)
↓
turing.tape.write (?m_2 ?m_4.fst) (turing.tape.map ?m_2 ?m_4)


unjoinable pair with turing.tape.write_self:
turing.tape.map ?m_3 ?m_4
↑
turing.tape.map ?m_3 (turing.tape.write ?m_4.fst ?m_4)
↓
turing.tape.write (?m_2 ?m_4.fst) (turing.tape.map ?m_2 ?m_4)
 -/

-- data/analysis/filter.lean
#print cfilter.mem_to_filter_sets /- timeout -/

-- data/analysis/topology.lean
#print ctop.mem_nhds_to_topsp /- timeout -/

-- data/array/lemmas.lean
#print array.to_list_reverse /- unjoinable pair with array.to_array_to_list:
list.reverse ?m_2
↑
list.reverse (array.to_list (list.to_array ?m_2))
↓
array.rev_list (list.to_array ?m_2)
 -/
#print array.mem_rev_list /- timeout -/
#print array.mem_to_list /- timeout -/
#print array.to_list_nth_le' /- unjoinable pair with array.to_array_to_list:
list.nth_le ?m_2 ?m_3.val _
↑
list.nth_le (array.to_list (list.to_array ?m_2)) ?m_3.val ?m_4
↓
array.read (list.to_array ?m_2) ?m_3


unjoinable pair with fin.last_val:
list.nth_le (array.to_list ?m_3) ?m_2 _
↑
list.nth_le (array.to_list ?m_3) (fin.last ?m_2).val ?m_4
↓
array.read ?m_3 (fin.last ?m_1)
 -/

-- data/bool.lean
#print bool.tt_eq_to_bool_iff /- timeout -/
#print bool.ff_eq_to_bool_iff /- timeout -/
#print bool.to_bool_eq /- timeout -/
#print bool.bxor_assoc /- unjoinable pair with bxor_self:
?m_1
↑
bxor (bxor ?m_1 ?m_1) ?m_2
↓
bxor ?m_1 (bxor ?m_1 ?m_2)


unjoinable pair with bxor_self:
?m_1
↑
bxor (bxor ?m_1 ?m_1) ?m_2
↓
bxor ?m_1 (bxor ?m_1 ?m_2)
 -/

-- data/buffer/basic.lean
#print buffer.to_list_append_list /- unjoinable pair with buffer.append_list_mk_buffer:
buffer.to_list (array.to_buffer (list.to_array ?m_2))
↑
buffer.to_list (buffer.append_list mk_buffer ?m_2)
↓
buffer.to_list mk_buffer ++ ?m_2


unjoinable pair with buffer.append_list_mk_buffer:
buffer.to_list (array.to_buffer (list.to_array ?m_2))
↑
buffer.to_list (buffer.append_list mk_buffer ?m_2)
↓
buffer.to_list mk_buffer ++ ?m_2
 -/

-- data/complex/basic.lean
#print complex.eta /- unjoinable pair with complex.one_re:
{re := 1, im := 0}
↑
{re := 1.re, im := 1.im}
↓
1


unjoinable pair with complex.one_im:
{re := 1, im := 0}
↑
{re := 1.re, im := 1.im}
↓
1
 -/
#print complex.of_real_im /- timeout -/
#print complex.of_real_inj /- unjoinable pair with complex.of_real_one:
1 = ↑?m_1
↑
↑1 = ↑?m_1
↓
1 = ?m_1


unjoinable pair with complex.of_real_one:
↑?m_1 = 1
↑
↑?m_1 = ↑1
↓
?m_1 = 1
 -/
#print complex.of_real_zero /- timeout -/
#print complex.of_real_eq_zero /- timeout -/
#print complex.of_real_add /- timeout -/
#print complex.of_real_neg /- timeout -/
#print complex.of_real_mul /- timeout -/
#print complex.re_add_im /- timeout -/
#print complex.conj_of_real /- timeout -/
#print complex.norm_sq_of_real /- timeout -/
#print complex.norm_sq_eq_zero /- timeout -/
#print complex.norm_sq_pos /- timeout -/
#print complex.of_real_sub /- timeout -/
#print complex.inv_re /- unjoinable pair with inv_inv':
?m_1.re
↑
?m_1⁻¹⁻¹.re
↓
?m_1.re / complex.norm_sq ?m_1 / (complex.norm_sq ?m_1)⁻¹
 -/
#print complex.inv_im /- unjoinable pair with inv_inv':
?m_1.im
↑
?m_1⁻¹⁻¹.im
↓
-(-?m_1.im / complex.norm_sq ?m_1) / (complex.norm_sq ?m_1)⁻¹
 -/
#print complex.of_real_inv /- timeout -/
#print complex.of_real_fpow /- timeout -/
#print complex.of_real_int_cast /- timeout -/
#print complex.of_real_nat_cast /- timeout -/
#print complex.of_real_rat_cast /- timeout -/
#print complex.nat_cast_re /- timeout -/
#print complex.nat_cast_im /- timeout -/
#print complex.int_cast_im /- timeout -/
#print complex.rat_cast_re /- timeout -/
#print complex.rat_cast_im /- timeout -/
#print complex.abs_eq_zero /- unjoinable pair with complex.abs_two:
2 = 0
↑
complex.abs 2 = 0
↓
2 = 0
 -/
#print complex.abs_pos /- timeout -/

-- data/complex/exponential.lean
#print complex.exp_conj /- unjoinable pair with complex.conj_neg_I:
complex.exp complex.I
↑
complex.exp (complex.conj (-complex.I))
↓
complex.conj (complex.exp (-complex.I))
 -/
#print complex.of_real_exp_of_real_re /- timeout -/
#print complex.of_real_exp /- timeout -/
#print complex.exp_of_real_im /- timeout -/
#print complex.of_real_sinh_of_real_re /- timeout -/
#print complex.of_real_sinh /- timeout -/
#print complex.sinh_of_real_im /- timeout -/
#print complex.of_real_cosh_of_real_re /- unjoinable pair with complex.of_real_one:
↑((complex.cosh 1).re)
↑
↑((complex.cosh ↑1).re)
↓
complex.cosh 1
 -/
#print complex.of_real_cosh /- timeout -/
#print complex.cosh_of_real_im /- timeout -/
#print complex.of_real_tanh_of_real_re /- timeout -/
#print complex.of_real_tanh /- timeout -/
#print complex.tanh_of_real_im /- timeout -/
#print complex.of_real_sin_of_real_re /- timeout -/
#print complex.of_real_sin /- timeout -/
#print complex.sin_of_real_im /- timeout -/
#print complex.of_real_cos_of_real_re /- timeout -/
#print complex.cos_of_real_im /- timeout -/
#print complex.of_real_tan_of_real_re /- unjoinable pair with complex.of_real_one:
↑((complex.tan 1).re)
↑
↑((complex.tan ↑1).re)
↓
complex.tan 1
 -/
#print complex.of_real_tan /- timeout -/
#print complex.tan_of_real_im /- timeout -/
#print real.exp_eq_one_iff /- timeout -/
#print complex.abs_exp_of_real /- unjoinable pair with complex.of_real_one:
complex.abs (complex.exp 1)
↑
complex.abs (complex.exp ↑1)
↓
real.exp 1
 -/

-- data/dfinsupp.lean
#print dfinsupp.mem_support_to_fun /- timeout -/
#print dfinsupp.support_eq_empty /- timeout -/

-- data/equiv/basic.lean
#print equiv.arrow_congr_trans /- unjoinable pair with equiv.trans_symm:
equiv.arrow_congr (equiv.refl ?m_1) (equiv.trans ?m_5 ?m_6)
↑
equiv.arrow_congr (equiv.trans ?m_5 (equiv.symm ?m_5)) (equiv.trans ?m_7 ?m_8)
↓
equiv.trans (equiv.arrow_congr ?m_6 ?m_7) (equiv.arrow_congr (equiv.symm ?m_6) ?m_8)


unjoinable pair with equiv.trans_symm:
equiv.arrow_congr (equiv.refl ?m_1) (equiv.trans ?m_5 ?m_6)
↑
equiv.arrow_congr (equiv.trans ?m_5 (equiv.symm ?m_5)) (equiv.trans ?m_7 ?m_8)
↓
equiv.trans (equiv.arrow_congr ?m_6 ?m_7) (equiv.arrow_congr (equiv.symm ?m_6) ?m_8)


unjoinable pair with equiv.trans_symm:
equiv.arrow_congr (equiv.trans ?m_5 ?m_6) (equiv.refl ?m_2)
↑
equiv.arrow_congr (equiv.trans ?m_5 ?m_6) (equiv.trans ?m_8 (equiv.symm ?m_8))
↓
equiv.trans (equiv.arrow_congr ?m_6 ?m_7) (equiv.arrow_congr ?m_8 (equiv.symm ?m_7))


unjoinable pair with equiv.trans_symm:
equiv.arrow_congr (equiv.trans ?m_5 ?m_6) (equiv.refl ?m_2)
↑
equiv.arrow_congr (equiv.trans ?m_5 ?m_6) (equiv.trans ?m_8 (equiv.symm ?m_8))
↓
equiv.trans (equiv.arrow_congr ?m_6 ?m_7) (equiv.arrow_congr ?m_8 (equiv.symm ?m_7))
 -/
#print equiv.conj_trans /- unjoinable pair with equiv.trans_symm:
equiv.refl (?m_1 → ?m_1)
↑
equiv.conj (equiv.trans ?m_3 (equiv.symm ?m_3))
↓
equiv.trans (equiv.conj ?m_3) (equiv.conj (equiv.symm ?m_3))


unjoinable pair with equiv.trans_symm:
equiv.refl (?m_1 → ?m_1)
↑
equiv.conj (equiv.trans ?m_3 (equiv.symm ?m_3))
↓
equiv.trans (equiv.conj ?m_3) (equiv.conj (equiv.symm ?m_3))
 -/

-- data/equiv/local_equiv.lean
#print equiv.to_local_equiv_to_fun /- unjoinable pair with equiv.refl_to_local_equiv:
id
↑
(equiv.to_local_equiv (equiv.refl ?m_1)).to_fun
↓
(equiv.refl ?m_1).to_fun
 -/
#print equiv.to_local_equiv_inv_fun /- unjoinable pair with equiv.refl_to_local_equiv:
id
↑
(equiv.to_local_equiv (equiv.refl ?m_1)).inv_fun
↓
(equiv.refl ?m_1).inv_fun
 -/
#print equiv.trans_to_local_equiv /- unjoinable pair with equiv.trans_symm:
local_equiv.refl ?m_1
↑
equiv.to_local_equiv (equiv.trans ?m_3 (equiv.symm ?m_3))
↓
local_equiv.trans (equiv.to_local_equiv ?m_3) (local_equiv.symm (equiv.to_local_equiv ?m_3))


unjoinable pair with equiv.trans_symm:
local_equiv.refl ?m_1
↑
equiv.to_local_equiv (equiv.trans ?m_3 (equiv.symm ?m_3))
↓
local_equiv.trans (equiv.to_local_equiv ?m_3) (local_equiv.symm (equiv.to_local_equiv ?m_3))
 -/

-- data/equiv/mul_add.lean
#print mul_equiv.map_eq_one_iff /- timeout -/

-- data/equiv/ring.lean
#print ring_equiv.map_eq_one_iff /- timeout -/
#print ring_equiv.map_eq_zero_iff /- timeout -/
#print equiv.coe_units_equiv_ne_zero /- timeout -/

-- data/fin.lean
#print fin.eta /- unjoinable pair with fin.last_val:
⟨?m_1, _⟩
↑
⟨(fin.last ?m_1).val, ?m_2⟩
↓
fin.last ?m_1
 -/
#print fin.mk.inj_iff /- timeout -/
#print fin.coe_mk /- timeout -/
#print fin.succ_inj /- timeout -/
#print fin.pred_inj /- unjoinable pair with fin.pred_succ:
?m_2 = fin.pred ?m_3 ?m_4
↑
fin.pred (fin.succ ?m_2) ?m_3 = fin.pred ?m_4 ?m_5
↓
fin.succ ?m_2 = ?m_3


unjoinable pair with fin.pred_succ:
fin.pred ?m_2 ?m_3 = ?m_4
↑
fin.pred ?m_2 ?m_3 = fin.pred (fin.succ ?m_4) ?m_5
↓
?m_2 = fin.succ ?m_3
 -/
#print fin.cast_succ_inj /- timeout -/
#print fin.tail_update_succ /- unjoinable pair with function.update_eq_self:
fin.tail ?m_3
↑
fin.tail (function.update ?m_3 (fin.succ ?m_4) (?m_3 (fin.succ ?m_4)))
↓
function.update (fin.tail ?m_3) ?m_4 (?m_3 (fin.succ ?m_4))


unjoinable pair with function.update_eq_self:
fin.tail ?m_3
↑
fin.tail (function.update ?m_3 (fin.succ ?m_4) (?m_3 (fin.succ ?m_4)))
↓
function.update (fin.tail ?m_3) ?m_4 (?m_3 (fin.succ ?m_4))
 -/
#print fin.init_update_cast_succ /- unjoinable pair with function.update_eq_self:
fin.init ?m_3
↑
fin.init (function.update ?m_3 (fin.cast_succ ?m_4) (?m_3 (fin.cast_succ ?m_4)))
↓
function.update (fin.init ?m_3) ?m_4 (?m_3 (fin.cast_succ ?m_4))


unjoinable pair with function.update_eq_self:
fin.init ?m_3
↑
fin.init (function.update ?m_3 (fin.cast_succ ?m_4) (?m_3 (fin.cast_succ ?m_4)))
↓
function.update (fin.init ?m_3) ?m_4 (?m_3 (fin.cast_succ ?m_4))
 -/

-- data/fin_enum.lean
#print fin_enum.mem_to_list /- timeout -/
#print fin_enum.finset.mem_enum /- timeout -/

-- data/finmap.lean
#print multiset.coe_keys /- timeout -/
#print multiset.coe_nodupkeys /- timeout -/
#print alist.to_finmap_entries /- unjoinable pair with finmap.empty_to_finmap:
∅.entries
↑
(alist.to_finmap ∅).entries
↓
0
 -/
#print finmap.lift_on_to_finmap /- unjoinable pair with finmap.empty_to_finmap:
finmap.lift_on ∅ ?m_4 ?m_5
↑
finmap.lift_on (alist.to_finmap ∅) ?m_4 ?m_5
↓
?m_1 ∅
 -/
#print finmap.lift_on₂_to_finmap /- unjoinable pair with finmap.empty_to_finmap:
finmap.lift_on₂ ∅ (alist.to_finmap ?m_4) ?m_5 ?m_6
↑
finmap.lift_on₂ (alist.to_finmap ∅) (alist.to_finmap ?m_4) ?m_5 ?m_6
↓
?m_1 ∅ ?m_4


unjoinable pair with finmap.empty_to_finmap:
finmap.lift_on₂ (alist.to_finmap ?m_4) ∅ ?m_5 ?m_6
↑
finmap.lift_on₂ (alist.to_finmap ?m_4) (alist.to_finmap ∅) ?m_5 ?m_6
↓
?m_1 ?m_2 ∅
 -/
#print finmap.ext_iff /- timeout -/
#print finmap.mem_to_finmap /- timeout -/
#print finmap.keys_ext /- timeout -/
#print finmap.mem_singleton /- timeout -/
#print finmap.mem_replace /- timeout -/
#print finmap.mem_erase /- timeout -/
#print finmap.mem_union /- timeout -/
#print finmap.union_to_finmap /- timeout -/
#print finmap.mem_lookup_union /- timeout -/

-- data/finset.lean
#print finset.val_inj /- unjoinable pair with finset.empty_val:
0 = ?m_2.val
↑
∅.val = ?m_2.val
↓
∅ = ?m_2
 -/
#print finset.mem_mk /- timeout -/
#print finset.mem_coe /- timeout -/
#print finset.coe_inj /- timeout -/
#print finset.coe_subset /- timeout -/
#print finset.val_le_iff /- timeout -/
#print finset.le_iff_subset /- timeout -/
#print finset.lt_iff_ssubset /- timeout -/
#print finset.coe_ssubset /- timeout -/
#print finset.val_lt_iff /- timeout -/
#print finset.val_eq_zero /- timeout -/
#print finset.mem_singleton /- timeout -/
#print finset.coe_singleton /- timeout -/
#print finset.mem_insert /- timeout -/
#print finset.union_val /- timeout -/
#print finset.mem_union /- timeout -/
#print finset.coe_union /- timeout -/
#print finset.union_assoc /- timeout -/
#print finset.union_eq_left_iff_subset /- timeout -/
#print finset.left_eq_union_iff_subset /- timeout -/
#print finset.union_eq_right_iff_subset /- timeout -/
#print finset.right_eq_union_iff_subset /- timeout -/
#print finset.inter_val /- timeout -/
#print finset.mem_inter /- timeout -/
#print finset.coe_inter /- timeout -/
#print finset.union_inter_cancel_left /- timeout -/
#print finset.union_inter_cancel_right /- timeout -/
#print finset.sup_eq_union /- timeout -/
#print finset.inf_eq_inter /- timeout -/
#print finset.mem_erase /- timeout -/
#print finset.mem_sdiff /- timeout -/
#print finset.sdiff_inter_self_right /- timeout -/
#print finset.coe_sdiff /- timeout -/
#print finset.sdiff_union_self_eq_union /- timeout -/
#print finset.mem_filter /- timeout -/
#print finset.coe_filter /- timeout -/
#print finset.mem_range /- timeout -/
#print finset.range_subset /- unjoinable pair with finset.range_zero:
finset.range ?m_1 ⊆ ∅
↑
finset.range ?m_1 ⊆ finset.range 0
↓
?m_1 = 0
 -/
#print option.to_finset_some /- unjoinable pair with ennreal.some_eq_coe:
option.to_finset ↑?m_1
↑
option.to_finset (some ?m_1)
↓
finset.singleton ?m_1
 -/
#print multiset.mem_to_finset /- timeout -/
#print list.mem_to_finset /- timeout -/
#print finset.map_val /- unjoinable pair with finset.map_empty:
0
↑
(finset.map ?m_3 ∅).val
↓
0


unjoinable pair with finset.map_empty:
0
↑
(finset.map ?m_3 ∅).val
↓
0
 -/
#print finset.mem_map /- timeout -/
#print finset.mem_image /- timeout -/
#print finset.coe_image /- timeout -/
#print finset.image_eq_empty /- unjoinable pair with finset.image_empty:
finset.image ?m_3 ∅ = ∅
↑
finset.image ?m_3 ∅ = ∅
↓
true


unjoinable pair with finset.image_empty:
finset.image ?m_3 ∅ = ∅
↑
finset.image ?m_3 ∅ = ∅
↓
true
 -/
#print finset.card_eq_zero /- timeout -/
#print finset.mem_bind /- timeout -/
#print finset.mem_product /- timeout -/
#print finset.mem_sigma /- timeout -/
#print finset.mem_pi /- timeout -/
#print finset.mem_powerset /- timeout -/
#print finset.empty_mem_powerset /- timeout -/
#print finset.mem_powerset_self /- timeout -/
#print finset.sort_eq /- timeout -/
#print finset.mem_sort /- timeout -/
#print finset.singleton_disjoint /- timeout -/
#print finset.disjoint_singleton /- timeout -/
#print finset.disjoint_insert_left /- timeout -/
#print finset.disjoint_insert_right /- timeout -/
#print finset.disjoint_union_left /- timeout -/
#print finset.disjoint_union_right /- timeout -/
#print finset.Ico.to_finset /- unjoinable pair with multiset.Ico.succ_singleton:
{?m_1}
↑
multiset.to_finset (multiset.Ico ?m_1 (?m_1 + 1))
↓
finset.singleton ?m_1


unjoinable pair with multiset.Ico.succ_singleton:
{?m_1}
↑
multiset.to_finset (multiset.Ico ?m_1 (?m_1 + 1))
↓
finset.singleton ?m_1
 -/
#print finset.Ico.mem /- timeout -/
#print finset.Ico.eq_empty_iff /- timeout -/
#print finset.Ico.diff_left /- unjoinable pair with finset.Ico.succ_singleton:
finset.Ico ?m_1 ?m_2 \ finset.singleton ?m_1
↑
finset.Ico ?m_1 ?m_2 \ finset.Ico ?m_1 (?m_1 + 1)
↓
finset.Ico (?m_1 + 1) ?m_2


unjoinable pair with finset.Ico.succ_singleton:
finset.Ico ?m_1 ?m_2 \ finset.singleton ?m_1
↑
finset.Ico ?m_1 ?m_2 \ finset.Ico ?m_1 (?m_1 + 1)
↓
finset.Ico (?m_1 + 1) ?m_2
 -/
#print finset.Ico.diff_right /- unjoinable pair with finset.Ico.succ_singleton:
finset.Ico ?m_1 (?m_2 + 1) \ finset.singleton ?m_2
↑
finset.Ico ?m_1 (?m_2 + 1) \ finset.Ico ?m_2 (?m_2 + 1)
↓
finset.Ico ?m_1 ?m_2


unjoinable pair with finset.Ico.succ_singleton:
finset.Ico ?m_1 (?m_2 + 1) \ finset.singleton ?m_2
↑
finset.Ico ?m_1 (?m_2 + 1) \ finset.Ico ?m_2 (?m_2 + 1)
↓
finset.Ico ?m_1 ?m_2
 -/
#print finset.Ico_ℤ.mem /- timeout -/
#print finset.nat.mem_antidiagonal /- timeout -/

-- data/finsupp.lean
#print finsupp.mem_support_iff /- timeout -/
#print finsupp.support_eq_empty /- timeout -/
#print finsupp.unique_single_eq_iff /- timeout -/
#print finsupp.to_multiset_add /- timeout -/
#print multiset.to_finsupp_support /- unjoinable pair with finsupp.to_multiset_to_finsupp:
?m_2.support
↑
(multiset.to_finsupp (finsupp.to_multiset ?m_2)).support
↓
multiset.to_finset (finsupp.to_multiset ?m_2)
 -/
#print finsupp.add_eq_zero_iff /- timeout -/

-- data/fintype.lean
#print finset.mem_univ /- timeout -/
#print finset.mem_univ_val /- timeout -/
#print finset.coe_univ /- timeout -/
#print set.mem_to_finset /- timeout -/
#print set.mem_to_finset_val /- timeout -/
#print fintype.card_coe /- timeout -/
#print fintype.mem_pi_finset /- timeout -/

-- data/fintype/card.lean
#print fintype.card_sum /- timeout -/
#print card_vector /- timeout -/
#print finset.sum_attach_univ /- timeout -/

-- data/holor.lean
#print holor.mul_zero /- unjoinable pair with holor.zero_mul:
holor.mul 0 0
↑
holor.mul 0 0
↓
0


unjoinable pair with holor.zero_mul:
holor.mul 0 0
↑
holor.mul 0 0
↓
0
 -/

-- data/int/basic.lean
#print int.coe_nat_mul_neg_succ /- timeout -/
#print int.neg_succ_mul_neg_succ /- timeout -/
#print int.coe_nat_le /- timeout -/
#print int.coe_nat_lt /- timeout -/
#print int.coe_nat_inj' /- timeout -/
#print int.coe_nat_pos /- unjoinable pair with int.coe_nat_zero:
0 < 0
↑
0 < ↑0
↓
0 < 0
 -/
#print int.coe_nat_eq_zero /- timeout -/
#print int.coe_nat_abs /- timeout -/
#print int.nat_abs_mul_self' /- timeout -/
#print int.nat_abs_eq_zero /- timeout -/
#print int.coe_nat_div /- timeout -/
#print int.coe_nat_mod /- timeout -/
#print int.mod_abs /- unjoinable pair with euclidean_domain.mod_self:
0
↑
abs ?m_1 % abs ?m_1
↓
abs ?m_1 % ?m_1


unjoinable pair with euclidean_domain.mod_self:
0
↑
abs ?m_1 % abs ?m_1
↓
abs ?m_1 % ?m_1
 -/
#print int.add_mul_mod_self /- timeout -/
#print int.add_mul_mod_self_left /- unjoinable pair with neg_add_cancel_right:
?m_1 % ?m_2
↑
(?m_1 + -(?m_2 * ?m_3) + ?m_2 * ?m_3) % ?m_2
↓
(?m_1 + -(?m_2 * ?m_3)) % ?m_2


unjoinable pair with neg_add_cancel_right:
?m_1 % ?m_2
↑
(?m_1 + -(?m_2 * ?m_3) + ?m_2 * ?m_3) % ?m_2
↓
(?m_1 + -(?m_2 * ?m_3)) % ?m_2
 -/
#print int.add_mod_mod /- unjoinable pair with neg_add_cancel_right:
?m_1 % ?m_2
↑
(?m_1 + -(?m_2 % ?m_3) + ?m_2 % ?m_3) % ?m_3
↓
(?m_1 + (-(?m_2 % ?m_3) + ?m_2)) % ?m_3


unjoinable pair with neg_add_cancel_right:
?m_1 % ?m_2
↑
(?m_1 + -(?m_2 % ?m_3) + ?m_2 % ?m_3) % ?m_3
↓
(?m_1 + (-(?m_2 % ?m_3) + ?m_2)) % ?m_3
 -/
#print int.to_nat_coe_nat /- timeout -/
#print int.to_nat_le /- timeout -/
#print int.units_nat_abs /- timeout -/
#print int.bit_coe_nat /- timeout -/
#print int.div2_bit /- unjoinable pair with int.bit_zero:
int.div2 0
↑
int.div2 (int.bit ff 0)
↓
0


unjoinable pair with int.bit_zero:
int.div2 0
↑
int.div2 (int.bit ff 0)
↓
0
 -/
#print int.test_bit_zero /- unjoinable pair with int.bit_zero:
int.test_bit 0 0
↑
int.test_bit (int.bit ff 0) 0
↓
ff


unjoinable pair with int.bit_zero:
int.test_bit 0 0
↑
int.test_bit (int.bit ff 0) 0
↓
ff
 -/
#print int.test_bit_succ /- unjoinable pair with int.bit_zero:
int.test_bit 0 (nat.succ ?m_1)
↑
int.test_bit (int.bit ff 0) (nat.succ ?m_1)
↓
int.test_bit 0 ?m_1


unjoinable pair with int.bit_zero:
int.test_bit 0 (nat.succ ?m_1)
↑
int.test_bit (int.bit ff 0) (nat.succ ?m_1)
↓
int.test_bit 0 ?m_1
 -/
#print int.bitwise_bit /- unjoinable pair with int.bit_zero:
int.bitwise ?m_1 0 (int.bit ?m_2 ?m_3)
↑
int.bitwise ?m_1 (int.bit ff 0) (int.bit ?m_2 ?m_3)
↓
int.bit (?m_1 ff ?m_2) (int.bitwise ?m_1 0 ?m_3)


unjoinable pair with int.bit_zero:
int.bitwise ?m_1 0 (int.bit ?m_2 ?m_3)
↑
int.bitwise ?m_1 (int.bit ff 0) (int.bit ?m_2 ?m_3)
↓
int.bit (?m_1 ff ?m_2) (int.bitwise ?m_1 0 ?m_3)


unjoinable pair with int.bit_zero:
int.bitwise ?m_1 (int.bit ?m_2 ?m_3) 0
↑
int.bitwise ?m_1 (int.bit ?m_2 ?m_3) (int.bit ff 0)
↓
int.bit (?m_1 ?m_2 ff) (int.bitwise ?m_1 ?m_3 0)


unjoinable pair with int.bit_zero:
int.bitwise ?m_1 (int.bit ?m_2 ?m_3) 0
↑
int.bitwise ?m_1 (int.bit ?m_2 ?m_3) (int.bit ff 0)
↓
int.bit (?m_1 ?m_2 ff) (int.bitwise ?m_1 ?m_3 0)
 -/
#print int.lor_bit /- unjoinable pair with int.bit_zero:
int.lor 0 (int.bit ?m_1 ?m_2)
↑
int.lor (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ?m_1 (int.lor 0 ?m_2)


unjoinable pair with int.bit_zero:
int.lor 0 (int.bit ?m_1 ?m_2)
↑
int.lor (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ?m_1 (int.lor 0 ?m_2)


unjoinable pair with int.bit_zero:
int.lor (int.bit ?m_1 ?m_2) 0
↑
int.lor (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.lor ?m_2 0)


unjoinable pair with int.bit_zero:
int.lor (int.bit ?m_1 ?m_2) 0
↑
int.lor (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.lor ?m_2 0)
 -/
#print int.land_bit /- unjoinable pair with int.bit_zero:
int.land 0 (int.bit ?m_1 ?m_2)
↑
int.land (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ff (int.land 0 ?m_1)


unjoinable pair with int.bit_zero:
int.land 0 (int.bit ?m_1 ?m_2)
↑
int.land (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ff (int.land 0 ?m_1)


unjoinable pair with int.bit_zero:
int.land (int.bit ?m_1 ?m_2) 0
↑
int.land (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ff (int.land ?m_1 0)


unjoinable pair with int.bit_zero:
int.land (int.bit ?m_1 ?m_2) 0
↑
int.land (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ff (int.land ?m_1 0)
 -/
#print int.ldiff_bit /- unjoinable pair with int.bit_zero:
int.ldiff 0 (int.bit ?m_1 ?m_2)
↑
int.ldiff (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ff (int.ldiff 0 ?m_1)


unjoinable pair with int.bit_zero:
int.ldiff 0 (int.bit ?m_1 ?m_2)
↑
int.ldiff (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ff (int.ldiff 0 ?m_1)


unjoinable pair with int.bit_zero:
int.ldiff (int.bit ?m_1 ?m_2) 0
↑
int.ldiff (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.ldiff ?m_2 0)


unjoinable pair with int.bit_zero:
int.ldiff (int.bit ?m_1 ?m_2) 0
↑
int.ldiff (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.ldiff ?m_2 0)
 -/
#print int.lxor_bit /- unjoinable pair with int.bit_zero:
int.lxor 0 (int.bit ?m_1 ?m_2)
↑
int.lxor (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ?m_1 (int.lxor 0 ?m_2)


unjoinable pair with int.bit_zero:
int.lxor 0 (int.bit ?m_1 ?m_2)
↑
int.lxor (int.bit ff 0) (int.bit ?m_1 ?m_2)
↓
int.bit ?m_1 (int.lxor 0 ?m_2)


unjoinable pair with int.bit_zero:
int.lxor (int.bit ?m_1 ?m_2) 0
↑
int.lxor (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.lxor ?m_2 0)


unjoinable pair with int.bit_zero:
int.lxor (int.bit ?m_1 ?m_2) 0
↑
int.lxor (int.bit ?m_1 ?m_2) (int.bit ff 0)
↓
int.bit ?m_1 (int.lxor ?m_2 0)
 -/
#print int.lnot_bit /- unjoinable pair with int.bit_zero:
int.lnot 0
↑
int.lnot (int.bit ff 0)
↓
int.bit tt (int.lnot 0)


unjoinable pair with int.bit_zero:
int.lnot 0
↑
int.lnot (int.bit ff 0)
↓
int.bit tt (int.lnot 0)
 -/
#print int.shiftl_coe_nat /- timeout -/
#print int.shiftr_coe_nat /- timeout -/
#print int.shiftl_neg_succ /- timeout -/
#print int.shiftr_neg_succ /- unjoinable pair with int.coe_nat_zero:
int.shiftr -[1+ ?m_1] 0
↑
int.shiftr -[1+ ?m_1] ↑0
↓
-[1+ nat.shiftr ?m_1 0]
 -/
#print int.nat_cast_eq_coe_nat /- timeout -/
#print int.cast_coe_nat /- unjoinable pair with int.coe_nat_zero:
↑0
↑
↑↑0
↓
↑0
 -/
#print int.cast_neg_succ_of_nat /- timeout -/
#print int.cast_one /- timeout -/
#print int.cast_neg_of_nat /- timeout -/
#print int.cast_add /- unjoinable pair with floor_add_fract:
↑(⌊?m_2⌋ + fract ?m_2)
↑
↑(↑⌊?m_2⌋ + fract ?m_2)
↓
↑⌊?m_2⌋ + ↑(fract ?m_2)


unjoinable pair with floor_add_fract:
↑(⌊?m_2⌋ + fract ?m_2)
↑
↑(↑⌊?m_2⌋ + fract ?m_2)
↓
↑⌊?m_2⌋ + ↑(fract ?m_2)
 -/
#print int.cast_neg /- timeout -/
#print int.cast_inj /- timeout -/
#print int.cast_mul /- timeout -/
#print int.coe_nat_bit0 /- timeout -/
#print int.coe_nat_bit1 /- timeout -/
#print int.cast_bit0 /- unjoinable pair with bit0_zero:
↑0
↑
↑(bit0 0)
↓
bit0 ↑0
 -/
#print int.cast_bit1 /- unjoinable pair with bit1_zero:
↑1
↑
↑(bit1 0)
↓
bit1 ↑0
 -/
#print int.cast_le /- timeout -/
#print int.cast_lt /- timeout -/
#print int.cast_nonpos /- timeout -/
#print int.cast_pos /- timeout -/
#print int.cast_lt_zero /- timeout -/
#print int.cast_abs /- timeout -/

-- data/int/parity.lean
#print int.mod_two_ne_one /- timeout -/

-- data/list/alist.lean
#print alist.mem_erase /- timeout -/
#print alist.mem_insert /- timeout -/
#print alist.mem_lookup_union /- timeout -/

-- data/list/basic.lean
#print list.mem_singleton /- timeout -/
#print list.mem_map /- timeout -/
#print list.map_eq_nil /- timeout -/
#print list.mem_join /- timeout -/
#print list.mem_bind /- timeout -/
#print list.append_eq_nil /- timeout -/
#print list.nil_eq_append_iff /- timeout -/
#print list.take_append_drop /- unjoinable pair with list.drop_one:
list.take 1 ?m_2 ++ list.tail ?m_2
↑
list.take 1 ?m_2 ++ list.drop 1 ?m_2
↓
?m_1


unjoinable pair with list.drop_one:
list.take 1 ?m_2 ++ list.tail ?m_2
↑
list.take 1 ?m_2 ++ list.drop 1 ?m_2
↓
?m_1
 -/
#print list.mem_pure /- timeout -/
#print list.bind_append /- unjoinable pair with list.append_nil:
list.bind ?m_3 ?m_4
↑
list.bind (?m_3 ++ list.nil) ?m_4
↓
list.bind ?m_2 ?m_3


unjoinable pair with list.append_nil:
list.bind ?m_3 ?m_4
↑
list.bind (?m_3 ++ list.nil) ?m_4
↓
list.bind ?m_2 ?m_3
 -/
#print list.reverse_inj /- timeout -/
#print list.mem_reverse /- timeout -/
#print list.last_cons /- unjoinable pair with list.last_singleton:
?m_1
↑
list.last [?m_2] ?m_3
↓
absurd _ _
 -/
#print list.append_sublist_append_left /- unjoinable pair with list.append_nil:
?m_2 ++ ?m_3 <+ ?m_2
↑
?m_2 ++ ?m_3 <+ ?m_2 ++ list.nil
↓
?m_2 <+ list.nil


unjoinable pair with list.append_nil:
?m_2 ++ ?m_3 <+ ?m_2
↑
?m_2 ++ ?m_3 <+ ?m_2 ++ list.nil
↓
?m_2 <+ list.nil
 -/
#print list.reverse_sublist_iff /- unjoinable pair with list.reverse_reverse:
?m_2 <+ list.reverse ?m_3
↑
list.reverse (list.reverse ?m_2) <+ list.reverse ?m_3
↓
list.reverse ?m_2 <+ ?m_3


unjoinable pair with list.reverse_reverse:
list.reverse ?m_2 <+ ?m_3
↑
list.reverse ?m_2 <+ list.reverse (list.reverse ?m_3)
↓
?m_2 <+ list.reverse ?m_3
 -/
#print list.nth_concat_length /- unjoinable pair with list.length_fin_range:
list.nth (list.fin_range ?m_1 ++ [?m_2]) ?m_1
↑
list.nth (list.fin_range ?m_1 ++ [?m_2]) (list.length (list.fin_range ?m_1))
↓
↑?m_2
 -/
#print list.nth_le_reverse /- unjoinable pair with list.reverse_reverse:
list.nth_le ?m_2 (list.length ?m_2 - 1 - ?m_3) _
↑
list.nth_le (list.reverse (list.reverse ?m_2)) (list.length (list.reverse ?m_2) - 1 - ?m_3) ?m_4
↓
list.nth_le (list.reverse ?m_2) ?m_3 ?m_4


unjoinable pair with nat.sub_self:
list.nth_le (list.reverse ?m_2) 0 _
↑
list.nth_le (list.reverse ?m_2) (list.length ?m_2 - 1 - (list.length ?m_2 - 1)) ?m_3
↓
list.nth_le ?m_2 (list.length ?m_2 - 1) ?m_3


unjoinable pair with list.length_fin_range:
list.nth_le (list.reverse (list.fin_range ?m_1)) (?m_1 - 1 - ?m_2) _
↑
list.nth_le (list.reverse (list.fin_range ?m_1)) (list.length (list.fin_range ?m_1) - 1 - ?m_2) ?m_3
↓
list.nth_le (list.fin_range ?m_1) ?m_2 ?m_3


unjoinable pair with nat.sub_self:
list.nth_le (list.reverse ?m_2) 0 _
↑
list.nth_le (list.reverse ?m_2) (list.length ?m_2 - 1 - (list.length ?m_2 - 1)) ?m_3
↓
list.nth_le ?m_2 (list.length ?m_2 - 1) ?m_3
 -/
#print list.foldr_map /- unjoinable pair with list.foldr_eta:
list.map ?m_3 ?m_4
↑
list.foldr list.cons list.nil (list.map ?m_3 ?m_4)
↓
list.foldr (list.cons ∘ ?m_3) list.nil ?m_4


unjoinable pair with list.foldr_eta:
list.map ?m_3 ?m_4
↑
list.foldr list.cons list.nil (list.map ?m_3 ?m_4)
↓
list.foldr (list.cons ∘ ?m_3) list.nil ?m_4


unjoinable pair with list.foldr_eta:
list.map ?m_3 ?m_4
↑
list.foldr list.cons list.nil (list.map ?m_3 ?m_4)
↓
list.foldr (list.cons ∘ ?m_3) list.nil ?m_4
 -/
#print list.take_all /- unjoinable pair with list.length_fin_range:
list.take ?m_1 (list.fin_range ?m_1)
↑
list.take (list.length (list.fin_range ?m_1)) (list.fin_range ?m_1)
↓
list.fin_range ?m_1
 -/
#print list.take_left /- unjoinable pair with list.length_fin_range:
list.take ?m_1 (list.fin_range ?m_1 ++ ?m_2)
↑
list.take (list.length (list.fin_range ?m_1)) (list.fin_range ?m_1 ++ ?m_2)
↓
list.fin_range ?m_1
 -/
#print list.drop_left /- unjoinable pair with list.length_fin_range:
list.drop ?m_1 (list.fin_range ?m_1 ++ ?m_2)
↑
list.drop (list.length (list.fin_range ?m_1)) (list.fin_range ?m_1 ++ ?m_2)
↓
?m_1
 -/
#print list.drop_all /- unjoinable pair with list.length_fin_range:
list.drop ?m_1 (list.fin_range ?m_1)
↑
list.drop (list.length (list.fin_range ?m_1)) (list.fin_range ?m_1)
↓
list.nil
 -/
#print list.drop_drop /- unjoinable pair with list.drop_one:
list.drop ?m_2 (list.tail ?m_3)
↑
list.drop ?m_2 (list.drop 1 ?m_3)
↓
list.drop (?m_2 + 1) ?m_3


unjoinable pair with list.drop_one:
list.drop ?m_2 (list.tail ?m_3)
↑
list.drop ?m_2 (list.drop 1 ?m_3)
↓
list.drop (?m_2 + 1) ?m_3
 -/
#print list.foldr_append /- unjoinable pair with list.foldr_eta:
?m_2 ++ ?m_3
↑
list.foldr list.cons list.nil (?m_2 ++ ?m_3)
↓
list.foldr list.cons ?m_2 ?m_3


unjoinable pair with list.foldr_eta:
?m_2 ++ ?m_3
↑
list.foldr list.cons list.nil (?m_2 ++ ?m_3)
↓
list.foldr list.cons ?m_2 ?m_3


unjoinable pair with list.foldr_eta:
?m_2 ++ ?m_3
↑
list.foldr list.cons list.nil (?m_2 ++ ?m_3)
↓
list.foldr list.cons ?m_2 ?m_3
 -/
#print list.foldr_join /- unjoinable pair with list.foldr_eta:
list.join ?m_2
↑
list.foldr list.cons list.nil (list.join ?m_2)
↓
list.foldr (λ (l b : list ?m_1), list.foldr list.cons b l) list.nil ?m_2


unjoinable pair with list.foldr_eta:
list.join ?m_2
↑
list.foldr list.cons list.nil (list.join ?m_2)
↓
list.foldr (λ (l b : list ?m_1), list.foldr list.cons b l) list.nil ?m_2


unjoinable pair with list.foldr_eta:
list.join ?m_2
↑
list.foldr list.cons list.nil (list.join ?m_2)
↓
list.foldr (λ (l b : list ?m_1), list.foldr list.cons b l) list.nil ?m_2
 -/
#print list.sum_append /- unjoinable pair with list.append_nil:
list.sum ?m_2
↑
list.sum (?m_2 ++ list.nil)
↓
list.sum ?m_2 + list.sum list.nil


unjoinable pair with list.append_nil:
list.sum ?m_2
↑
list.sum (?m_2 ++ list.nil)
↓
list.sum ?m_2 + list.sum list.nil
 -/
#print list.prod_append /- unjoinable pair with list.append_nil:
list.prod ?m_2
↑
list.prod (?m_2 ++ list.nil)
↓
list.prod ?m_2 * list.prod list.nil


unjoinable pair with list.append_nil:
list.prod ?m_2
↑
list.prod (?m_2 ++ list.nil)
↓
list.prod ?m_2 * list.prod list.nil
 -/
#print list.mem_attach /- timeout -/
#print list.find_eq_none /- timeout -/
#print list.mem_filter_map /- timeout -/
#print list.mem_filter /- timeout -/
#print list.prefix_append /- unjoinable pair with list.append_nil:
?m_2 <+: ?m_2
↑
?m_2 <+: ?m_2 ++ list.nil
↓
true


unjoinable pair with list.append_nil:
?m_2 <+: ?m_2
↑
?m_2 <+: ?m_2 ++ list.nil
↓
true
 -/
#print list.suffix_append /- unjoinable pair with list.append_nil:
list.nil <:+ ?m_2
↑
list.nil <:+ ?m_2 ++ list.nil
↓
true


unjoinable pair with list.append_nil:
list.nil <:+ ?m_2
↑
list.nil <:+ ?m_2 ++ list.nil
↓
true
 -/
#print list.infix_append' /- unjoinable pair with list.append_nil:
?m_2 <:+: ?m_3 ++ ?m_2
↑
?m_2 <:+: ?m_3 ++ (?m_2 ++ list.nil)
↓
true


unjoinable pair with list.append_nil:
?m_2 <:+: ?m_3 ++ ?m_2
↑
?m_2 <:+: ?m_3 ++ (?m_2 ++ list.nil)
↓
true
 -/
#print list.mem_sublists' /- timeout -/
#print list.mem_sublists /- timeout -/
#print list.mem_sublists_len /- timeout -/
#print list.mem_insert_iff /- timeout -/
#print list.mem_insert_self /- timeout -/
#print list.unzip_cons /- unjoinable pair with prod.mk.eta:
list.unzip (?m_3 :: ?m_4)
↑
list.unzip ((?m_3.fst, ?m_3.snd) :: ?m_4)
↓
(?m_3.fst :: (list.unzip ?m_4).fst, ?m_3.snd :: (list.unzip ?m_4).snd)


unjoinable pair with prod.mk.eta:
list.unzip (?m_3 :: ?m_4)
↑
list.unzip ((?m_3.fst, ?m_3.snd) :: ?m_4)
↓
(?m_3.fst :: (list.unzip ?m_4).fst, ?m_3.snd :: (list.unzip ?m_4).snd)
 -/
#print list.mem_product /- timeout -/
#print list.mem_sigma /- timeout -/
#print list.nth_le_of_fn /- unjoinable pair with fin.last_val:
list.nth_le (list.of_fn ?m_3) ?m_2 _
↑
list.nth_le (list.of_fn ?m_3) (fin.last ?m_2).val _
↓
?m_1 (fin.last ?m_2)
 -/
#print list.mem_inter /- timeout -/
#print list.mem_erase_dup /- timeout -/
#print list.mem_fin_range /- timeout -/
#print list.Ico.mem /- timeout -/
#print list.Ico.inter_consecutive /- unjoinable pair with list.Ico.succ_singleton:
list.Ico ?m_1 ?m_2 ∩ [?m_2]
↑
list.Ico ?m_1 ?m_2 ∩ list.Ico ?m_2 (?m_2 + 1)
↓
list.nil


unjoinable pair with list.Ico.succ_singleton:
list.Ico ?m_1 ?m_2 ∩ [?m_2]
↑
list.Ico ?m_1 ?m_2 ∩ list.Ico ?m_2 (?m_2 + 1)
↓
list.nil
 -/
#print list.Ico.bag_inter_consecutive /- unjoinable pair with list.Ico.succ_singleton:
list.bag_inter (list.Ico ?m_1 ?m_2) [?m_2]
↑
list.bag_inter (list.Ico ?m_1 ?m_2) (list.Ico ?m_2 (?m_2 + 1))
↓
list.nil


unjoinable pair with list.Ico.succ_singleton:
list.bag_inter (list.Ico ?m_1 ?m_2) [?m_2]
↑
list.bag_inter (list.Ico ?m_1 ?m_2) (list.Ico ?m_2 (?m_2 + 1))
↓
list.nil
 -/
#print list.rotate'_length /- unjoinable pair with list.length_fin_range:
list.rotate' (list.fin_range ?m_1) ?m_1
↑
list.rotate' (list.fin_range ?m_1) (list.length (list.fin_range ?m_1))
↓
list.fin_range ?m_1
 -/
#print list.rotate'_length_mul /- unjoinable pair with list.length_fin_range:
list.rotate' (list.fin_range ?m_1) (?m_1 * ?m_2)
↑
list.rotate' (list.fin_range ?m_1) (list.length (list.fin_range ?m_1) * ?m_2)
↓
list.fin_range ?m_1
 -/
#print list.rotate_length /- unjoinable pair with list.length_fin_range:
list.rotate (list.fin_range ?m_1) ?m_1
↑
list.rotate (list.fin_range ?m_1) (list.length (list.fin_range ?m_1))
↓
list.fin_range ?m_1
 -/
#print list.rotate_length_mul /- unjoinable pair with list.length_fin_range:
list.rotate (list.fin_range ?m_1) (?m_1 * ?m_2)
↑
list.rotate (list.fin_range ?m_1) (list.length (list.fin_range ?m_1) * ?m_2)
↓
list.fin_range ?m_1
 -/
#print list.nat.mem_antidiagonal /- timeout -/

-- data/list/min_max.lean
#print list.foldl_argmax₂_eq_none /- timeout -/
#print list.maximum_eq_none /- timeout -/
#print list.minimum_eq_none /- timeout -/

-- data/list/perm.lean
#print list.perm_app_comm /- unjoinable pair with list.append_nil:
?m_2 ~ ?m_2
↑
?m_2 ++ list.nil ~ list.nil ++ ?m_2
↓
true


unjoinable pair with list.append_nil:
?m_2 ~ ?m_2
↑
?m_2 ++ list.nil ~ list.nil ++ ?m_2
↓
true


unjoinable pair with list.append_nil:
?m_2 ~ ?m_2
↑
list.nil ++ ?m_2 ~ ?m_2 ++ list.nil
↓
true


unjoinable pair with list.append_nil:
?m_2 ~ ?m_2
↑
list.nil ++ ?m_2 ~ ?m_2 ++ list.nil
↓
true
 -/
#print list.reverse_perm /- unjoinable pair with list.reverse_reverse:
?m_2 ~ list.reverse ?m_2
↑
list.reverse (list.reverse ?m_2) ~ list.reverse ?m_2
↓
true
 -/
#print list.mem_permutations /- timeout -/

-- data/list/sigma.lean
#print list.mem_keys_kunion /- timeout -/
#print list.mem_lookup_kunion /- timeout -/

-- data/matrix/basic.lean
#print matrix.add_val /- timeout -/
#print matrix.mul_eq_mul /- timeout -/

-- data/matrix/pequiv.lean
#print pequiv.single_mul_single_right /- timeout -/

-- data/multiset.lean
#print multiset.coe_eq_coe /- timeout -/
#print multiset.coe_nil_eq_zero /- timeout -/
#print multiset.cons_coe /- timeout -/
#print multiset.cons_inj_left /- timeout -/
#print multiset.cons_inj_right /- timeout -/
#print multiset.mem_coe /- timeout -/
#print multiset.coe_subset /- timeout -/
#print multiset.coe_le /- timeout -/
#print multiset.coe_card /- timeout -/
#print multiset.mem_singleton /- timeout -/
#print multiset.coe_add /- timeout -/
#print multiset.cons_add /- timeout -/
#print multiset.card_add /- timeout -/
#print multiset.mem_range /- timeout -/
#print multiset.erase_lt /- timeout -/
#print multiset.map_add /- timeout -/
#print multiset.mem_map /- timeout -/
#print multiset.map_eq_zero /- timeout -/
#print multiset.foldl_add /- timeout -/
#print multiset.coe_foldr /- timeout -/
#print multiset.coe_prod /- timeout -/
#print multiset.coe_sum /- timeout -/
#print multiset.sum_add /- timeout -/
#print multiset.join_add /- timeout -/
#print multiset.mem_join /- timeout -/
#print multiset.coe_bind /- unjoinable pair with multiset.coe_bind:
↑(list.bind ?m_3 ?m_4)
↑
multiset.bind ↑?m_3 (λ (a : ?m_1), ↑(?m_4 a))
↓
↑(list.bind ?m_3 ?m_4)


unjoinable pair with multiset.coe_bind:
↑(list.bind ?m_3 ?m_4)
↑
multiset.bind ↑?m_3 (λ (a : ?m_1), ↑(?m_4 a))
↓
↑(list.bind ?m_3 ?m_4)
 -/
#print multiset.cons_bind /- unjoinable pair with multiset.bind_zero:
0
↑
multiset.bind (?m_3 :: ?m_4) (λ (a : ?m_1), 0)
↓
0 + 0


unjoinable pair with multiset.bind_zero:
0
↑
multiset.bind (?m_3 :: ?m_4) (λ (a : ?m_1), 0)
↓
0 + 0
 -/
#print multiset.add_bind /- timeout -/
#print multiset.mem_bind /- timeout -/
#print multiset.coe_product /- timeout -/
#print multiset.product_singleton /- unjoinable pair with multiset.cons_product:
(?m_2, ?m_3) :: 0
↑
multiset.product (?m_3 :: 0) (?m_4 :: 0)
↓
(?m_3, ?m_4) :: 0


unjoinable pair with multiset.cons_product:
(?m_2, ?m_3) :: 0
↑
multiset.product (?m_3 :: 0) (?m_4 :: 0)
↓
(?m_3, ?m_4) :: 0
 -/
#print multiset.mem_product /- timeout -/
#print multiset.coe_sigma /- timeout -/
#print multiset.mem_sigma /- timeout -/
#print multiset.mem_attach /- timeout -/
#print multiset.mem_pmap /- timeout -/
#print multiset.coe_sub /- timeout -/
#print multiset.sub_cons /- unjoinable pair with multiset.add_sub_cancel:
?m_2 :: (?m_3 + ?m_4) - ?m_2 :: ?m_4
↑
?m_2 + ?m_3 :: ?m_4 - ?m_3 :: ?m_4
↓
multiset.erase (?m_2 :: (?m_3 + ?m_4)) ?m_2 - ?m_4


unjoinable pair with multiset.add_sub_cancel:
?m_2 :: (?m_3 + ?m_4) - ?m_2 :: ?m_4
↑
?m_2 + ?m_3 :: ?m_4 - ?m_3 :: ?m_4
↓
multiset.erase (?m_2 :: (?m_3 + ?m_4)) ?m_2 - ?m_4
 -/
#print multiset.add_sub_cancel_left /- timeout -/
#print multiset.sup_eq_union /- timeout -/
#print multiset.inf_eq_inter /- timeout -/
#print multiset.le_inter_iff /- timeout -/
#print multiset.union_le_iff /- timeout -/
#print multiset.coe_filter /- timeout -/
#print multiset.filter_le /- timeout -/
#print multiset.mem_filter /- timeout -/
#print multiset.coe_filter_map /- timeout -/
#print multiset.mem_filter_map /- timeout -/
#print multiset.powerset_coe' /- timeout -/
#print multiset.mem_powerset /- timeout -/
#print multiset.antidiagonal_coe' /- timeout -/
#print multiset.mem_antidiagonal /- timeout -/
#print multiset.mem_powerset_len_aux /- timeout -/
#print multiset.mem_powerset_len /- unjoinable pair with multiset.powerset_len_zero_left:
?m_2 = 0
↑
?m_2 ∈ multiset.powerset_len 0 ?m_3
↓
?m_2 ≤ ?m_3 ∧ ?m_2 = 0


unjoinable pair with multiset.powerset_len_zero_left:
?m_2 = 0
↑
?m_2 ∈ multiset.powerset_len 0 ?m_3
↓
?m_2 ≤ ?m_3 ∧ ?m_2 = 0
 -/
#print multiset.coe_countp /- timeout -/
#print multiset.countp_add /- timeout -/
#print multiset.coe_count /- timeout -/
#print multiset.coe_inter /- timeout -/
#print multiset.coe_disjoint /- timeout -/
#print multiset.disjoint_add_left /- timeout -/
#print multiset.coe_nodup /- timeout -/
#print multiset.nodup_bind /- unjoinable pair with multiset.zero_bind:
true
↑
multiset.nodup (multiset.bind 0 ?m_3)
↓
multiset.pairwise (λ (a b : ?m_1), multiset.disjoint (?m_3 a) (?m_3 b)) 0


unjoinable pair with multiset.zero_bind:
true
↑
multiset.nodup (multiset.bind 0 ?m_3)
↓
multiset.pairwise (λ (a b : ?m_1), multiset.disjoint (?m_3 a) (?m_3 b)) 0
 -/
#print multiset.coe_ndinsert /- timeout -/
#print multiset.mem_ndinsert /- timeout -/
#print multiset.le_ndinsert_self /- timeout -/
#print multiset.mem_ndinsert_self /- timeout -/
#print multiset.coe_ndunion /- timeout -/
#print multiset.mem_ndunion /- timeout -/
#print multiset.coe_ndinter /- timeout -/
#print multiset.mem_ndinter /- timeout -/
#print multiset.coe_fold_r /- timeout -/
#print multiset.sup_add /- timeout -/
#print multiset.coe_sort /- timeout -/
#print multiset.sort_eq /- timeout -/
#print multiset.mem_sort /- timeout -/
#print multiset.lift_beta /- timeout -/
#print multiset.Ico.mem /- unjoinable pair with multiset.Ico.succ_singleton:
?m_1 = ?m_2
↑
?m_1 ∈ multiset.Ico ?m_2 (?m_2 + 1)
↓
?m_1 ≤ ?m_2 ∧ ?m_2 < ?m_1 + 1


unjoinable pair with multiset.Ico.succ_singleton:
?m_1 = ?m_2
↑
?m_1 ∈ multiset.Ico ?m_2 (?m_2 + 1)
↓
?m_1 ≤ ?m_2 ∧ ?m_2 < ?m_1 + 1
 -/
#print multiset.Ico.inter_consecutive /- unjoinable pair with multiset.Ico.succ_singleton:
multiset.Ico ?m_1 ?m_2 ∩ (?m_2 :: 0)
↑
multiset.Ico ?m_1 ?m_2 ∩ multiset.Ico ?m_2 (?m_2 + 1)
↓
0


unjoinable pair with multiset.Ico.succ_singleton:
multiset.Ico ?m_1 ?m_2 ∩ (?m_2 :: 0)
↑
multiset.Ico ?m_1 ?m_2 ∩ multiset.Ico ?m_2 (?m_2 + 1)
↓
0
 -/
#print multiset.nat.mem_antidiagonal /- timeout -/

-- data/mv_polynomial.lean
#print mv_polynomial.C_mul /- timeout -/
#print mv_polynomial.coeff_C_mul /- timeout -/
#print mv_polynomial.coeff_mul_X /- timeout -/
#print mv_polynomial.eval₂_add /- timeout -/
#print mv_polynomial.map_mul /- timeout -/
#print mv_polynomial.eval₂_hom_X /- unjoinable pair with function.comp.left_id:
mv_polynomial.eval₂ ?m_2 mv_polynomial.X ?m_3
↑
mv_polynomial.eval₂ ?m_2 (id ∘ mv_polynomial.X) ?m_3
↓
?m_1


unjoinable pair with function.comp.left_id:
mv_polynomial.eval₂ ?m_2 mv_polynomial.X ?m_3
↑
mv_polynomial.eval₂ ?m_2 (id ∘ mv_polynomial.X) ?m_3
↓
?m_1
 -/

-- data/nat/basic.lean
#print nat.pred_eq_succ_iff /- unjoinable pair with nat.pred_zero:
0 = nat.succ ?m_1
↑
nat.pred 0 = nat.succ ?m_1
↓
0 = ?m_1 + 2
 -/
#print nat.zero_eq_mul /- timeout -/
#print nat.ppred_eq_some /- timeout -/
#print nat.ppred_eq_none /- timeout -/

-- data/nat/cast.lean
#print nat.cast_succ /- timeout -/
#print nat.cast_one /- timeout -/
#print nat.cast_add /- timeout -/
#print nat.cast_bit1 /- timeout -/
#print nat.cast_mul /- timeout -/
#print nat.cast_nonneg /- timeout -/
#print nat.cast_le /- timeout -/
#print nat.cast_lt /- timeout -/
#print nat.cast_pos /- timeout -/
#print nat.cast_id /- timeout -/
#print nat.cast_min /- timeout -/
#print nat.cast_max /- timeout -/
#print nat.abs_cast /- timeout -/

-- data/nat/enat.lean
#print enat.coe_inj /- timeout -/
#print enat.coe_zero /- timeout -/
#print enat.coe_add /- timeout -/
#print enat.get_add /- timeout -/
#print enat.coe_le_coe /- timeout -/
#print enat.coe_lt_coe /- timeout -/
#print enat.to_with_top_coe' /- unjoinable pair with enat.coe_one:
enat.to_with_top 1
↑
enat.to_with_top ↑1
↓
1
 -/
#print enat.to_with_top_le /- timeout -/
#print enat.with_top_equiv_symm_le /- timeout -/

-- data/nat/modeq.lean
#print nat.mod_mul_left_mod /- timeout -/

-- data/nat/parity.lean
#print nat.mod_two_ne_one /- timeout -/
#print nat.mod_two_ne_zero /- timeout -/

-- data/num/lemmas.lean
#print pos_num.cast_one' /- timeout -/
#print pos_num.cast_bit0 /- timeout -/
#print pos_num.cast_bit1 /- timeout -/
#print pos_num.cast_to_nat /- unjoinable pair with pos_num.cast_one:
↑1
↑
↑↑1
↓
↑1
 -/
#print pos_num.to_nat_to_int /- timeout -/
#print pos_num.cast_to_int /- unjoinable pair with pos_num.cast_one:
↑1
↑
↑↑1
↓
↑1
 -/
#print num.add_of_nat /- timeout -/
#print num.cast_zero' /- timeout -/
#print num.cast_to_nat /- timeout -/
#print num.to_nat_to_int /- timeout -/
#print num.cast_to_int /- unjoinable pair with num.cast_zero:
↑0
↑
↑↑0
↓
↑0
 -/
#print num.of_nat_cast /- timeout -/
#print pos_num.of_to_nat /- unjoinable pair with pos_num.cast_one:
1
↑
↑↑1
↓
num.pos 1
 -/
#print num.of_to_nat /- timeout -/
#print pos_num.cast_to_num /- timeout -/
#print pos_num.cast_add /- timeout -/
#print pos_num.cast_succ /- timeout -/
#print pos_num.cast_inj /- timeout -/
#print pos_num.one_le_cast /- timeout -/
#print pos_num.cast_pos /- timeout -/
#print pos_num.cast_mul /- timeout -/
#print pos_num.cast_lt /- timeout -/
#print pos_num.cast_le /- timeout -/
#print num.cast_add /- timeout -/
#print num.cast_bit0 /- timeout -/
#print num.cast_bit1 /- timeout -/
#print num.cast_mul /- timeout -/
#print num.cast_to_znum_neg /- timeout -/
#print num.add_to_znum /- unjoinable pair with add_zero:
num.to_znum ?m_1
↑
num.to_znum (?m_1 + 0)
↓
num.to_znum ?m_1 + num.to_znum 0


unjoinable pair with add_zero:
num.to_znum ?m_1
↑
num.to_znum (?m_1 + 0)
↓
num.to_znum ?m_1 + num.to_znum 0
 -/
#print num.cast_lt /- timeout -/
#print num.cast_le /- timeout -/
#print num.cast_inj /- timeout -/
#print num.lor_to_nat /- timeout -/
#print num.land_to_nat /- timeout -/
#print num.ldiff_to_nat /- timeout -/
#print num.lxor_to_nat /- timeout -/
#print num.shiftl_to_nat /- timeout -/
#print num.shiftr_to_nat /- timeout -/
#print znum.cast_one /- timeout -/
#print znum.cast_pos /- timeout -/
#print znum.cast_zneg /- timeout -/
#print znum.abs_to_nat /- timeout -/
#print znum.cast_to_int /- timeout -/
#print znum.cast_bit0 /- timeout -/
#print num.cast_sub' /- timeout -/
#print num.of_nat_to_znum /- timeout -/
#print num.of_nat_to_znum_neg /- timeout -/
#print num.sub_to_nat /- timeout -/
#print znum.cast_add /- timeout -/
#print znum.cast_succ /- timeout -/
#print znum.mul_to_int /- timeout -/
#print znum.of_to_int /- timeout -/
#print znum.of_int_cast /- unjoinable pair with int.cast_zero:
↑0
↑
↑↑0
↓
↑0
 -/
#print znum.of_nat_cast /- unjoinable pair with nat.cast_zero:
↑0
↑
↑↑0
↓
↑0
 -/
#print znum.cast_lt /- timeout -/
#print znum.cast_le /- timeout -/
#print znum.cast_inj /- timeout -/
#print znum.dvd_to_int /- unjoinable pair with znum.cast_zero':
↑?m_1 = 0
↑
↑znum.zero ∣ ↑?m_1
↓
znum.zero ∣ ?m_1


unjoinable pair with znum.cast_zero':
true
↑
↑?m_1 ∣ ↑znum.zero
↓
?m_1 ∣ znum.zero
 -/
#print pos_num.mod'_to_nat /- timeout -/
#print num.mod_to_nat /- timeout -/
#print num.gcd_to_nat /- timeout -/
#print znum.gcd_to_nat /- timeout -/

-- data/opposite.lean
#print opposite.op_inj_iff /- timeout -/
#print opposite.unop_inj_iff /- unjoinable pair with opposite.unop_op:
?m_2 = opposite.unop ?m_3
↑
opposite.unop (opposite.op ?m_2) = opposite.unop ?m_3
↓
opposite.op ?m_2 = ?m_3


unjoinable pair with opposite.unop_op:
opposite.unop ?m_2 = ?m_3
↑
opposite.unop ?m_2 = opposite.unop (opposite.op ?m_3)
↓
?m_2 = opposite.op ?m_3
 -/

-- data/option/basic.lean
#print option.get_mem /- timeout -/
#print option.some_bind /- unjoinable pair with ennreal.some_eq_coe:
↑?m_2 >>= ?m_3
↑
some ?m_2 >>= ?m_3
↓
?m_1 ?m_2
 -/
#print option.some_bind' /- unjoinable pair with ennreal.some_eq_coe:
option.bind ↑?m_2 ?m_3
↑
option.bind (some ?m_2) ?m_3
↓
?m_1 ?m_2
 -/
#print option.bind_eq_some /- timeout -/
#print option.bind_eq_some' /- timeout -/
#print option.bind_eq_none' /- unjoinable pair with option.bind_eq_none':
∀ (b : ?m_1) (a : ?m_2), ?m_3 = some a → ¬?m_4 a = some b
↑
option.bind ?m_3 ?m_4 = none
↓
∀ (b : ?m_1) (a : ?m_2), ?m_3 = some a → b ∉ ?m_4 a


unjoinable pair with option.bind_eq_none':
∀ (b : ?m_1) (a : ?m_2), ?m_3 = some a → ¬?m_4 a = some b
↑
option.bind ?m_3 ?m_4 = none
↓
∀ (b : ?m_1) (a : ?m_2), ?m_3 = some a → b ∉ ?m_4 a
 -/
#print option.bind_eq_none /- timeout -/
#print option.map_some /- unjoinable pair with ennreal.some_eq_coe:
?m_2 <$> ↑?m_3
↑
?m_2 <$> some ?m_3
↓
some (?m_2 ?m_3)
 -/
#print option.map_some' /- unjoinable pair with ennreal.some_eq_coe:
option.map ?m_2 ↑?m_3
↑
option.map ?m_2 (some ?m_3)
↓
some (?m_2 ?m_3)
 -/
#print option.map_eq_some /- unjoinable pair with ennreal.some_eq_coe:
?m_2 <$> ?m_3 = ↑?m_4
↑
?m_2 <$> ?m_3 = some ?m_4
↓
∃ (a : ?m_1), ?m_2 = some a ∧ ?m_3 a = ?m_4
 -/
#print option.map_eq_some' /- timeout -/
#print option.seq_some /- unjoinable pair with ennreal.some_eq_coe:
some ?m_2 <*> ↑?m_3
↑
some ?m_2 <*> some ?m_3
↓
some (?m_2 ?m_3)
 -/
#print option.some_orelse' /- unjoinable pair with ennreal.some_eq_coe:
option.orelse ↑?m_1 ?m_2
↑
option.orelse (some ?m_1) ?m_2
↓
↑?m_1
 -/
#print option.some_orelse /- unjoinable pair with ennreal.some_eq_coe:
↑?m_1 <|> ?m_2
↑
some ?m_1 <|> ?m_2
↓
↑?m_1
 -/
#print option.is_some_some /- unjoinable pair with ennreal.some_eq_coe:
option.is_some ↑?m_1
↑
option.is_some (some ?m_1)
↓
tt
 -/
#print option.is_none_some /- unjoinable pair with ennreal.some_eq_coe:
option.is_none ↑?m_1
↑
option.is_none (some ?m_1)
↓
ff
 -/
#print option.not_is_some /- timeout -/
#print option.guard_eq_some /- timeout -/
#print option.lift_or_get_some_some /- unjoinable pair with ennreal.some_eq_coe:
option.lift_or_get ?m_1 ↑?m_2 ↑?m_3
↑
option.lift_or_get ?m_1 (some ?m_2) (some ?m_3)
↓
↑(?m_1 ?m_2 ?m_3)


unjoinable pair with ennreal.some_eq_coe:
option.lift_or_get ?m_1 ↑?m_2 ↑?m_3
↑
option.lift_or_get ?m_1 (some ?m_2) (some ?m_3)
↓
↑(?m_1 ?m_2 ?m_3)
 -/

-- data/option/defs.lean
#print option.mem_def /- timeout -/
#print option.mem_to_list /- timeout -/

-- data/padics/padic_integers.lean
#print padic_int.val_eq_coe /- timeout -/
#print padic_int.coe_add /- timeout -/
#print padic_int.coe_mul /- timeout -/
#print padic_int.coe_neg /- timeout -/
#print padic_int.coe_sub /- timeout -/
#print padic_int.coe_one /- timeout -/
#print padic_int.coe_coe /- timeout -/
#print padic_int.coe_zero /- timeout -/
#print padic_int.cast_pow /- timeout -/
#print padic_norm_z.mul /- timeout -/
#print padic_norm_z.pow /- timeout -/
#print padic_norm_z.padic_norm_e_of_padic_int /- timeout -/
#print padic_norm_z.padic_norm_z_eq_padic_norm_e /- timeout -/
#print padic_int.mem_nonunits /- timeout -/

-- data/padics/padic_norm.lean
#print padic_norm.neg /- unjoinable pair with neg_neg:
padic_norm ?m_1 ?m_2
↑
padic_norm ?m_1 (- -?m_2)
↓
padic_norm ?m_1 (-?m_2)
 -/

-- data/padics/padic_numbers.lean
#print padic.cast_eq_of_rat_of_nat /- timeout -/
#print padic_norm_e.mul /- timeout -/
#print padic_norm_e.eq_padic_norm /- timeout -/

-- data/pequiv.lean
#print pequiv.symm_symm /- unjoinable pair with pequiv.symm_bot:
⊥
↑
pequiv.symm (pequiv.symm ⊥)
↓
⊥
 -/
#print pequiv.of_set_eq_some_iff /- unjoinable pair with ennreal.some_eq_coe:
⇑(pequiv.of_set ?m_1) ?m_3 = ↑?m_4
↑
⇑(pequiv.of_set ?m_1) ?m_3 = some ?m_4
↓
?m_1 = ?m_2 ∧ ?m_1 ∈ ?m_3
 -/
#print pequiv.of_set_eq_some_self_iff /- timeout -/

-- data/pfun.lean
#print roption.mem_some_iff /- timeout -/
#print roption.some_get /- unjoinable pair with enat.get_one:
roption.some 1
↑
roption.some (1.get ?m_1)
↓
1
 -/
#print roption.mem_to_option /- timeout -/
#print roption.mem_of_option /- timeout -/
#print roption.mem_coe /- timeout -/
#print roption.coe_none /- timeout -/
#print roption.coe_some /- timeout -/
#print roption.mem_map_iff /- timeout -/
#print roption.mem_assert_iff /- timeout -/
#print roption.mem_bind_iff /- timeout -/
#print roption.bind_map /- unjoinable pair with roption.bind_some_right:
roption.map ?m_3 ?m_4
↑
roption.bind (roption.map ?m_3 ?m_4) roption.some
↓
roption.bind ?m_3 (λ (y : ?m_1), roption.some (?m_4 y))


unjoinable pair with roption.bind_some_right:
roption.map ?m_3 ?m_4
↑
roption.bind (roption.map ?m_3 ?m_4) roption.some
↓
roption.bind ?m_3 (λ (y : ?m_1), roption.some (?m_4 y))
 -/
#print roption.map_bind /- unjoinable pair with roption.bind_some_right:
roption.map ?m_3 ?m_4
↑
roption.map ?m_3 (roption.bind ?m_4 roption.some)
↓
roption.bind ?m_3 (λ (y : ?m_1), roption.some (?m_4 y))


unjoinable pair with roption.bind_some_right:
roption.map ?m_3 ?m_4
↑
roption.map ?m_3 (roption.bind ?m_4 roption.some)
↓
roption.bind ?m_3 (λ (y : ?m_1), roption.some (?m_4 y))
 -/
#print roption.mem_restrict /- timeout -/
#print pfun.coe_val /- timeout -/

-- data/pnat/basic.lean
#print nat.succ_pnat_coe /- timeout -/
#print nat.to_pnat'_coe /- timeout -/
#print pnat.pos /- timeout -/
#print pnat.mk_coe /- timeout -/
#print pnat.add_coe /- timeout -/
#print pnat.coe_to_pnat' /- timeout -/
#print pnat.one_le /- timeout -/
#print pnat.mk_bit1 /- unjoinable pair with bit1_zero:
1
↑
⟨bit1 0, ?m_1⟩
↓
bit1 ⟨0, ?m_1⟩
 -/
#print pnat.bit0_le_bit0 /- timeout -/
#print pnat.bit0_le_bit1 /- timeout -/
#print pnat.bit1_le_bit0 /- timeout -/
#print pnat.bit1_le_bit1 /- timeout -/
#print pnat.one_coe /- timeout -/
#print pnat.mul_coe /- timeout -/
#print pnat.coe_bit0 /- timeout -/
#print pnat.coe_bit1 /- timeout -/
#print pnat.pow_coe /- timeout -/

-- data/pnat/intervals.lean
#print pnat.Ico.mem /- timeout -/

-- data/polynomial.lean
#print polynomial.C_mul /- timeout -/
#print polynomial.coeff_C_mul /- timeout -/
#print polynomial.eval₂_add /- timeout -/
#print polynomial.eval₂_mul /- timeout -/
#print polynomial.eval_add /- timeout -/
#print polynomial.eval_mul /- timeout -/
#print polynomial.add_comp /- timeout -/
#print polynomial.nat_degree_nat_cast /- timeout -/
#print polynomial.map_mul /- timeout -/
#print polynomial.leading_coeff_eq_zero /- timeout -/
#print polynomial.leading_coeff_monomial /- timeout -/
#print polynomial.coeff_mul_degree_add_degree /- timeout -/
#print polynomial.degree_X_pow /- timeout -/
#print polynomial.degree_mul_eq /- timeout -/
#print polynomial.leading_coeff_mul /- timeout -/
#print polynomial.degree_coe_units /- timeout -/
#print polynomial.nat_degree_coe_units /- timeout -/
#print polynomial.degree_map /- timeout -/
#print polynomial.nat_degree_map /- timeout -/
#print polynomial.leading_coeff_map /- timeout -/
#print polynomial.map_eq_zero /- timeout -/

-- data/prod.lean
#print prod.mk.inj_iff /- timeout -/
#print prod.swap_prod_mk /- unjoinable pair with prod.mk.eta:
prod.swap ?m_3
↑
prod.swap (?m_3.fst, ?m_3.snd)
↓
(?m_3.snd, ?m_3.fst)


unjoinable pair with prod.mk.eta:
prod.swap ?m_3
↑
prod.swap (?m_3.fst, ?m_3.snd)
↓
(?m_3.snd, ?m_3.fst)
 -/

-- data/quot.lean
#print quotient.eq /- timeout -/
#print quotient.eq' /- timeout -/

-- data/rat/basic.lean
#print rat.num_denom /- timeout -/
#print rat.coe_int_denom /- unjoinable pair with int.cast_zero:
0.denom
↑
↑0.denom
↓
1
 -/
#print rat.coe_nat_num /- timeout -/
#print rat.coe_nat_denom /- timeout -/
#print rat.mul_own_denom_eq_num /- timeout -/

-- data/rat/cast.lean
#print rat.cast_coe_int /- timeout -/
#print rat.cast_coe_nat /- unjoinable pair with nat.cast_zero:
↑0
↑
↑↑0
↓
↑0
 -/
#print rat.cast_zero /- timeout -/
#print rat.cast_neg /- unjoinable pair with neg_neg:
↑?m_2
↑
↑- -?m_2
↓
-↑-?m_2
 -/
#print rat.cast_inj /- timeout -/
#print rat.cast_eq_zero /- timeout -/
#print rat.cast_add /- timeout -/
#print rat.cast_sub /- timeout -/
#print rat.cast_mul /- timeout -/
#print rat.cast_bit0 /- unjoinable pair with bit0_zero:
↑0
↑
↑(bit0 0)
↓
bit0 ↑0
 -/
#print rat.cast_bit1 /- timeout -/
#print rat.cast_inv /- unjoinable pair with inv_inv':
↑?m_2
↑
↑?m_2⁻¹⁻¹
↓
(↑?m_2⁻¹)⁻¹
 -/
#print rat.cast_nonneg /- timeout -/
#print rat.cast_le /- timeout -/
#print rat.cast_lt /- timeout -/
#print rat.cast_nonpos /- timeout -/
#print rat.cast_lt_zero /- timeout -/
#print rat.cast_min /- timeout -/
#print rat.cast_max /- timeout -/

-- data/real/basic.lean
#print real.mk_pos /- timeout -/

-- data/real/cau_seq_completion.lean
#print cau_seq.completion.mk_eq_zero /- timeout -/
#print cau_seq.completion.mk_add /- timeout -/

-- data/real/ennreal.lean
#print ennreal.to_nnreal_coe /- unjoinable pair with with_bot.coe_one:
ennreal.to_nnreal 1
↑
ennreal.to_nnreal ↑1
↓
1
 -/
#print ennreal.coe_zero /- timeout -/
#print ennreal.to_real_nonneg /- timeout -/
#print ennreal.coe_to_real /- unjoinable pair with with_bot.coe_one:
ennreal.to_real 1
↑
ennreal.to_real ↑1
↓
1
 -/
#print ennreal.coe_eq_coe /- timeout -/
#print ennreal.coe_lt_coe /- timeout -/
#print ennreal.coe_eq_zero /- timeout -/
#print ennreal.zero_eq_coe /- timeout -/
#print ennreal.coe_nonneg /- timeout -/
#print ennreal.coe_pos /- timeout -/
#print ennreal.coe_add /- timeout -/
#print ennreal.coe_mul /- timeout -/
#print ennreal.coe_bit0 /- timeout -/
#print ennreal.coe_bit1 /- timeout -/
#print ennreal.one_lt_two /- timeout -/
#print ennreal.two_pos /- timeout -/
#print ennreal.add_top /- timeout -/
#print ennreal.coe_pow /- timeout -/
#print ennreal.coe_finset_prod /- timeout -/
#print ennreal.coe_lt_top /- timeout -/
#print ennreal.one_le_coe_iff /- unjoinable pair with with_bot.coe_one:
1 ≤ 1
↑
1 ≤ ↑1
↓
1 ≤ 1
 -/
#print ennreal.coe_le_one_iff /- unjoinable pair with with_bot.coe_one:
1 ≤ 1
↑
↑1 ≤ 1
↓
1 ≤ 1
 -/
#print ennreal.coe_lt_one_iff /- timeout -/
#print ennreal.one_lt_coe_iff /- timeout -/
#print ennreal.coe_nat /- timeout -/
#print ennreal.max_eq_zero_iff /- timeout -/
#print ennreal.top_sub_coe /- unjoinable pair with with_bot.coe_one:
⊤ - 1
↑
⊤ - ↑1
↓
⊤
 -/
#print ennreal.sub_le_iff_le_add /- timeout -/
#print ennreal.bit0_inj /- unjoinable pair with bit0_zero:
0 = bit0 ?m_1
↑
bit0 0 = bit0 ?m_1
↓
0 = ?m_1
 -/
#print ennreal.bit0_eq_top_iff /- timeout -/
#print ennreal.bit1_inj /- timeout -/
#print ennreal.bit1_eq_one_iff /- timeout -/
#print ennreal.inv_eq_inv /- timeout -/
#print ennreal.inv_eq_zero /- timeout -/
#print ennreal.inv_pos /- timeout -/
#print ennreal.inv_lt_inv /- unjoinable pair with ennreal.inv_inv:
?m_1 < ?m_2⁻¹
↑
?m_1⁻¹⁻¹ < ?m_2⁻¹
↓
?m_1 < ?m_2⁻¹


unjoinable pair with ennreal.inv_inv:
?m_1⁻¹ < ?m_2
↑
?m_1⁻¹ < ?m_2⁻¹⁻¹
↓
?m_1⁻¹ < ?m_2
 -/
#print ennreal.inv_le_inv /- unjoinable pair with ennreal.inv_inv:
?m_1 * ?m_2 ≤ 1
↑
?m_1⁻¹⁻¹ ≤ ?m_2⁻¹
↓
?m_1 * ?m_2 ≤ 1


unjoinable pair with ennreal.inv_inv:
?m_1⁻¹ ≤ ?m_2
↑
?m_1⁻¹ ≤ ?m_2⁻¹⁻¹
↓
?m_1⁻¹ ≤ ?m_2
 -/
#print ennreal.inv_lt_one /- unjoinable pair with ennreal.inv_inv:
?m_1 < 1
↑
?m_1⁻¹⁻¹ < 1
↓
1 < ?m_1⁻¹
 -/
#print ennreal.le_inv_iff_mul_le /- timeout -/
#print ennreal.div_zero_iff /- timeout -/
#print ennreal.div_pos_iff /- timeout -/
#print ennreal.of_real_pos /- unjoinable pair with ennreal.of_real_zero:
false
↑
0 < ennreal.of_real 0
↓
0 < 0
 -/
#print ennreal.of_real_eq_zero /- timeout -/
#print ennreal.to_real_mul_top /- timeout -/

-- data/real/ereal.lean
#print ereal.coe_real_le /- timeout -/
#print ereal.coe_real_lt /- timeout -/
#print ereal.coe_real_inj' /- timeout -/

-- data/real/hyperreal.lean
#print hyperreal.coe_eq_coe /- timeout -/
#print hyperreal.cast_div /- timeout -/
#print hyperreal.coe_lt_coe /- unjoinable pair with filter.filter_product.of_zero:
0 < ↑?m_1
↑
↑0 < ↑?m_1
↓
0 < ?m_1


unjoinable pair with filter.filter_product.of_zero:
↑?m_1 < 0
↑
↑?m_1 < ↑0
↓
?m_1 < 0
 -/
#print hyperreal.coe_le_coe /- timeout -/
#print hyperreal.coe_abs /- timeout -/
#print hyperreal.coe_max /- timeout -/
#print hyperreal.coe_min /- timeout -/

-- data/real/irrational.lean
#print irr_rat_add_iff_irr /- unjoinable pair with add_zero:
irrational ↑?m_1
↑
irrational (↑?m_1 + 0)
↓
irrational 0


unjoinable pair with rat.cast_one:
irrational (1 + ?m_1)
↑
irrational (↑1 + ?m_1)
↓
irrational ?m_1


unjoinable pair with add_zero:
irrational ↑?m_1
↑
irrational (↑?m_1 + 0)
↓
irrational 0
 -/
#print irr_add_rat_iff_irr /- timeout -/

-- data/real/nnreal.lean
#print nnreal.coe_mk /- timeout -/
#print nnreal.coe_one /- timeout -/
#print nnreal.coe_add /- timeout -/
#print nnreal.coe_mul /- timeout -/
#print nnreal.coe_div /- timeout -/
#print nnreal.coe_inv /- timeout -/
#print nnreal.coe_eq_zero /- timeout -/
#print nnreal.coe_nat_cast /- timeout -/
#print nnreal.zero_le_coe /- timeout -/
#print nnreal.of_real_pos /- timeout -/
#print nnreal.of_real_eq_zero /- unjoinable pair with nnreal.of_real_coe:
?m_1 = 0
↑
nnreal.of_real ↑?m_1 = 0
↓
↑?m_1 ≤ 0
 -/
#print nnreal.of_real_lt_of_real_iff' /- unjoinable pair with nnreal.of_real_coe:
?m_1 < nnreal.of_real ?m_2
↑
nnreal.of_real ↑?m_1 < nnreal.of_real ?m_2
↓
↑?m_1 < ?m_2 ∧ 0 < ?m_2


unjoinable pair with nnreal.of_real_coe:
nnreal.of_real ?m_1 < ?m_2
↑
nnreal.of_real ?m_1 < nnreal.of_real ↑?m_2
↓
?m_1 < ↑?m_2 ∧ 0 < ↑?m_2
 -/
#print nnreal.sub_le_iff_le_add /- timeout -/
#print nnreal.sub_le_self /- timeout -/

-- data/real/pi.lean
#print real.cos_pi_over_two_pow /- timeout -/
#print real.sin_pi_over_two_pow_succ /- timeout -/

-- data/semiquot.lean
#print semiquot.mem_blur' /- timeout -/
#print semiquot.mem_map /- unjoinable pair with semiquot.mem_map:
∃ (a : ?m_1), a ∈ ?m_2 ∧ ?m_3 a = ?m_4
↑
?m_2 ∈ semiquot.map ?m_4 ?m_5
↓
∃ (a : ?m_1), a ∈ ?m_3 ∧ ?m_4 a = ?m_5


unjoinable pair with semiquot.mem_map:
∃ (a : ?m_1), a ∈ ?m_2 ∧ ?m_3 a = ?m_4
↑
?m_2 ∈ semiquot.map ?m_4 ?m_5
↓
∃ (a : ?m_1), a ∈ ?m_3 ∧ ?m_4 a = ?m_5
 -/
#print semiquot.mem_bind /- timeout -/
#print semiquot.pure_inj /- timeout -/
#print semiquot.pure_le /- timeout -/
#print semiquot.mem_univ /- timeout -/

-- data/seq/computation.lean
#print computation.destruct_map /- unjoinable pair with computation.map_id:
computation.destruct ?m_2
↑
computation.destruct (computation.map id ?m_2)
↓
computation.lmap id (computation.rmap (computation.map id) (computation.destruct ?m_2))


unjoinable pair with computation.map_id:
computation.destruct ?m_2
↑
computation.destruct (computation.map id ?m_2)
↓
computation.lmap id (computation.rmap (computation.map id) (computation.destruct ?m_2))
 -/
#print computation.bind_ret /- unjoinable pair with computation.bind_ret':
?m_1
↑
computation.bind ?m_2 (computation.return ∘ λ (x : ?m_1), x)
↓
computation.map (λ (x : ?m_1), x) ?m_2


unjoinable pair with computation.bind_ret':
?m_1
↑
computation.bind ?m_2 (computation.return ∘ λ (x : ?m_1), x)
↓
computation.map (λ (x : ?m_1), x) ?m_2
 -/

-- data/seq/seq.lean
#print seq.map_nth /- unjoinable pair with seq.map_nil:
seq.nth seq.nil ?m_2
↑
seq.nth (seq.map ?m_3 seq.nil) ?m_4
↓
option.map ?m_3 (seq.nth seq.nil ?m_4)


unjoinable pair with seq.map_nil:
seq.nth seq.nil ?m_2
↑
seq.nth (seq.map ?m_3 seq.nil) ?m_4
↓
option.map ?m_3 (seq.nth seq.nil ?m_4)
 -/
#print seq.join_cons /- unjoinable pair with prod.mk.eta:
seq.join (seq.cons ?m_2 ?m_3)
↑
seq.join (seq.cons (?m_2.fst, ?m_2.snd) ?m_3)
↓
seq.cons ?m_2.fst (seq.append ?m_2.snd (seq.join ?m_3))


unjoinable pair with prod.mk.eta:
seq.join (seq.cons ?m_2 ?m_3)
↑
seq.join (seq.cons (?m_2.fst, ?m_2.snd) ?m_3)
↓
seq.cons ?m_2.fst (seq.append ?m_2.snd (seq.join ?m_3))
 -/
#print seq1.bind_ret /- unjoinable pair with function.comp.right_id:
seq1.map (λ (x : ?m_1), x) ?m_2
↑
seq1.bind ?m_2 (seq1.ret ∘ id)
↓
seq1.map id ?m_2


unjoinable pair with function.comp.right_id:
seq1.map (λ (x : ?m_1), x) ?m_2
↑
seq1.bind ?m_2 (seq1.ret ∘ id)
↓
seq1.map id ?m_2
 -/

-- data/seq/wseq.lean
#print wseq.destruct_flatten /- unjoinable pair with wseq.flatten_ret:
wseq.destruct ?m_2
↑
wseq.destruct (wseq.flatten (computation.return ?m_2))
↓
computation.return ?m_2 >>= wseq.destruct
 -/
#print wseq.mem_think /- timeout -/
#print wseq.join_map_ret /- unjoinable pair with wseq.map_nil:
wseq.nil ~ wseq.nil
↑
wseq.join (wseq.map wseq.ret wseq.nil) ~ wseq.nil
↓
true


unjoinable pair with wseq.map_nil:
wseq.nil ~ wseq.nil
↑
wseq.join (wseq.map wseq.ret wseq.nil) ~ wseq.nil
↓
true
 -/
#print wseq.join_append /- unjoinable pair with wseq.nil_append:
wseq.join ?m_2 ~ wseq.join ?m_2
↑
wseq.join (wseq.append wseq.nil ?m_2) ~ wseq.append (wseq.join wseq.nil) (wseq.join ?m_2)
↓
true


unjoinable pair with wseq.nil_append:
wseq.join ?m_2 ~ wseq.join ?m_2
↑
wseq.join (wseq.append wseq.nil ?m_2) ~ wseq.append (wseq.join wseq.nil) (wseq.join ?m_2)
↓
true


unjoinable pair with wseq.join_nil:
wseq.join ?m_2 ~ wseq.join ?m_2
↑
wseq.join (wseq.append wseq.nil ?m_2) ~ wseq.append (wseq.join wseq.nil) (wseq.join ?m_2)
↓
true


unjoinable pair with wseq.join_nil:
wseq.join ?m_2 ~ wseq.join ?m_2
↑
wseq.join (wseq.append ?m_2 wseq.nil) ~ wseq.append (wseq.join ?m_2) (wseq.join wseq.nil)
↓
true
 -/
#print wseq.bind_ret /- unjoinable pair with function.comp.right_id:
wseq.bind ?m_2 wseq.ret ~ ?m_2
↑
wseq.bind ?m_2 (wseq.ret ∘ id) ~ wseq.map id ?m_2
↓
true


unjoinable pair with function.comp.right_id:
wseq.bind ?m_2 wseq.ret ~ ?m_2
↑
wseq.bind ?m_2 (wseq.ret ∘ id) ~ wseq.map id ?m_2
↓
true


unjoinable pair with wseq.map_nil:
wseq.bind wseq.nil (wseq.ret ∘ ?m_3) ~ wseq.nil
↑
wseq.bind wseq.nil (wseq.ret ∘ ?m_3) ~ wseq.map ?m_3 wseq.nil
↓
true


unjoinable pair with wseq.map_nil:
wseq.bind wseq.nil (wseq.ret ∘ ?m_3) ~ wseq.nil
↑
wseq.bind wseq.nil (wseq.ret ∘ ?m_3) ~ wseq.map ?m_3 wseq.nil
↓
true
 -/
#print wseq.join_join /- unjoinable pair with wseq.join_nil:
wseq.nil ~ wseq.nil
↑
wseq.join (wseq.join wseq.nil) ~ wseq.join (wseq.map wseq.join wseq.nil)
↓
true


unjoinable pair with wseq.map_nil:
wseq.nil ~ wseq.nil
↑
wseq.join (wseq.join wseq.nil) ~ wseq.join (wseq.map wseq.join wseq.nil)
↓
true


unjoinable pair with wseq.map_nil:
wseq.nil ~ wseq.nil
↑
wseq.join (wseq.join wseq.nil) ~ wseq.join (wseq.map wseq.join wseq.nil)
↓
true
 -/

-- data/set/basic.lean
#print set.mem_set_of_eq /- timeout -/
#print set.set_of_subset_set_of /- unjoinable pair with set.set_of_false:
set_of ?m_2 ⊆ ∅
↑
{a : ?m_1 | ?m_2 a} ⊆ {a : ?m_1 | false}
↓
∀ (a : ?m_1), ?m_2 a → false
 -/
#print set.sep_set_of /- unjoinable pair with set.set_of_false:
has_sep.sep ?m_2 ∅
↑
{a ∈ {a : ?m_1 | false} | ?m_2 a}
↓
∅
 -/
#print set.not_not_mem /- unjoinable pair with manifold.chart_mem_atlas:
true
↑
¬chart_at ?m_2 ?m_6 ∉ atlas ?m_2 ?m_1
↓
chart_at ?m_2 ?m_6 ∈ atlas ?m_2 ?m_1


unjoinable pair with manifold.chart_mem_atlas:
true
↑
¬chart_at ?m_2 ?m_6 ∉ atlas ?m_2 ?m_1
↓
chart_at ?m_2 ?m_6 ∈ atlas ?m_2 ?m_1
 -/
#print set.mem_univ /- timeout -/
#print set.mem_union_eq /- timeout -/
#print set.union_empty_iff /- timeout -/
#print set.mem_inter_eq /- timeout -/
#print set.mem_singleton_iff /- timeout -/
#print set.singleton_eq_singleton_iff /- timeout -/
#print set.mem_sep_eq /- timeout -/
#print set.mem_compl_eq /- timeout -/
#print set.mem_diff /- timeout -/
#print set.insert_diff_singleton /- unjoinable pair with set.diff_self:
{?m_2}
↑
insert ?m_2 ({?m_2} \ {?m_2})
↓
{?m_2}


unjoinable pair with set.diff_self:
{?m_2}
↑
insert ?m_2 ({?m_2} \ {?m_2})
↓
{?m_2}
 -/
#print set.preimage_inter /- unjoinable pair with set.inter_self:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 ∩ ?m_4)
↓
?m_2 ⁻¹' ?m_3


unjoinable pair with set.inter_self:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 ∩ ?m_4)
↓
?m_2 ⁻¹' ?m_3
 -/
#print set.preimage_union /- unjoinable pair with set.union_self:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 ∪ ?m_4)
↓
?m_2 ⁻¹' ?m_3


unjoinable pair with set.union_self:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 ∪ ?m_4)
↓
?m_2 ⁻¹' ?m_3
 -/
#print set.preimage_diff /- unjoinable pair with set.diff_empty:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 \ ∅)
↓
?m_2 ⁻¹' ?m_3


unjoinable pair with set.diff_empty:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' (?m_4 \ ∅)
↓
?m_2 ⁻¹' ?m_3
 -/
#print set.mem_image /- unjoinable pair with set.mem_image:
∃ (x : ?m_1), x ∈ ?m_2 ∧ ?m_3 x = ?m_4
↑
?m_2 ∈ ?m_4 '' ?m_5
↓
∃ (x : ?m_1), x ∈ ?m_3 ∧ ?m_4 x = ?m_5


unjoinable pair with set.mem_image:
∃ (x : ?m_1), x ∈ ?m_2 ∧ ?m_3 x = ?m_4
↑
?m_2 ∈ ?m_4 '' ?m_5
↓
∃ (x : ?m_1), x ∈ ?m_3 ∧ ?m_4 x = ?m_5


unjoinable pair with set.image_univ:
∃ (y : ?m_1), ?m_3 y = ?m_4
↑
?m_2 ∈ ?m_4 '' set.univ
↓
∃ (x : ?m_1), ?m_2 x = ?m_3


unjoinable pair with set.image_univ:
∃ (y : ?m_1), ?m_3 y = ?m_4
↑
?m_2 ∈ ?m_4 '' set.univ
↓
∃ (x : ?m_1), ?m_2 x = ?m_3
 -/
#print set.image_eq_empty /- timeout -/
#print set.image_id' /- unjoinable pair with set.image_univ:
set.range (λ (x : ?m_1), x)
↑
(λ (x : ?m_1), x) '' set.univ
↓
set.univ


unjoinable pair with set.image_univ:
set.range (λ (x : ?m_1), x)
↑
(λ (x : ?m_1), x) '' set.univ
↓
set.univ
 -/
#print set.nonempty_image_iff /- unjoinable pair with set.image_univ:
set.nonempty (set.range ?m_3)
↑
set.nonempty (?m_3 '' set.univ)
↓
set.nonempty set.univ


unjoinable pair with set.image_univ:
set.nonempty (set.range ?m_3)
↑
set.nonempty (?m_3 '' set.univ)
↓
set.nonempty set.univ
 -/
#print set.range_eq_empty /- unjoinable pair with set.range_coe_subtype:
?m_2 = ∅
↑
set.range coe = ∅
↓
¬nonempty ↥?m_2
 -/
#print set.mem_prod /- timeout -/
#print set.empty_prod /- unjoinable pair with set.prod_empty:
∅
↑
set.prod ∅ ∅
↓
∅


unjoinable pair with set.prod_empty:
∅
↑
set.prod ∅ ∅
↓
∅
 -/
#print set.prod_singleton_singleton /- unjoinable pair with set.prod_singleton_singleton:
{(?m_2, ?m_3)}
↑
set.prod {?m_3} {?m_4}
↓
{(?m_3, ?m_4)}


unjoinable pair with set.prod_singleton_singleton:
{(?m_2, ?m_3)}
↑
set.prod {?m_3} {?m_4}
↓
{(?m_3, ?m_4)}
 -/
#print set.prod_mk_mem_set_prod_eq /- timeout -/

-- data/set/finite.lean
#print set.finite.mem_to_finset /- timeout -/
#print finset.coe_bind /- timeout -/
#print finset.coe_to_finset /- timeout -/
#print finset.coe_to_finset' /- timeout -/
#print finset.mem_preimage /- timeout -/

-- data/set/intervals/basic.lean
#print set.mem_Iio /- timeout -/
#print set.mem_Icc /- timeout -/
#print set.mem_Ici /- timeout -/
#print set.mem_Ioi /- timeout -/
#print set.right_mem_Icc /- timeout -/
#print set.Ico_inter_Iio /- timeout -/

-- data/set/intervals/unordered_interval.lean
#print set.right_mem_interval /- timeout -/

-- data/set/lattice.lean
#print set.mem_Inter /- timeout -/
#print set.compl_Union /- unjoinable pair with set.bUnion_of_singleton:
-?m_2
↑
-⋃ (i : ?m_1) (H : i ∈ ?m_2), {i}
↓
⋂ (i : ?m_1) (i_1 : i ∈ ?m_2), -{i}
 -/
#print set.compl_bUnion /- unjoinable pair with set.bUnion_of_singleton:
-?m_2
↑
-⋃ (i : ?m_1) (H : i ∈ ?m_2), {i}
↓
⋂ (i : ?m_1) (H : i ∈ ?m_2), -{i}
 -/
#print set.sUnion_range /- unjoinable pair with set.range_coe_subtype:
⋃₀?m_2
↑
⋃₀ set.range coe
↓
set.Union coe
 -/
#print set.sInter_range /- unjoinable pair with set.range_coe_subtype:
⋂₀?m_2
↑
⋂₀ set.range coe
↓
set.Inter coe
 -/
#print set.bUnion_image /- unjoinable pair with set.bUnion_of_singleton:
⋃ (y : ?m_1) (H : y ∈ ?m_2), {?m_3 y}
↑
⋃ (x : ?m_1) (H : x ∈ ?m_3 '' ?m_4), {x}
↓
⋃ (y : ?m_2) (H : y ∈ ?m_3), {?m_4 y}
 -/
#print set.preimage_Union /- unjoinable pair with set.bUnion_of_singleton:
?m_3 ⁻¹' ?m_4
↑
?m_3 ⁻¹' ⋃ (i : ?m_2) (H : i ∈ ?m_4), {i}
↓
⋃ (i : ?m_2) (i_1 : i ∈ ?m_3), ?m_4 ⁻¹' {i}
 -/
#print set.preimage_sUnion /- unjoinable pair with set.sUnion_empty:
∅
↑
?m_3 ⁻¹' ⋃₀∅
↓
⋃ (t : set ?m_2), ∅
 -/
#print set.mem_seq_iff /- timeout -/

-- data/setoid.lean
#print setoid.eqv_gen_idem /- unjoinable pair with setoid.eqv_gen_of_setoid:
eqv_gen.setoid (setoid.rel ?m_2)
↑
eqv_gen.setoid (setoid.rel (eqv_gen.setoid setoid.r))
↓
?m_1
 -/

-- data/sigma/basic.lean
#print sigma.mk.inj_iff /- timeout -/

-- data/string/basic.lean
#print string.le_iff_to_list_le /- timeout -/

-- data/subtype.lean
#print subtype.coe_eta /- timeout -/
#print subtype.coe_mk /- timeout -/
#print subtype.mk_eq_mk /- timeout -/
#print subtype.val_prop /- timeout -/
#print subtype.val_prop' /- timeout -/

-- data/vector2.lean
#print vector.to_list_of_fn /- unjoinable pair with vector.of_fn_nth:
vector.to_list ?m_3
↑
vector.to_list (vector.of_fn (vector.nth ?m_3))
↓
list.of_fn (vector.nth ?m_3)
 -/
#print vector.mk_to_list /- unjoinable pair with vector.to_list_nil:
⟨list.nil ?m_1, _⟩
↑
⟨vector.to_list vector.nil, ?m_2⟩
↓
vector.nil
 -/
#print vector.nth_map /- unjoinable pair with vector.map_nil:
vector.nth vector.nil ?m_2
↑
vector.nth (vector.map ?m_3 vector.nil) ?m_4
↓
?m_1 (vector.nth vector.nil ?m_3)


unjoinable pair with vector.map_nil:
vector.nth vector.nil ?m_2
↑
vector.nth (vector.map ?m_3 vector.nil) ?m_4
↓
?m_1 (vector.nth vector.nil ?m_3)
 -/
#print vector.tail_of_fn /- unjoinable pair with vector.of_fn_nth:
vector.tail ?m_3
↑
vector.tail (vector.of_fn (vector.nth ?m_3))
↓
vector.of_fn (λ (i : fin (nat.succ ?m_2 - 1)), vector.nth ?m_3 (fin.succ i))
 -/
#print vector.nth_mem /- timeout -/

-- data/zmod/basic.lean
#print zmod.cast_self_eq_zero /- timeout -/
#print zmod.cast_mod_nat /- timeout -/
#print zmod.cast_mod_nat' /- timeout -/
#print zmod.cast_mod_int /- timeout -/
#print zmod.cast_mod_int' /- timeout -/
#print zmod.cast_mul_right_val_cast /- timeout -/
#print zmod.cast_mul_left_val_cast /- timeout -/
#print zmod.coe_val_min_abs /- timeout -/
#print zmod.val_min_abs_eq_zero /- timeout -/
#print zmod.nat_abs_mod_two /- timeout -/
#print zmodp.cast_mod_nat /- unjoinable pair with nat.mod_one:
0
↑
↑(?m_2 % 1)
↓
↑?m_2


unjoinable pair with nat.mod_one:
0
↑
↑(?m_2 % 1)
↓
↑?m_2
 -/
#print zmodp.cast_val /- unjoinable pair with zmod.zero_val:
0
↑
↑(0.val)
↓
0
 -/
#print zmodp.cast_mod_int /- timeout -/

-- data/zmod/quadratic_reciprocity.lean
#print zmodp.wilsons_lemma /- timeout -/
#print zmodp.prod_Ico_one_prime /- unjoinable pair with finset.Ico.succ_singleton:
0 + 1
↑
finset.prod (finset.Ico 1 (1 + 1)) (λ (x : ℕ), ↑x)
↓
-1


unjoinable pair with finset.Ico.succ_singleton:
0 + 1
↑
finset.prod (finset.Ico 1 (1 + 1)) (λ (x : ℕ), ↑x)
↓
-1
 -/

-- data/zsqrtd/basic.lean
#print zsqrtd.add_re /- timeout -/
#print zsqrtd.add_im /- timeout -/
#print zsqrtd.mul_re /- timeout -/
#print zsqrtd.mul_im /- timeout -/
#print zsqrtd.coe_nat_re /- timeout -/
#print zsqrtd.coe_nat_im /- timeout -/
#print zsqrtd.coe_int_im /- timeout -/
#print zsqrtd.smul_val /- timeout -/
#print zsqrtd.smuld_val /- timeout -/
#print zsqrtd.norm_nat_cast /- timeout -/

-- data/zsqrtd/gaussian_int.lean
#print gaussian_int.to_real_re /- timeout -/
#print gaussian_int.to_real_im /- timeout -/
#print gaussian_int.to_complex_re /- timeout -/
#print gaussian_int.to_complex_im /- timeout -/
#print gaussian_int.to_complex_add /- timeout -/
#print gaussian_int.to_complex_one /- timeout -/
#print gaussian_int.to_complex_zero /- timeout -/
#print gaussian_int.to_complex_neg /- timeout -/
#print gaussian_int.to_complex_inj /- timeout -/
#print gaussian_int.to_complex_eq_zero /- timeout -/
#print gaussian_int.nat_cast_complex_norm /- timeout -/
#print gaussian_int.norm_eq_zero /- timeout -/
#print gaussian_int.nat_cast_nat_abs_norm /- unjoinable pair with zsqrtd.norm_zero:
↑0
↑
↑(int.nat_abs (zsqrtd.norm 0))
↓
↑0
 -/

-- field_theory/minimal_polynomial.lean
#print minimal_polynomial.algebra_map /- timeout -/

-- geometry/manifold/basic_smooth_bundle.lean
#print basic_smooth_bundle_core.mem_chart_source_iff /- timeout -/
#print basic_smooth_bundle_core.chart_at_inv_fun_fst /- timeout -/

-- geometry/manifold/smooth_manifold_with_corners.lean
#print mem_ext_chart_source /- timeout -/

-- group_theory/congruence.lean
#print add_con.eq /- timeout -/
#print con.eq /- timeout -/
#print add_con.coe_add /- timeout -/
#print con.coe_mul /- timeout -/
#print con.lift_on_beta /- timeout -/
#print add_con.lift_on_beta /- timeout -/
#print add_con.coe_zero /- timeout -/

-- group_theory/free_abelian_group.lean
#print free_abelian_group.map_add /- unjoinable pair with add_zero:
?m_3 <$> ?m_4
↑
?m_3 <$> (?m_4 + 0)
↓
?m_2 <$> ?m_3


unjoinable pair with add_zero:
?m_3 <$> ?m_4
↑
?m_3 <$> (?m_4 + 0)
↓
?m_2 <$> ?m_3
 -/
#print free_abelian_group.map_neg /- unjoinable pair with neg_neg:
?m_3 <$> ?m_4
↑
?m_3 <$> - -?m_4
↓
?m_2 <$> ?m_3
 -/
#print free_abelian_group.map_sub /- unjoinable pair with add_sub_cancel':
?m_3 <$> ?m_4
↑
?m_3 <$> (?m_4 + ?m_5 - ?m_4)
↓
?m_2 <$> ?m_3


unjoinable pair with add_sub_cancel':
?m_3 <$> ?m_4
↑
?m_3 <$> (?m_4 + ?m_5 - ?m_4)
↓
?m_2 <$> ?m_3
 -/
#print free_abelian_group.add_bind /- unjoinable pair with add_zero:
?m_3 >>= ?m_4
↑
?m_3 + 0 >>= ?m_4
↓
?m_2 >>= ?m_3


unjoinable pair with add_zero:
?m_3 >>= ?m_4
↑
?m_3 + 0 >>= ?m_4
↓
?m_2 >>= ?m_3
 -/
#print free_abelian_group.neg_bind /- unjoinable pair with neg_neg:
?m_3 >>= ?m_4
↑
- -?m_3 >>= ?m_4
↓
?m_2 >>= ?m_3
 -/
#print free_abelian_group.sub_bind /- unjoinable pair with add_sub_cancel':
?m_3 >>= ?m_4
↑
?m_3 + ?m_4 - ?m_3 >>= ?m_5
↓
?m_2 >>= ?m_3


unjoinable pair with add_sub_cancel':
?m_3 >>= ?m_4
↑
?m_3 + ?m_4 - ?m_3 >>= ?m_5
↓
?m_2 >>= ?m_3
 -/
#print free_abelian_group.seq_add /- unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> ?m_3 + ?m_4
↓
0 + 0


unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> ?m_3 + ?m_4
↓
0 + 0


unjoinable pair with add_zero:
?m_3 <*> ?m_4
↑
?m_3 <*> ?m_4 + 0
↓
?m_2 <*> ?m_3


unjoinable pair with add_zero:
?m_3 <*> ?m_4
↑
?m_3 <*> ?m_4 + 0
↓
?m_2 <*> ?m_3
 -/
#print free_abelian_group.seq_neg /- unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> -?m_3
↓
-0


unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> -?m_3
↓
-0


unjoinable pair with neg_neg:
?m_3 <*> ?m_4
↑
?m_3 <*> - -?m_4
↓
?m_2 <*> ?m_3
 -/
#print free_abelian_group.seq_sub /- unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> ?m_3 - ?m_4
↓
0 - 0


unjoinable pair with free_abelian_group.zero_seq:
0
↑
0 <*> ?m_3 - ?m_4
↓
0 - 0


unjoinable pair with add_sub_cancel':
?m_3 <*> ?m_4
↑
?m_3 <*> ?m_4 + ?m_5 - ?m_4
↓
?m_2 <*> ?m_3


unjoinable pair with add_sub_cancel':
?m_3 <*> ?m_4
↑
?m_3 <*> ?m_4 + ?m_5 - ?m_4
↓
?m_2 <*> ?m_3
 -/

-- group_theory/free_group.lean
#print free_group.red.step.bnot_rev /- unjoinable pair with bool.bnot_false:
free_group.red.step (?m_2 ++ (?m_3, tt) :: (?m_3, ff) :: ?m_4) (?m_2 ++ ?m_4)
↑
free_group.red.step (?m_2 ++ (?m_3, !ff) :: (?m_3, ff) :: ?m_4) (?m_2 ++ ?m_4)
↓
true


unjoinable pair with prod.mk.eta:
free_group.red.step (?m_2 ++ (?m_3.fst, !?m_3.snd) :: ?m_3 :: ?m_4) (?m_2 ++ ?m_4)
↑
free_group.red.step (?m_2 ++ (?m_3.fst, !?m_3.snd) :: (?m_3.fst, ?m_3.snd) :: ?m_4) (?m_2 ++ ?m_4)
↓
true


unjoinable pair with prod.mk.eta:
free_group.red.step (?m_2 ++ (?m_3.fst, !?m_3.snd) :: ?m_3 :: ?m_4) (?m_2 ++ ?m_4)
↑
free_group.red.step (?m_2 ++ (?m_3.fst, !?m_3.snd) :: (?m_3.fst, ?m_3.snd) :: ?m_4) (?m_2 ++ ?m_4)
↓
true


unjoinable pair with list.append_nil:
free_group.red.step (?m_2 ++ [(?m_3, !?m_4), (?m_3, ?m_4)]) ?m_2
↑
free_group.red.step (?m_2 ++ [(?m_3, !?m_4), (?m_3, ?m_4)]) (?m_2 ++ list.nil)
↓
true


unjoinable pair with list.append_nil:
free_group.red.step (?m_2 ++ [(?m_3, !?m_4), (?m_3, ?m_4)]) ?m_2
↑
free_group.red.step (?m_2 ++ [(?m_3, !?m_4), (?m_3, ?m_4)]) (?m_2 ++ list.nil)
↓
true
 -/
#print free_group.red.step.cons_bnot /- unjoinable pair with prod.mk.eta:
free_group.red.step (?m_2 :: (?m_2.fst, !?m_2.snd) :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2.fst, ?m_2.snd) :: (?m_2.fst, !?m_2.snd) :: ?m_3) ?m_3
↓
true


unjoinable pair with prod.mk.eta:
free_group.red.step (?m_2 :: (?m_2.fst, !?m_2.snd) :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2.fst, ?m_2.snd) :: (?m_2.fst, !?m_2.snd) :: ?m_3) ?m_3
↓
true


unjoinable pair with bool.bnot_false:
free_group.red.step ((?m_2, ff) :: (?m_2, tt) :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2, ff) :: (?m_2, !ff) :: ?m_3) ?m_3
↓
true
 -/
#print free_group.red.step.cons_bnot_rev /- unjoinable pair with bool.bnot_false:
free_group.red.step ((?m_2, tt) :: (?m_2, ff) :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2, !ff) :: (?m_2, ff) :: ?m_3) ?m_3
↓
true


unjoinable pair with prod.mk.eta:
free_group.red.step ((?m_2.fst, !?m_2.snd) :: ?m_2 :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2.fst, !?m_2.snd) :: (?m_2.fst, ?m_2.snd) :: ?m_3) ?m_3
↓
true


unjoinable pair with prod.mk.eta:
free_group.red.step ((?m_2.fst, !?m_2.snd) :: ?m_2 :: ?m_3) ?m_3
↑
free_group.red.step ((?m_2.fst, !?m_2.snd) :: (?m_2.fst, ?m_2.snd) :: ?m_3) ?m_3
↓
true
 -/
#print free_group.to_group.mul /- timeout -/
#print free_group.sum.mul /- timeout -/

-- group_theory/group_action.lean
#print mul_action.mem_stabilizer_iff /- timeout -/

-- group_theory/monoid_localization.lean
#print submonoid.localization_map.mul_inv_left /- timeout -/
#print add_submonoid.localization_map.add_neg_left /- timeout -/
#print add_submonoid.localization_map.add_neg_right /- timeout -/
#print submonoid.localization_map.mul_inv_right /- timeout -/
#print submonoid.localization_map.mul_inv /- timeout -/
#print add_submonoid.localization_map.add_neg /- timeout -/
#print add_submonoid.localization_map.mk'_add /- timeout -/
#print submonoid.localization_map.mk'_sec /- timeout -/
#print submonoid.localization_map.eq_mk'_iff_mul_eq /- timeout -/
#print submonoid.localization_map.mk'_eq_iff_eq_mul /- timeout -/
#print submonoid.localization_map.mk'_self /- timeout -/
#print add_submonoid.localization_map.mk'_self /- timeout -/
#print submonoid.localization_map.mul_mk'_eq_mk'_of_mul /- timeout -/
#print add_submonoid.localization_map.mk'_add_cancel_right /- timeout -/
#print submonoid.localization_map.mk'_mul_cancel_right /- timeout -/
#print submonoid.localization_map.mk'_mul_cancel_left /- timeout -/
#print add_submonoid.localization_map.mk'_add_cancel_left /- timeout -/

-- group_theory/perm/sign.lean
#print equiv.perm.mem_support /- timeout -/

-- group_theory/quotient_group.lean
#print quotient_add_group.coe_zero /- timeout -/
#print quotient_group.coe_one /- timeout -/
#print quotient_add_group.coe_add /- timeout -/
#print quotient_group.coe_inv /- timeout -/
#print quotient_add_group.coe_neg /- timeout -/
#print quotient_group.coe_pow /- timeout -/
#print quotient_group.coe_gpow /- timeout -/
#print quotient_group.lift_mk /- timeout -/
#print quotient_group.ker_lift_mk /- timeout -/

-- group_theory/subgroup.lean
#print is_subgroup.coe_inv /- timeout -/
#print is_subgroup.mem_trivial /- timeout -/
#print is_add_subgroup.mem_trivial /- timeout -/

-- group_theory/submonoid.lean
#print is_add_submonoid.coe_zero /- timeout -/
#print is_add_submonoid.smul_coe /- timeout -/
#print submonoid.mem_coe /- timeout -/
#print add_submonoid.mem_coe /- timeout -/
#print add_submonoid.coe_add /- timeout -/
#print submonoid.coe_mul /- timeout -/
#print submonoid.coe_one /- timeout -/
#print submonoid.coe_pow /- timeout -/
#print add_submonoid.coe_smul /- timeout -/
#print add_submonoid.mem_bot /- timeout -/
#print add_submonoid.mem_top /- timeout -/
#print submonoid.mem_top /- timeout -/

-- linear_algebra/basic.lean
#print linear_map.cod_restrict_apply /- timeout -/
#print submodule.of_le_apply /- timeout -/
#print submodule.bot_coe /- timeout -/
#print submodule.mem_bot /- timeout -/
#print submodule.mem_top /- timeout -/
#print submodule.inf_coe /- timeout -/
#print submodule.mem_inf /- timeout -/
#print submodule.Inf_coe /- timeout -/
#print submodule.mem_infi /- timeout -/
#print submodule.mem_map /- timeout -/
#print submodule.comap_coe /- timeout -/
#print submodule.prod_coe /- timeout -/
#print submodule.mem_prod /- timeout -/
#print submodule.quotient.mk_eq_zero /- timeout -/
#print linear_map.mem_range /- timeout -/
#print submodule.ker_of_le /- unjoinable pair with submodule.ker_of_le:
linear_map.ker (submodule.of_le ?m_6)
↑
linear_map.ker (submodule.of_le ?m_6)
↓
⊥
 -/
#print linear_equiv.range /- timeout -/

-- linear_algebra/multilinear.lean
#print linear_map.curry_uncurry_left /- unjoinable pair with linear_map.curry_uncurry_left:
multilinear_map.curry_left (linear_map.uncurry_left ?m_5)
↑
multilinear_map.curry_left (linear_map.uncurry_left ?m_5)
↓
?m_1


unjoinable pair with multilinear_map.uncurry_curry_left:
multilinear_map.curry_left (linear_map.uncurry_left (multilinear_map.curry_left ?m_5))
↑
multilinear_map.curry_left (linear_map.uncurry_left (multilinear_map.curry_left ?m_5))
↓
multilinear_map.curry_left ?m_5
 -/
#print multilinear_map.uncurry_curry_left /- unjoinable pair with multilinear_map.uncurry_curry_left:
linear_map.uncurry_left (multilinear_map.curry_left ?m_5)
↑
linear_map.uncurry_left (multilinear_map.curry_left ?m_5)
↓
?m_1


unjoinable pair with linear_map.curry_uncurry_left:
linear_map.uncurry_left (multilinear_map.curry_left (linear_map.uncurry_left ?m_5))
↑
linear_map.uncurry_left (multilinear_map.curry_left (linear_map.uncurry_left ?m_5))
↓
linear_map.uncurry_left ?m_5
 -/
#print multilinear_map.curry_uncurry_right /- unjoinable pair with multilinear_map.curry_uncurry_right:
multilinear_map.curry_right (multilinear_map.uncurry_right ?m_5)
↑
multilinear_map.curry_right (multilinear_map.uncurry_right ?m_5)
↓
?m_1


unjoinable pair with multilinear_map.uncurry_curry_right:
multilinear_map.curry_right (multilinear_map.uncurry_right (multilinear_map.curry_right ?m_5))
↑
multilinear_map.curry_right (multilinear_map.uncurry_right (multilinear_map.curry_right ?m_5))
↓
multilinear_map.curry_right ?m_5
 -/
#print multilinear_map.uncurry_curry_right /- unjoinable pair with multilinear_map.uncurry_curry_right:
multilinear_map.uncurry_right (multilinear_map.curry_right ?m_5)
↑
multilinear_map.uncurry_right (multilinear_map.curry_right ?m_5)
↓
?m_1


unjoinable pair with multilinear_map.curry_uncurry_right:
multilinear_map.uncurry_right (multilinear_map.curry_right (multilinear_map.uncurry_right ?m_5))
↑
multilinear_map.uncurry_right (multilinear_map.curry_right (multilinear_map.uncurry_right ?m_5))
↓
multilinear_map.uncurry_right ?m_5
 -/

-- linear_algebra/special_linear_group.lean
#print matrix.special_linear_group.inv_val /- timeout -/
#print matrix.special_linear_group.mul_val /- timeout -/
#print matrix.special_linear_group.one_val /- timeout -/

-- logic/basic.lean
#print coe_coe /- timeout -/
#print eq_iff_iff /- timeout -/
#print not_not /- unjoinable pair with not_exists:
¬∀ (x : ?m_1), ¬?m_2 x
↑
¬¬∃ (x : ?m_1), ?m_2 x
↓
Exists ?m_2
 -/
#print not_exists_not /- unjoinable pair with not_exists:
∀ (x : ?m_1), ¬¬?m_2 x
↑
¬∃ (x : ?m_1), ¬?m_2 x
↓
∀ (x : ?m_1), ?m_2 x


unjoinable pair with set_coe.exists:
∀ (x : ?m_1) (x_1 : x ∈ ?m_2), ¬¬?m_3 ⟨x, x_1⟩
↑
¬∃ (x : ↥?m_2), ¬?m_3 x
↓
∀ (x : ?m_1) (h : x ∈ ?m_2), ?m_3 ⟨x, h⟩
 -/
#print exists_const /- unjoinable pair with exists_prop:
?m_1 ∧ ?m_2
↑
∃ (x : ?m_1), ?m_2
↓
?m_1
 -/
#print exists_prop_of_true /- unjoinable pair with exists_pempty:
false
↑
∃ (h' : pempty), ?m_1 h'
↓
?m_1 ?m_2
 -/

-- measure_theory/ae_eq_fun.lean
#print measure_theory.ae_eq_fun.eintegral_eq_zero_iff /- timeout -/

-- measure_theory/bochner_integration.lean
#print measure_theory.l1.simple_func.coe_sub /- timeout -/

-- measure_theory/integration.lean
#print measure_theory.simple_func.mem_range /- timeout -/

-- measure_theory/l1_space.lean
#print measure_theory.l1.coe_add /- timeout -/
#print measure_theory.l1.coe_neg /- timeout -/
#print measure_theory.l1.coe_sub /- timeout -/
#print measure_theory.l1.coe_smul /- timeout -/

-- measure_theory/lebesgue_measure.lean
#print measure_theory.lebesgue_length_Icc /- unjoinable pair with set.Icc_self:
measure_theory.lebesgue_length {?m_1}
↑
measure_theory.lebesgue_length (set.Icc ?m_1 ?m_1)
↓
0


unjoinable pair with set.Icc_self:
measure_theory.lebesgue_length {?m_1}
↑
measure_theory.lebesgue_length (set.Icc ?m_1 ?m_1)
↓
0
 -/

-- measure_theory/measurable_space.lean
#print measurable_space.is_measurable_inf /- unjoinable pair with bot_inf_eq:
measurable_space.is_measurable ⊥ ?m_2
↑
measurable_space.is_measurable (⊥ ⊓ ?m_2) ?m_3
↓
measurable_space.is_measurable ⊥ ?m_2 ∧ measurable_space.is_measurable ?m_3 ?m_2


unjoinable pair with bot_inf_eq:
measurable_space.is_measurable ⊥ ?m_2
↑
measurable_space.is_measurable (⊥ ⊓ ?m_2) ?m_3
↓
measurable_space.is_measurable ⊥ ?m_2 ∧ measurable_space.is_measurable ?m_3 ?m_2
 -/
#print measurable_space.is_measurable_Inf /- unjoinable pair with Inf_univ:
measurable_space.is_measurable ⊥ ?m_2
↑
measurable_space.is_measurable (Inf set.univ) ?m_2
↓
∀ (m : measurable_space ?m_1), measurable_space.is_measurable m ?m_2
 -/
#print measurable_space.comap_sup /- unjoinable pair with bot_sup_eq:
measurable_space.comap ?m_3 ?m_4
↑
measurable_space.comap ?m_3 (⊥ ⊔ ?m_4)
↓
⊥ ⊔ measurable_space.comap ?m_3 ?m_4


unjoinable pair with bot_sup_eq:
measurable_space.comap ?m_3 ?m_4
↑
measurable_space.comap ?m_3 (⊥ ⊔ ?m_4)
↓
⊥ ⊔ measurable_space.comap ?m_3 ?m_4
 -/
#print measurable_space.map_inf /- unjoinable pair with bot_inf_eq:
measurable_space.map ?m_3 ⊥
↑
measurable_space.map ?m_3 (⊥ ⊓ ?m_4)
↓
measurable_space.map ?m_3 ⊥ ⊓ measurable_space.map ?m_3 ?m_4


unjoinable pair with bot_inf_eq:
measurable_space.map ?m_3 ⊥
↑
measurable_space.map ?m_3 (⊥ ⊓ ?m_4)
↓
measurable_space.map ?m_3 ⊥ ⊓ measurable_space.map ?m_3 ?m_4
 -/

-- number_theory/dioph.lean
#print option.cons_head_tail /- unjoinable pair with function.comp.left_id:
none :: some
↑
id none :: id ∘ some
↓
id


unjoinable pair with function.comp.left_id:
none :: some
↑
id none :: id ∘ some
↓
id
 -/

-- number_theory/pell.lean
#print pell.pell_eqz /- timeout -/
#print pell.pell_eq /- timeout -/

-- order/boolean_algebra.lean
#print compl_inj_iff /- timeout -/

-- order/bounded_lattice.lean
#print le_top /- timeout -/
#print top_le_iff /- timeout -/
#print bot_le /- timeout -/
#print le_bot_iff /- timeout -/
#print inf_eq_top_iff /- timeout -/
#print with_bot.some_lt_some /- timeout -/
#print with_bot.coe_le_coe /- timeout -/
#print with_bot.some_le_some /- unjoinable pair with ennreal.some_eq_coe:
↑?m_1 ≤ ↑?m_2
↑
some ?m_1 ≤ some ?m_2
↓
?m_1 ≤ ?m_2


unjoinable pair with ennreal.some_eq_coe:
↑?m_1 ≤ ↑?m_2
↑
some ?m_1 ≤ some ?m_2
↓
?m_1 ≤ ?m_2
 -/
#print with_top.some_le_some /- timeout -/
#print with_top.none_lt_some /- unjoinable pair with ennreal.some_eq_coe:
↑?m_1 < ⊤
↑
some ?m_1 < none
↓
true
 -/
#print with_top.coe_le_coe /- timeout -/

-- order/complete_lattice.lean
#print Sup_le_iff /- timeout -/
#print le_Inf_iff /- timeout -/
#print Sup_insert /- unjoinable pair with set.pair_eq_singleton:
Sup {?m_2}
↑
Sup {?m_2, ?m_2}
↓
?m_2 ⊔ Sup {?m_2}


unjoinable pair with set.pair_eq_singleton:
Sup {?m_2}
↑
Sup {?m_2, ?m_2}
↓
?m_2 ⊔ Sup {?m_2}
 -/
#print Inf_insert /- unjoinable pair with set.pair_eq_singleton:
Inf {?m_2}
↑
Inf {?m_2, ?m_2}
↓
?m_2 ⊓ Inf {?m_2}


unjoinable pair with set.pair_eq_singleton:
Inf {?m_2}
↑
Inf {?m_2, ?m_2}
↓
?m_2 ⊓ Inf {?m_2}
 -/
#print Inf_eq_top /- timeout -/
#print Sup_eq_bot /- timeout -/

-- order/filter/basic.lean
#print filter.mem_principal_sets /- timeout -/
#print filter.mem_join_sets /- timeout -/
#print filter.mem_inf_sets /- timeout -/
#print filter.mem_top_sets /- timeout -/
#print filter.mem_sup_sets /- timeout -/
#print filter.mem_Sup_sets /- timeout -/
#print filter.mem_supr_sets /- unjoinable pair with supr_empty:
true
↑
?m_2 ∈ supr ?m_3
↓
∀ (i : empty), ?m_2 ∈ (?m_3 i).sets
 -/
#print filter.sup_join /- unjoinable pair with filter.join_pure:
?m_2 ⊔ filter.join ?m_3
↑
filter.join (pure ?m_2) ⊔ filter.join ?m_3
↓
filter.join (pure ?m_2 ⊔ ?m_3)


unjoinable pair with filter.join_pure:
filter.join ?m_2 ⊔ ?m_3
↑
filter.join ?m_2 ⊔ filter.join (pure ?m_3)
↓
filter.join (?m_2 ⊔ pure ?m_3)
 -/
#print filter.eventually_Sup /- unjoinable pair with cSup_Iic:
filter.eventually ?m_2 ?m_3
↑
∀ᶠ (x : ?m_1) in Sup (set.Iic ?m_3), ?m_2 x
↓
∀ (f : filter ?m_1), f ≤ ?m_2 → filter.eventually ?m_3 f
 -/
#print filter.eventually_supr /- unjoinable pair with supr_empty:
true
↑
∀ᶠ (x : ?m_1) in ⨆ (b : empty), ?m_3 b, ?m_2 x
↓
∀ (b : empty), filter.eventually ?m_2 (?m_3 b)
 -/
#print filter.not_eventually /- unjoinable pair with filter.eventually_top:
¬∀ (x : ?m_1), ?m_2 x
↑
¬∀ᶠ (x : ?m_1) in ⊤, ?m_2 x
↓
∃ (x : ?m_1), ¬?m_2 x


unjoinable pair with filter.eventually_bot:
false
↑
¬∀ᶠ (x : ?m_1) in ⊥, ?m_2 x
↓
∃ᶠ (x : ?m_1) in ⊥, ¬?m_2 x


unjoinable pair with filter.eventually_top:
¬∀ (x : ?m_1), ?m_2 x
↑
¬∀ᶠ (x : ?m_1) in ⊤, ?m_2 x
↓
∃ (x : ?m_1), ¬?m_2 x


unjoinable pair with filter.eventually_bot:
false
↑
¬∀ᶠ (x : ?m_1) in ⊥, ?m_2 x
↓
∃ᶠ (x : ?m_1) in ⊥, ¬?m_2 x
 -/
#print filter.frequently_Sup /- unjoinable pair with cSup_Iic:
filter.frequently ?m_2 ?m_3
↑
∃ᶠ (x : ?m_1) in Sup (set.Iic ?m_3), ?m_2 x
↓
∃ (f : filter ?m_1), f ≤ ?m_2 ∧ filter.frequently ?m_3 f
 -/
#print filter.frequently_supr /- unjoinable pair with supr_empty:
filter.frequently ?m_2 ⊥
↑
∃ᶠ (x : ?m_1) in ⨆ (b : empty), ?m_3 b, ?m_2 x
↓
∃ (b : empty), filter.frequently ?m_2 (?m_3 b)
 -/
#print filter.principal_eq_bot_iff /- timeout -/
#print filter.mem_map /- timeout -/
#print filter.mem_cofinite /- timeout -/
#print filter.mem_pure_sets /- timeout -/
#print filter.mem_comap_sets /- unjoinable pair with filter.mem_comap_sets:
∃ (t : set ?m_1), t ∈ ?m_2.sets ∧ ?m_3 ⁻¹' t ⊆ ?m_4
↑
?m_2 ∈ filter.comap ?m_4 ?m_5
↓
∃ (t : set ?m_1), t ∈ ?m_3.sets ∧ ?m_4 ⁻¹' t ⊆ ?m_5


unjoinable pair with filter.mem_comap_sets:
∃ (t : set ?m_1), t ∈ ?m_2.sets ∧ ?m_3 ⁻¹' t ⊆ ?m_4
↑
?m_2 ∈ filter.comap ?m_4 ?m_5
↓
∃ (t : set ?m_1), t ∈ ?m_3.sets ∧ ?m_4 ⁻¹' t ⊆ ?m_5


unjoinable pair with filter.comap_bot:
true
↑
?m_2 ∈ filter.comap ?m_4 ⊥
↓
∃ (t : set ?m_1), ?m_2 ⁻¹' t ⊆ ?m_3


unjoinable pair with filter.comap_bot:
true
↑
?m_2 ∈ filter.comap ?m_4 ⊥
↓
∃ (t : set ?m_1), ?m_2 ⁻¹' t ⊆ ?m_3
 -/
#print filter.map_sup /- timeout -/
#print filter.comap_infi /- unjoinable pair with infi_false:
⊤
↑
filter.comap ?m_3 (⨅ (i : false), ?m_4 i)
↓
⊤
 -/
#print filter.map_eq_bot_iff /- timeout -/
#print filter.bot_prod /- unjoinable pair with filter.prod_bot:
⊥
↑
filter.prod ⊥ ⊥
↓
⊥


unjoinable pair with filter.prod_bot:
⊥
↑
filter.prod ⊥ ⊥
↓
⊥
 -/
#print filter.prod_pure_pure /- unjoinable pair with filter.prod_pure_pure:
pure (?m_3, ?m_4)
↑
filter.prod (pure ?m_3) (pure ?m_4)
↓
pure (?m_3, ?m_4)


unjoinable pair with filter.prod_pure_pure:
pure (?m_3, ?m_4)
↑
filter.prod (pure ?m_3) (pure ?m_4)
↓
pure (?m_3, ?m_4)
 -/

-- order/filter/filter_product.lean
#print filter.filter_product.of_seq_mul /- timeout -/
#print filter.filter_product.of_add /- timeout -/
#print filter.filter_product.of_sub /- timeout -/
#print filter.filter_product.of_one /- timeout -/
#print filter.filter_product.of_mul /- timeout -/
#print filter.filter_product.of_inv /- timeout -/
#print filter.filter_product.of_div /- timeout -/
#print filter.filter_product.of_max /- timeout -/
#print filter.filter_product.of_min /- timeout -/
#print filter.filter_product.of_abs /- timeout -/

-- order/filter/partial.lean
#print filter.mem_rmap /- timeout -/
#print filter.mem_rcomap' /- timeout -/
#print filter.mem_pmap /- timeout -/

-- order/filter/pointwise.lean
#print filter.mem_pointwise_zero /- timeout -/
#print filter.mem_pointwise_one /- timeout -/

-- order/lattice.lean
#print le_sup_left /- timeout -/
#print le_sup_right /- timeout -/
#print sup_le_iff /- timeout -/
#print sup_lt_iff /- timeout -/
#print inf_le_left /- timeout -/
#print inf_le_right /- timeout -/
#print lt_inf_iff /- timeout -/

-- ring_theory/algebra.lean
#print algebra.smul_mul_assoc /- timeout -/
#print alg_hom.comp_to_linear_map /- unjoinable pair with alg_hom.comp_id:
alg_hom.to_linear_map ?m_9
↑
alg_hom.to_linear_map (alg_hom.comp ?m_9 (alg_hom.id ?m_1 ?m_2))
↓
alg_hom.to_linear_map ?m_7


unjoinable pair with alg_hom.comp_id:
alg_hom.to_linear_map ?m_9
↑
alg_hom.to_linear_map (alg_hom.comp ?m_9 (alg_hom.id ?m_1 ?m_2))
↓
alg_hom.to_linear_map ?m_7
 -/
#print span_int_eq /- timeout -/

-- ring_theory/fractional_ideal.lean
#print ring.fractional_ideal.mem_zero_iff /- timeout -/
#print ring.fractional_ideal.val_add /- timeout -/
#print ring.fractional_ideal.val_mul /- timeout -/
#print ring.fractional_ideal.div_one /- timeout -/

-- ring_theory/free_comm_ring.lean
#print free_ring.coe_zero /- timeout -/
#print free_ring.coe_of /- timeout -/
#print free_ring.coe_sub /- timeout -/

-- ring_theory/free_ring.lean
#print free_ring.map_add /- unjoinable pair with add_zero:
free_ring.map ?m_3 ?m_4
↑
free_ring.map ?m_3 (?m_4 + 0)
↓
free_ring.map ?m_2 ?m_3


unjoinable pair with add_zero:
free_ring.map ?m_3 ?m_4
↑
free_ring.map ?m_3 (?m_4 + 0)
↓
free_ring.map ?m_2 ?m_3
 -/
#print free_ring.map_neg /- unjoinable pair with neg_neg:
free_ring.map ?m_3 ?m_4
↑
free_ring.map ?m_3 (- -?m_4)
↓
free_ring.map ?m_2 ?m_3
 -/
#print free_ring.map_sub /- unjoinable pair with add_sub_cancel':
free_ring.map ?m_3 ?m_4
↑
free_ring.map ?m_3 (?m_4 + ?m_5 - ?m_4)
↓
free_ring.map ?m_3 ?m_4 + free_ring.map ?m_3 ?m_5 - free_ring.map ?m_3 ?m_4


unjoinable pair with add_sub_cancel':
free_ring.map ?m_3 ?m_4
↑
free_ring.map ?m_3 (?m_4 + ?m_5 - ?m_4)
↓
free_ring.map ?m_3 ?m_4 + free_ring.map ?m_3 ?m_5 - free_ring.map ?m_3 ?m_4
 -/

-- ring_theory/ideal_operations.lean
#print ideal.add_eq_sup /- timeout -/
#print ideal.mem_comap /- timeout -/

-- ring_theory/ideals.lean
#print ideal.quotient.mk_add /- timeout -/
#print mem_nonunits_iff /- timeout -/
#print local_ring.mem_nonunits_ideal /- timeout -/

-- ring_theory/localization.lean
#print localization.to_units_coe /- timeout -/
#print localization.coe_zero /- timeout -/
#print localization.coe_one /- timeout -/
#print localization.coe_add /- timeout -/
#print localization.coe_sub /- timeout -/
#print localization.coe_neg /- timeout -/
#print localization.coe_pow /- timeout -/
#print localization.coe_is_unit /- timeout -/
#print localization.coe_mul_mk /- timeout -/
#print localization.mk_mul_mk /- timeout -/
#print localization.mk_eq /- timeout -/
#print localization.lift'_coe /- timeout -/
#print localization.lift_coe /- timeout -/
#print localization.lift'_comp_of /- timeout -/
#print localization.map_coe /- timeout -/
#print localization.away.lift_coe /- timeout -/
#print localization.fraction_ring.map_coe /- timeout -/

-- ring_theory/polynomial.lean
#print polynomial.coeff_to_subring /- timeout -/

-- ring_theory/power_series.lean
#print mv_polynomial.coe_monomial /- timeout -/
#print mv_polynomial.coe_zero /- timeout -/
#print mv_polynomial.coe_one /- timeout -/
#print mv_polynomial.coe_add /- timeout -/
#print mv_polynomial.coe_mul /- timeout -/
#print mv_polynomial.coe_C /- timeout -/
#print mv_polynomial.coe_X /- timeout -/
#print power_series.order_one /- timeout -/
#print polynomial.coe_one /- timeout -/
#print polynomial.coe_add /- timeout -/
#print polynomial.coe_mul /- timeout -/
#print polynomial.coe_X /- timeout -/

-- ring_theory/unique_factorization_domain.lean
#print associates.factor_set.coe_add /- timeout -/
#print associates.prod_coe /- timeout -/
#print associates.factors_mul /- timeout -/

-- set_theory/cardinal.lean
#print cardinal.add_def /- unjoinable pair with cardinal.mk_punit:
1 + cardinal.mk ?m_1
↑
cardinal.mk punit + cardinal.mk ?m_1
↓
cardinal.mk (punit ⊕ ?m_1)


unjoinable pair with cardinal.mk_punit:
cardinal.mk ?m_1 + 1
↑
cardinal.mk ?m_1 + cardinal.mk punit
↓
cardinal.mk (?m_1 ⊕ punit)
 -/
#print cardinal.mul_def /- timeout -/
#print cardinal.power_def /- unjoinable pair with cardinal.mk_bool:
2 ^ cardinal.mk ?m_1
↑
cardinal.mk bool ^ cardinal.mk ?m_1
↓
cardinal.mk (?m_1 → bool)


unjoinable pair with cardinal.mk_bool:
cardinal.mk ?m_1 ^ 2
↑
cardinal.mk ?m_1 ^ cardinal.mk bool
↓
cardinal.mk (bool → ?m_1)
 -/
#print cardinal.pow_cast_right /- timeout -/
#print cardinal.lift_le /- unjoinable pair with cardinal.lift_omega:
cardinal.omega ≤ cardinal.lift ?m_1
↑
cardinal.lift cardinal.omega ≤ cardinal.lift ?m_1
↓
cardinal.omega ≤ ?m_1


unjoinable pair with cardinal.lift_omega:
cardinal.lift ?m_1 ≤ cardinal.omega
↑
cardinal.lift ?m_1 ≤ cardinal.lift cardinal.omega
↓
?m_1 ≤ cardinal.omega
 -/
#print cardinal.lift_inj /- timeout -/
#print cardinal.lift_lt /- timeout -/
#print cardinal.lift_add /- unjoinable pair with add_zero:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 + 0)
↓
cardinal.lift ?m_1 + 0


unjoinable pair with add_zero:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 + 0)
↓
cardinal.lift ?m_1 + 0
 -/
#print cardinal.lift_mul /- unjoinable pair with mul_one:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 * 1)
↓
cardinal.lift ?m_1 * 1


unjoinable pair with mul_one:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 * 1)
↓
cardinal.lift ?m_1 * 1
 -/
#print cardinal.lift_power /- unjoinable pair with cardinal.lift_two_power:
2 ^ cardinal.lift ?m_1
↑
cardinal.lift (2 ^ ?m_1)
↓
cardinal.lift 2 ^ cardinal.lift ?m_1


unjoinable pair with cardinal.power_one:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 ^ 1)
↓
cardinal.lift ?m_1 ^ 1


unjoinable pair with cardinal.power_one:
cardinal.lift ?m_1
↑
cardinal.lift (?m_1 ^ 1)
↓
cardinal.lift ?m_1 ^ 1
 -/
#print cardinal.lift_two_power /- unjoinable pair with cardinal.power_one:
cardinal.lift 2
↑
cardinal.lift (2 ^ 1)
↓
2 ^ 1


unjoinable pair with cardinal.power_one:
cardinal.lift 2
↑
cardinal.lift (2 ^ 1)
↓
2 ^ 1
 -/
#print cardinal.lift_succ /- unjoinable pair with cardinal.succ_zero:
1
↑
cardinal.lift (cardinal.succ 0)
↓
1
 -/
#print cardinal.lift_max /- unjoinable pair with cardinal.lift_omega:
cardinal.omega = cardinal.lift ?m_1
↑
cardinal.lift cardinal.omega = cardinal.lift ?m_1
↓
cardinal.omega = cardinal.lift ?m_1


unjoinable pair with cardinal.lift_omega:
cardinal.lift ?m_1 = cardinal.omega
↑
cardinal.lift ?m_1 = cardinal.lift cardinal.omega
↓
cardinal.lift ?m_1 = cardinal.omega
 -/
#print cardinal.lift_nat_cast /- timeout -/
#print cardinal.nat_cast_pow /- timeout -/
#print cardinal.nat_cast_le /- timeout -/
#print cardinal.nat_cast_lt /- timeout -/
#print cardinal.nat_cast_inj /- timeout -/
#print cardinal.nat_succ /- timeout -/
#print cardinal.finset_card /- unjoinable pair with finset.card_fin:
↑?m_1
↑
↑(finset.card finset.univ)
↓
cardinal.mk ↥set.univ
 -/

-- set_theory/cofinality.lean
#print ordinal.cof_eq_zero /- unjoinable pair with ordinal.cof_omega:
cardinal.omega = 0
↑
ordinal.cof ordinal.omega = 0
↓
ordinal.omega = 0
 -/
#print ordinal.cof_succ /- unjoinable pair with ordinal.succ_zero:
ordinal.cof 1
↑
ordinal.cof (ordinal.succ 0)
↓
1
 -/
#print ordinal.cof_eq_one_iff_is_succ /- unjoinable pair with ordinal.cof_omega:
cardinal.omega = 1
↑
ordinal.cof ordinal.omega = 1
↓
∃ (a : ordinal), ordinal.omega = ordinal.succ a
 -/

-- set_theory/lists.lean
#print lists'.mem_cons /- timeout -/

-- set_theory/ordinal.lean
#print ordinal.type_lt /- timeout -/
#print ordinal.le_zero /- timeout -/
#print ordinal.type_add /- timeout -/
#print ordinal.card_nat /- timeout -/
#print ordinal.lift_le /- timeout -/
#print ordinal.lift_inj /- timeout -/
#print ordinal.lift_lt /- unjoinable pair with ordinal.lift_univ:
ordinal.univ < ordinal.lift ?m_1
↑
ordinal.lift ordinal.univ < ordinal.lift ?m_1
↓
ordinal.univ < ?m_1


unjoinable pair with ordinal.lift_univ:
ordinal.lift ?m_1 < ordinal.univ
↑
ordinal.lift ?m_1 < ordinal.lift ordinal.univ
↓
?m_1 < ordinal.univ
 -/
#print ordinal.lift_add /- unjoinable pair with add_zero:
ordinal.lift ?m_1
↑
ordinal.lift (?m_1 + 0)
↓
ordinal.lift ?m_1 + 0


unjoinable pair with add_zero:
ordinal.lift ?m_1
↑
ordinal.lift (?m_1 + 0)
↓
ordinal.lift ?m_1 + 0
 -/
#print ordinal.lift_succ /- unjoinable pair with ordinal.succ_zero:
1
↑
ordinal.lift (ordinal.succ 0)
↓
1
 -/
#print ordinal.typein_le_typein /- timeout -/
#print ordinal.succ_lt_succ /- unjoinable pair with ordinal.succ_zero:
1 < ordinal.succ ?m_1
↑
ordinal.succ 0 < ordinal.succ ?m_1
↓
0 < ?m_1


unjoinable pair with ordinal.succ_zero:
ordinal.succ ?m_1 < 1
↑
ordinal.succ ?m_1 < ordinal.succ 0
↓
?m_1 < 0
 -/
#print ordinal.succ_le_succ /- unjoinable pair with ordinal.succ_zero:
1 ≤ ordinal.succ ?m_1
↑
ordinal.succ 0 ≤ ordinal.succ ?m_1
↓
0 ≤ ?m_1


unjoinable pair with ordinal.succ_zero:
ordinal.succ ?m_1 ≤ 1
↑
ordinal.succ ?m_1 ≤ ordinal.succ 0
↓
?m_1 = 0
 -/
#print ordinal.card_eq_zero /- timeout -/
#print ordinal.type_eq_zero_iff_empty /- timeout -/
#print ordinal.pred_succ /- unjoinable pair with ordinal.succ_zero:
ordinal.pred 1
↑
ordinal.pred (ordinal.succ 0)
↓
0
 -/
#print ordinal.lift_is_limit /- unjoinable pair with ordinal.lift_univ:
ordinal.is_limit ordinal.univ
↑
ordinal.is_limit (ordinal.lift ordinal.univ)
↓
ordinal.is_limit ordinal.univ
 -/
#print ordinal.limit_rec_on_limit /- unjoinable pair with ordinal.limit_rec_on_zero:
?m_1
↑
ordinal.limit_rec_on 0 ?m_2 ?m_3 ?m_4
↓
?m_1 0 ?m_2 (λ (x : ordinal) (h : x < 0), ordinal.limit_rec_on x ?m_4 ?m_5 ?m_1)


unjoinable pair with ordinal.limit_rec_on_zero:
?m_1
↑
ordinal.limit_rec_on 0 ?m_2 ?m_3 ?m_4
↓
?m_1 0 ?m_2 (λ (x : ordinal) (h : x < 0), ordinal.limit_rec_on x ?m_4 ?m_5 ?m_1)


unjoinable pair with ordinal.limit_rec_on_zero:
?m_1
↑
ordinal.limit_rec_on 0 ?m_2 ?m_3 ?m_4
↓
?m_1 0 ?m_2 (λ (x : ordinal) (h : x < 0), ordinal.limit_rec_on x ?m_4 ?m_5 ?m_1)
 -/
#print ordinal.lift_mul /- unjoinable pair with ordinal.zero_mul:
0
↑
ordinal.lift (0 * ?m_1)
↓
0 * ordinal.lift ?m_1


unjoinable pair with ordinal.zero_mul:
0
↑
ordinal.lift (0 * ?m_1)
↓
0 * ordinal.lift ?m_1
 -/
#print ordinal.mul_add_one /- timeout -/
#print cardinal.card_ord /- unjoinable pair with cardinal.ord_omega:
ordinal.card ordinal.omega
↑
ordinal.card (cardinal.ord cardinal.omega)
↓
cardinal.omega
 -/
#print cardinal.ord_le_ord /- timeout -/
#print cardinal.ord_lt_ord /- unjoinable pair with cardinal.ord_omega:
ordinal.omega < cardinal.ord ?m_1
↑
cardinal.ord cardinal.omega < cardinal.ord ?m_1
↓
cardinal.omega < ?m_1


unjoinable pair with cardinal.ord_omega:
cardinal.ord ?m_1 < ordinal.omega
↑
cardinal.ord ?m_1 < cardinal.ord cardinal.omega
↓
?m_1 < cardinal.omega
 -/
#print cardinal.ord_nat /- timeout -/
#print ordinal.nat_cast_mul /- timeout -/
#print ordinal.nat_cast_le /- timeout -/
#print ordinal.nat_cast_lt /- timeout -/
#print ordinal.nat_cast_inj /- timeout -/
#print ordinal.nat_cast_eq_zero /- timeout -/
#print ordinal.nat_cast_pos /- timeout -/
#print ordinal.nat_cast_sub /- timeout -/
#print ordinal.nat_cast_div /- timeout -/
#print ordinal.nat_le_card /- timeout -/
#print ordinal.nat_lt_card /- timeout -/
#print ordinal.card_lt_nat /- timeout -/
#print ordinal.card_le_nat /- timeout -/
#print ordinal.card_eq_nat /- timeout -/
#print ordinal.lift_nat_cast /- timeout -/
#print ordinal.CNF_rec_ne_zero /- unjoinable pair with ordinal.CNF_rec_zero:
?m_1
↑
ordinal.CNF_rec ?m_2 ?m_4 ?m_5 0
↓
?m_1 0 ?m_2 _ (ordinal.CNF_rec ?m_4 ?m_6 ?m_1 (0 % ?m_3 ^ ordinal.log ?m_3 0))


unjoinable pair with ordinal.CNF_rec_zero:
?m_1
↑
ordinal.CNF_rec ?m_2 ?m_4 ?m_5 0
↓
?m_1 0 ?m_2 _ (ordinal.CNF_rec ?m_4 ?m_6 ?m_1 (0 % ?m_3 ^ ordinal.log ?m_3 0))
 -/
#print ordinal.deriv_succ /- unjoinable pair with ordinal.succ_zero:
ordinal.deriv ?m_1 1
↑
ordinal.deriv ?m_1 (ordinal.succ 0)
↓
ordinal.nfp ?m_1 (ordinal.succ (ordinal.nfp ?m_1 0))
 -/
#print cardinal.aleph_idx_lt /- timeout -/
#print cardinal.aleph_idx_le /- unjoinable pair with cardinal.aleph_idx_aleph':
?m_1 ≤ cardinal.aleph_idx ?m_2
↑
cardinal.aleph_idx (cardinal.aleph' ?m_1) ≤ cardinal.aleph_idx ?m_2
↓
cardinal.aleph' ?m_1 ≤ ?m_2


unjoinable pair with cardinal.aleph_idx_aleph':
cardinal.aleph_idx ?m_1 ≤ ?m_2
↑
cardinal.aleph_idx ?m_1 ≤ cardinal.aleph_idx (cardinal.aleph' ?m_2)
↓
?m_1 ≤ cardinal.aleph' ?m_2
 -/
#print cardinal.aleph'_lt /- unjoinable pair with cardinal.aleph'_zero:
0 < cardinal.aleph' ?m_1
↑
cardinal.aleph' 0 < cardinal.aleph' ?m_1
↓
0 < ?m_1


unjoinable pair with cardinal.aleph'_zero:
cardinal.aleph' ?m_1 < 0
↑
cardinal.aleph' ?m_1 < cardinal.aleph' 0
↓
?m_1 < 0
 -/
#print cardinal.aleph'_le /- timeout -/
#print cardinal.aleph_idx_aleph' /- unjoinable pair with cardinal.aleph'_zero:
cardinal.aleph_idx 0
↑
cardinal.aleph_idx (cardinal.aleph' 0)
↓
0
 -/
#print cardinal.aleph'_succ /- unjoinable pair with ordinal.succ_zero:
cardinal.aleph' 1
↑
cardinal.aleph' (ordinal.succ 0)
↓
1
 -/
#print cardinal.aleph'_nat /- timeout -/
#print cardinal.aleph_lt /- timeout -/
#print cardinal.aleph_le /- timeout -/
#print cardinal.aleph_succ /- unjoinable pair with ordinal.succ_zero:
cardinal.aleph 1
↑
cardinal.aleph (ordinal.succ 0)
↓
cardinal.succ cardinal.omega
 -/

-- set_theory/ordinal_notation.lean
#print onote.zero_add /- timeout -/
#print onote.repr_add /- timeout -/
#print onote.repr_sub /- timeout -/
#print onote.zero_mul /- timeout -/
#print onote.mul_zero /- timeout -/

-- set_theory/pgame.lean
#print pgame.mk_le_mk /- timeout -/
#print pgame.mk_lt_mk /- timeout -/

-- set_theory/zfc.lean
#print Set.mem_insert /- timeout -/
#print Set.mem_singleton /- timeout -/
#print Set.mem_pair /- timeout -/
#print Set.omega_zero /- timeout -/
#print Set.mem_sep /- timeout -/
#print Set.mem_powerset /- timeout -/
#print Set.mem_Union /- timeout -/
#print Set.mem_union /- timeout -/
#print Set.mem_inter /- timeout -/
#print Set.mem_diff /- timeout -/
#print Set.mem_image /- timeout -/
#print Set.mem_pair_sep /- timeout -/
#print Set.pair_mem_prod /- timeout -/
#print Class.to_Set_of_Set /- timeout -/
#print Class.mem_hom_left /- timeout -/
#print Class.mem_hom_right /- timeout -/
#print Class.subset_hom /- timeout -/
#print Class.sep_hom /- timeout -/
#print Class.empty_hom /- timeout -/
#print Class.insert_hom /- timeout -/
#print Class.union_hom /- timeout -/
#print Class.inter_hom /- timeout -/
#print Class.diff_hom /- timeout -/
#print Class.powerset_hom /- timeout -/
#print Class.Union_hom /- timeout -/

-- topology/algebra/module.lean
#print continuous_linear_map.coe_zero /- timeout -/
#print continuous_linear_map.coe_id /- timeout -/
#print continuous_linear_map.coe_add /- timeout -/
#print continuous_linear_map.coe_comp /- timeout -/
#print continuous_linear_map.coe_apply /- timeout -/
#print continuous_linear_map.smul_right_one_eq_iff /- timeout -/
#print continuous_linear_equiv.map_eq_zero_iff /- timeout -/
#print continuous_linear_equiv.coe_comp_coe_symm /- timeout -/
#print continuous_linear_equiv.coe_symm_comp_coe /- timeout -/

-- topology/algebra/ring.lean
#print ideal.coe_closure /- timeout -/

-- topology/category/Top/open_nhds.lean
#print topological_space.open_nhds.inclusion_obj /- timeout -/
#print topological_space.open_nhds.map_obj /- unjoinable pair with subtype.eta:
(topological_space.open_nhds.map ?m_3 ?m_4).obj ?m_5
↑
(topological_space.open_nhds.map ?m_3 ?m_4).obj ⟨?m_5.val, ?m_6⟩
↓
⟨(topological_space.opens.map ?m_4).obj ?m_5.val, ?m_6⟩
 -/
#print topological_space.open_nhds.map_id_obj /- timeout -/
#print topological_space.open_nhds.map_id_obj_unop /- timeout -/

-- topology/category/Top/opens.lean
#print topological_space.opens.map_obj /- unjoinable pair with topological_space.opens.map_id_obj:
⟨?m_2, ?m_3⟩
↑
(topological_space.opens.map (𝟙 ?m_1)).obj ⟨?m_2, ?m_3⟩
↓
⟨(𝟙 ?m_1).val ⁻¹' ?m_2, _⟩


unjoinable pair with topological_space.opens.map_id_obj:
⟨?m_2, ?m_3⟩
↑
(topological_space.opens.map (𝟙 ?m_1)).obj ⟨?m_2, ?m_3⟩
↓
⟨(𝟙 ?m_1).val ⁻¹' ?m_2, _⟩


unjoinable pair with subtype.eta:
(topological_space.opens.map ?m_3).obj ?m_4
↑
(topological_space.opens.map ?m_3).obj ⟨?m_4.val, ?m_5⟩
↓
⟨?m_3.val ⁻¹' ?m_4.val, _⟩
 -/
#print topological_space.opens.op_map_id_obj /- timeout -/
#print topological_space.opens.map_id_hom_app /- timeout -/
#print topological_space.opens.map_comp_obj /- timeout -/
#print topological_space.opens.map_comp_obj' /- timeout -/
#print topological_space.opens.map_comp_obj_unop /- timeout -/
#print topological_space.opens.op_map_comp_obj /- timeout -/
#print topological_space.opens.map_comp_hom_app /- unjoinable pair with topological_space.opens.map_comp_hom_app:
𝟙 ((topological_space.opens.map (?m_3 ≫ ?m_4)).obj ?m_5)
↑
(topological_space.opens.map_comp ?m_4 ?m_5).hom.app ?m_6
↓
category_theory.eq_to_hom _
 -/
#print topological_space.opens.map_comp_inv_app /- timeout -/
#print topological_space.opens.map_iso_hom_app /- unjoinable pair with topological_space.opens.map_iso_hom_app:
category_theory.eq_to_hom _
↑
(topological_space.opens.map_iso ?m_3 ?m_4 ?m_5).hom.app ?m_6
↓
category_theory.eq_to_hom _
 -/
#print topological_space.opens.map_iso_inv_app /- timeout -/

-- topology/category/UniformSpace.lean
#print UniformSpace.extension_comp_coe /- unjoinable pair with category_theory.category.comp_id:
UniformSpace.extension_hom (UniformSpace.completion_hom ?m_1)
↑
UniformSpace.extension_hom
  (UniformSpace.completion_hom ?m_1 ≫
     𝟙 ((category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj (UniformSpace.completion_functor.obj ?m_1)))
↓
𝟙 ((category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj (UniformSpace.completion_functor.obj ?m_1))


unjoinable pair with category_theory.category.comp_id:
UniformSpace.extension_hom (UniformSpace.completion_hom ?m_1)
↑
UniformSpace.extension_hom
  (UniformSpace.completion_hom ?m_1 ≫
     𝟙 ((category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj (UniformSpace.completion_functor.obj ?m_1)))
↓
𝟙 ((category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj (UniformSpace.completion_functor.obj ?m_1))
 -/

-- topology/instances/ennreal.lean
#print ennreal.tendsto_inv_iff /- unjoinable pair with ennreal.inv_inv:
filter.tendsto (λ (x : ?m_1), (?m_2 x)⁻¹) ?m_3 (nhds ?m_4)
↑
filter.tendsto (λ (x : ?m_1), (?m_2 x)⁻¹) ?m_3 (nhds ?m_4⁻¹⁻¹)
↓
filter.tendsto ?m_2 ?m_3 (nhds ?m_4⁻¹)
 -/

-- topology/instances/real.lean
#print rat.dist_cast /- timeout -/
#print int.dist_cast_real /- unjoinable pair with int.cast_zero:
dist 0 ↑?m_1
↑
dist ↑0 ↑?m_1
↓
dist 0 ?m_1


unjoinable pair with int.cast_zero:
∥↑?m_1∥
↑
dist ↑?m_1 ↑0
↓
∥?m_1∥
 -/
#print int.dist_cast_rat /- unjoinable pair with int.cast_zero:
dist 0 ↑?m_1
↑
dist ↑0 ↑?m_1
↓
dist 0 ?m_1
 -/

-- topology/metric_space/basic.lean
#print dist_eq_zero /- timeout -/
#print zero_eq_dist /- timeout -/
#print dist_pos /- timeout -/
#print nndist_eq_zero /- timeout -/
#print zero_eq_nndist /- timeout -/
#print metric.mem_closed_ball /- timeout -/

-- topology/metric_space/emetric_space.lean
#print emetric.mem_ball /- timeout -/
#print emetric.mem_closed_ball /- timeout -/

-- topology/order.lean
#print induced_inf /- unjoinable pair with bot_inf_eq:
topological_space.induced ?m_3 ⊥
↑
topological_space.induced ?m_3 (⊥ ⊓ ?m_4)
↓
topological_space.induced ?m_3 ⊥ ⊓ topological_space.induced ?m_3 ?m_4


unjoinable pair with bot_inf_eq:
topological_space.induced ?m_3 ⊥
↑
topological_space.induced ?m_3 (⊥ ⊓ ?m_4)
↓
topological_space.induced ?m_3 ⊥ ⊓ topological_space.induced ?m_3 ?m_4
 -/
#print coinduced_sup /- unjoinable pair with bot_sup_eq:
topological_space.coinduced ?m_3 ?m_4
↑
topological_space.coinduced ?m_3 (⊥ ⊔ ?m_4)
↓
⊥ ⊔ topological_space.coinduced ?m_3 ?m_4


unjoinable pair with bot_sup_eq:
topological_space.coinduced ?m_3 ?m_4
↑
topological_space.coinduced ?m_3 (⊥ ⊔ ?m_4)
↓
⊥ ⊔ topological_space.coinduced ?m_3 ?m_4
 -/

-- topology/separation.lean
#print nhds_eq_nhds_iff /- timeout -/
#print nhds_le_nhds_iff /- timeout -/

-- topology/sheaves/presheaf.lean
#print Top.presheaf.pushforward.id_hom_app /- timeout -/
#print Top.presheaf.pushforward.comp_hom_app /- timeout -/
#print Top.presheaf.pushforward.comp_inv_app /- timeout -/

-- topology/topological_fiber_bundle.lean
#print topological_fiber_bundle_core.mem_triv_change_source /- timeout -/
#print topological_fiber_bundle_core.mem_local_triv'_source /- timeout -/
#print topological_fiber_bundle_core.mem_local_triv_source /- timeout -/
#print topological_fiber_bundle_core.mem_local_triv_target /- timeout -/
#print topological_fiber_bundle_core.mem_local_triv_at_source /- timeout -/

-- topology/uniform_space/basic.lean
#print mem_id_rel /- unjoinable pair with prod.mk.eta:
?m_2 ∈ id_rel
↑
(?m_2.fst, ?m_2.snd) ∈ id_rel
↓
?m_2.fst = ?m_2.snd


unjoinable pair with prod.mk.eta:
?m_2 ∈ id_rel
↑
(?m_2.fst, ?m_2.snd) ∈ id_rel
↓
?m_2.fst = ?m_2.snd
 -/
#print mem_comp_rel /- timeout -/


/- OK: No commutativity lemma is marked simp. -/
/home/runner/work/mathlib/mathlib/src/lint_mathlib.lean:2:0: error: Linting did not succeed