MathGraph.
Explore · real source-pinned knowledge

Find the mathematics. Then inspect what is known about it.

Search genuine declarations from an exact Mathlib revision alongside MathGraph’s qualified evidence objects and one bounded reusable capability. Names and structural references help you navigate; they do not create proof or implication.

  • 2,345source-indexed declarations
  • 13pinned Mathlib modules
  • 3,571typed structural relations
  • 1qualified reusable capability
Source indexing is not independent proof checking.These declarations and structural relations are reproduced from pinned source bytes. Their independent verification is NOT_CHECKED; the catalogue grants no terminal form or action authority.
Living knowledge catalogue

Search exact mathematical objects and evidence

Deterministic name and metadata ranking · no semantic inference

2372 of 2372 displayed.

  1. AddCommGroup.toGrindIntModule

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2. AddCommMonoid.toGrindNatModule

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  3. AddHom.mulLeft

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  4. AddHom.mulLeft_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  5. AddHom.mulRight

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  6. AddHom.mulRight_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  7. AddMonoid.End.mulLeft

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  8. AddMonoid.End.mulLeft_apply_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  9. AddMonoid.End.mulRight

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  10. AddMonoid.End.mulRight_apply_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  11. AddMonoid.End.mulRight_eq_mulLeft

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  12. AddMonoidHom.coe_flip_mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  13. AddMonoidHom.coe_mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  14. AddMonoidHom.coe_mulLeft

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  15. AddMonoidHom.coe_mulRight

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  16. AddMonoidHom.map_mul_iff

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  17. AddMonoidHom.mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  18. AddMonoidHom.mulLeft

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  19. AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  20. AddMonoidHom.mulRight

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  21. AddMonoidHom.mulRight_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  22. AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  23. AddMonoidHom.mul_apply

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  24. AddSemigroup.to_isAssociative

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  25. AddSemigroup.to_isLawfulIdentity

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  26. Bool.involutive_not

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  27. Complex.abs_cpow_inv_two_im

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  28. Complex.cpow_inv_two_im_eq_neg_sqrt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  29. Complex.cpow_inv_two_im_eq_sqrt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  30. Complex.cpow_inv_two_re

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  31. Complex.cpow_mul_ofReal_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  32. Complex.cpow_ofReal

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  33. Complex.cpow_ofReal_im

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  34. Complex.cpow_ofReal_re

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  35. Complex.inv_natCast_cpow_ofReal_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  36. Complex.norm_cpow_eq_rpow_re_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  37. Complex.norm_cpow_eq_rpow_re_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  38. Complex.norm_cpow_inv_nat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  39. Complex.norm_cpow_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  40. Complex.norm_cpow_of_imp

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  41. Complex.norm_cpow_of_ne_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  42. Complex.norm_cpow_real

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  43. Complex.norm_log_natCast_le_rpow_div

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  44. Complex.norm_natCast_cpow_le_norm_natCast_cpow_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  45. Complex.norm_natCast_cpow_le_norm_natCast_cpow_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  46. Complex.norm_natCast_cpow_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  47. Complex.norm_natCast_cpow_of_re_ne_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  48. Complex.norm_natCast_cpow_pos_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  49. Complex.norm_ofReal_cpow_eventually_eq_atTop

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  50. Complex.norm_prime_cpow_le_one_half

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  51. Complex.ofReal_cpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  52. Complex.ofReal_cpow_of_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  53. Complex.one_sub_prime_cpow_ne_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  54. Decidable.List.eq_or_ne_mem_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  55. Decidable.eq_iff_ge_not_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  56. Decidable.eq_iff_le_not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  57. Decidable.eq_or_lt_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  58. Decidable.eq_or_lt_of_le'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  59. Decidable.le_iff_eq_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  60. Decidable.le_iff_eq_or_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  61. Decidable.ne_iff_gt_iff_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  62. Decidable.ne_iff_lt_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  63. DenselyOrdered

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  64. DenselyOrdered.dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  65. DenselyOrdered.dense'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  66. DenselyOrdered.mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  67. DenselyOrdered.mk'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  68. DivisionMonoid.toDivInvOneMonoid

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  69. Eq.ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  70. Eq.le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  71. Eq.not_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  72. Eq.not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  73. Eq.trans_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  74. Eq.trans_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  75. Eq.trans_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  76. Eq.trans_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  77. Equiv.Finset.disjUnionEquiv

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  78. Equiv.Finset.disjUnionEquiv_inl

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  79. Equiv.Finset.disjUnionEquiv_inr

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  80. Equiv.Finset.disjUnionEquiv_symm_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  81. Equiv.Finset.disjUnionEquiv_symm_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  82. Equiv.Finset.union

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  83. Equiv.Finset.union_inl

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  84. Equiv.Finset.union_inr

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  85. Equiv.Finset.union_symm_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  86. Equiv.Finset.union_symm_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  87. Equiv.piFinsetUnion

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  88. Equiv.piFinsetUnion_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  89. Equiv.piFinsetUnion_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  90. Equiv.setSubtypeComm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  91. Equiv.setSubtypeComm_apply

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  92. Equiv.setSubtypeComm_symm_apply

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  93. Finset.Nonempty.attach

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  94. Finset.Nonempty.not_disjoint

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  95. Finset.Nonempty.not_empty_toList

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  96. Finset.Nonempty.toList_ne_nil

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  97. Finset.Nontrivial.erase_nonempty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  98. Finset.Nontrivial.exists_cons_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  99. Finset.attach_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  100. Finset.attach_eq_empty_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  101. Finset.attach_nonempty_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  102. Finset.choose

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  103. Finset.chooseX

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  104. Finset.choose_eq_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  105. Finset.choose_mem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  106. Finset.choose_property

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  107. Finset.choose_spec

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  108. Finset.disjUnion_eq_union

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  109. Finset.disjoint_disjUnion_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  110. Finset.disjoint_disjUnion_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  111. Finset.disjoint_erase_comm

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  112. Finset.disjoint_erase_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  113. Finset.disjoint_filter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  114. Finset.disjoint_filter_filter'

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  115. Finset.disjoint_filter_filter_not

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  116. Finset.disjoint_insert_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  117. Finset.disjoint_of_erase_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  118. Finset.disjoint_of_erase_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  119. Finset.disjoint_of_subset_iff_left_eq_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  120. Finset.disjoint_or_nonempty_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  121. Finset.disjoint_sdiff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  122. Finset.disjoint_sdiff_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  123. Finset.disjoint_union_left

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  124. Finset.disjoint_union_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  125. Finset.empty_toList

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  126. Finset.equivToSet

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  127. Finset.erase_cons

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  128. Finset.erase_cons_of_ne

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  129. Finset.erase_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  130. Finset.erase_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  131. Finset.erase_eq_empty_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  132. Finset.erase_eq_iff_eq_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  133. Finset.erase_injOn'

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  134. Finset.erase_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  135. Finset.erase_insert_eq_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  136. Finset.erase_insert_of_ne

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  137. Finset.erase_insert_subset

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  138. Finset.erase_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  139. Finset.erase_inter_comm

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  140. Finset.erase_nonempty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  141. Finset.erase_sdiff_comm

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  142. Finset.erase_sdiff_distrib

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  143. Finset.erase_sdiff_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  144. Finset.erase_singleton

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  145. Finset.erase_ssubset

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  146. Finset.erase_ssubset_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  147. Finset.erase_subset_iff_of_mem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  148. Finset.erase_union_distrib

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  149. Finset.erase_union_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  150. Finset.erase_union_of_mem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  151. Finset.filter_and

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  152. Finset.filter_and_not

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  153. Finset.filter_cons

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  154. Finset.filter_cons_of_neg

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  155. Finset.filter_cons_of_pos

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  156. Finset.filter_disjUnion

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  157. Finset.filter_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  158. Finset.filter_eq'

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  159. Finset.filter_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  160. Finset.filter_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  161. Finset.filter_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  162. Finset.filter_inter_distrib

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  163. Finset.filter_mem_eq_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  164. Finset.filter_ne

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  165. Finset.filter_ne'

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  166. Finset.filter_not

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  167. Finset.filter_notMem_eq_sdiff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  168. Finset.filter_or

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  169. Finset.filter_singleton

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  170. Finset.filter_union

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  171. Finset.filter_union_filter_not_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  172. Finset.filter_union_filter_of_codisjoint

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  173. Finset.filter_union_right

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  174. Finset.insert_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  175. Finset.insert_erase_eq_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  176. Finset.insert_erase_invOn

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  177. Finset.insert_erase_subset

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  178. Finset.insert_inter_distrib

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  179. Finset.inter_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  180. Finset.inter_filter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  181. Finset.isDirected_le

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  182. Finset.isDirected_subset

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  183. Finset.isEmpty_of_forall_eq_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  184. Finset.mem_union_of_disjoint

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  185. Finset.not_disjoint_iff_nonempty_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  186. Finset.pairwiseDisjoint_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  187. Finset.range_filter_eq

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  188. Finset.range_inter_range

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  189. Finset.range_union_range

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  190. Finset.sdiff_disjoint

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  191. Finset.sdiff_eq_filter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  192. Finset.sdiff_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  193. Finset.sdiff_erase_self

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  194. Finset.sdiff_insert

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  195. Finset.sdiff_insert_insert_of_mem_of_notMem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  196. Finset.sdiff_singleton_eq_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  197. Finset.sdiff_union_erase_cancel

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  198. Finset.ssubset_iff_exists_subset_erase

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  199. Finset.subset_insert_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  200. Finset.subset_insert_iff_of_notMem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  201. Finset.subset_union_elim

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  202. Finset.toList_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  203. Finset.toList_eq_nil

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  204. Finset.union_erase_of_mem

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  205. Finset.univ_finset_eq_singleton_empty_iff

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  206. Finset.univ_finset_of_isEmpty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  207. Function.Bijective.comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  208. Function.Bijective.comp_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  209. Function.Bijective.existsUnique

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  210. Function.Bijective.existsUnique_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  211. Function.Bijective.injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  212. Function.Bijective.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  213. Function.Bijective.of_comp_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  214. Function.Bijective.of_comp_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  215. Function.Bijective.of_comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  216. Function.Bijective.piMap

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  217. Function.Bijective.surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  218. Function.FactorsThrough

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  219. Function.FactorsThrough.comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  220. Function.FactorsThrough.comp_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  221. Function.FactorsThrough.extend_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  222. Function.FactorsThrough.extend_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  223. Function.FactorsThrough.rfl

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  224. Function.HasUncurry

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  225. Function.HasUncurry.mk

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  226. Function.HasUncurry.uncurry

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  227. Function.Injective.antisymm_onFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  228. Function.Injective.bijective₂_of_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  229. Function.Injective.comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  230. Function.Injective.decidableEq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  231. Function.Injective.dite

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  232. Function.Injective.extend_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  233. Function.Injective.extend_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  234. Function.Injective.factorsThrough

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  235. Function.Injective.hasLeftInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  236. Function.Injective.isLinearOrder_onFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  237. Function.Injective.isPartialInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  238. Function.Injective.isPartialOrder_onFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  239. Function.Injective.isStrictTotalOrder_onFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  240. Function.Injective.linearOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  241. Function.Injective.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  242. Function.Injective.nonempty_apply_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  243. Function.Injective.of_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  244. Function.Injective.of_comp_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  245. Function.Injective.of_comp_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  246. Function.Injective.of_comp_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  247. Function.Injective.partialOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  248. Function.Injective.piMap

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  249. Function.Injective.preorder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  250. Function.Injective.surjective_comp_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  251. Function.Injective.surjective_comp_right'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  252. Function.Injective.trichotomous_onFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  253. Function.Injective2

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  254. Function.Injective2.eq_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  255. Function.Injective2.left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  256. Function.Injective2.left'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  257. Function.Injective2.right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  258. Function.Injective2.right'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  259. Function.Injective2.uncurry

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  260. Function.Involutive

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  261. Function.Involutive.bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  262. Function.Involutive.comp_self

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  263. Function.Involutive.eq_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  264. Function.Involutive.exists_mem_and_apply_eq_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  265. Function.Involutive.injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  266. Function.Involutive.ite_not

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  267. Function.Involutive.leftInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  268. Function.Involutive.leftInverse_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  269. Function.Involutive.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  270. Function.Involutive.rightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  271. Function.Involutive.surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  272. Function.IsPartialInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  273. Function.IsPartialInv.comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  274. Function.IsPartialInv.eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  275. Function.IsPartialInv.get_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  276. Function.IsPartialInv.injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  277. Function.IsPartialInv.surjective_getD

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  278. Function.LeftInverse.cast_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  279. Function.LeftInverse.comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  280. Function.LeftInverse.comp_eq_id

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  281. Function.LeftInverse.eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  282. Function.LeftInverse.eq_rec_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  283. Function.LeftInverse.eq_rec_on_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  284. Function.LeftInverse.eq_rightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  285. Function.LeftInverse.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  286. Function.LeftInverse.rightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  287. Function.LeftInverse.rightInverse_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  288. Function.LeftInverse.rightInverse_of_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  289. Function.LeftInverse.surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  290. Function.RightInverse.comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  291. Function.RightInverse.comp_eq_id

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  292. Function.RightInverse.eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  293. Function.RightInverse.injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  294. Function.RightInverse.leftInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  295. Function.RightInverse.leftInverse_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  296. Function.RightInverse.leftInverse_of_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  297. Function.RightInverse.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  298. Function.Surjective.bijective₂_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  299. Function.Surjective.comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  300. Function.Surjective.exists

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  301. Function.Surjective.exists₂

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  302. Function.Surjective.exists₃

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  303. Function.Surjective.forall

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  304. Function.Surjective.forall₂

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  305. Function.Surjective.forall₃

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  306. Function.Surjective.hasRightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  307. Function.Surjective.injective_comp_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  308. Function.Surjective.list_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  309. Function.Surjective.of_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  310. Function.Surjective.of_comp_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  311. Function.Surjective.of_comp_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  312. Function.Surjective.of_comp_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  313. Function.Surjective.piMap

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  314. Function.Surjective.right_cancellable

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  315. Function._aux_Mathlib_Logic_Function_Basic___unexpand_Function_HasUncurry_uncurry_1

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  316. Function.apply_extend

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  317. Function.apply_invFun_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  318. Function.apply_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  319. Function.apply_update₂

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  320. Function.bijective_iff_existsUnique

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  321. Function.bijective_iff_has_inverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  322. Function.bijective_of_subsingleton

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  323. Function.bijective_of_subsingleton'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  324. Function.cantor_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  325. Function.cantor_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  326. Function.comp_surjInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  327. Function.comp_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  328. Function.const_def

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  329. Function.const_inj

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  330. Function.const_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  331. Function.const_le_const

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  332. Function.const_lt_const

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  333. Function.curry_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  334. Function.curry_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  335. Function.decidableEqPFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  336. Function.eq_const_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  337. Function.eq_update_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  338. Function.eq_update_self_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  339. Function.eval

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  340. Function.eval_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  341. Function.exists_fixed_point_of_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  342. Function.exists_update_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  343. Function.extend

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  344. Function.extend_apply'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  345. Function.extend_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  346. Function.extend_const

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  347. Function.extend_def

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  348. Function.extend_id

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  349. Function.extend_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  350. Function.factorsThrough_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  351. Function.flip_curry

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  352. Function.forall_update_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  353. Function.funext_iff_of_subsingleton

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  354. Function.hasUncurryBase

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  355. Function.hasUncurryInduction

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  356. Function.hfunext

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  357. Function.injective_comp_left_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  358. Function.injective_comp_right_iff_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  359. Function.injective_iff_hasLeftInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  360. Function.injective_of_isPartialInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  361. Function.injective_of_isPartialInv_right

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  362. Function.injective_of_subsingleton

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  363. Function.injective_surjInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  364. Function.instAntisymmSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  365. Function.instAsymmOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  366. Function.instAsymmSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  367. Function.instIrreflOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  368. Function.instIrreflSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  369. Function.instIsEquivOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  370. Function.instIsEquivSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  371. Function.instIsLinearOrderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  372. Function.instIsPartialOrderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  373. Function.instIsPreorderOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  374. Function.instIsPreorderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  375. Function.instIsStrictOrderOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  376. Function.instIsStrictOrderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  377. Function.instIsStrictTotalOrderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  378. Function.instIsStrictWeakOrderOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  379. Function.instIsStrictWeakOrderSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  380. Function.instIsTransOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  381. Function.instIsTransSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  382. Function.instReflOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  383. Function.instReflSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  384. Function.instSymmOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  385. Function.instSymmSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  386. Function.instTotalOnFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  387. Function.instTotalSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  388. Function.instTrichotomousSwapProp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  389. Function.invFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  390. Function.invFun_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  391. Function.invFun_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  392. Function.invFun_eq_of_injective_of_rightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  393. Function.invFun_neg

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  394. Function.invFun_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  395. Function.isPartialInv_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  396. Function.leftInverse_iff_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  397. Function.leftInverse_invFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  398. Function.leftInverse_surjInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  399. Function.ne_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  400. Function.ne_update_self_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  401. Function.not_bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  402. Function.not_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  403. Function.not_injective_const

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  404. Function.not_injective_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  405. Function.not_involutive

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  406. Function.not_surjective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  407. Function.not_surjective_Type

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  408. Function.onFun_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  409. Function.onFun_comp_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  410. Function.onFun_onFun_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  411. Function.partialInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  412. Function.partialInv_left

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  413. Function.partialInv_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  414. Function.pred_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  415. Function.rec_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  416. Function.rightInverse_iff_comp

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  417. Function.rightInverse_invFun

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  418. Function.rightInverse_surjInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  419. Function.sometimes

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  420. Function.sometimes_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  421. Function.sometimes_spec

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  422. Function.surjInv

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  423. Function.surjInv_eq

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  424. Function.surjective_comp_left_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  425. Function.surjective_comp_right_iff_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  426. Function.surjective_eval

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  427. Function.surjective_iff_hasRightInverse

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  428. Function.surjective_of_right_cancellable_Prop

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  429. Function.surjective_to_subsingleton

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  430. Function.swap_ge

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  431. Function.swap_gt

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  432. Function.swap_le

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  433. Function.swap_lt

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  434. Function.symm_apply_eq_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  435. Function.symmetric_apply_eq_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  436. Function.uncurry_def

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  437. Function.uncurry_flip

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  438. Function.uncurry_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  439. Function.uncurry_update_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  440. Function.update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  441. Function.update_apply

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  442. Function.update_apply_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  443. Function.update_comm

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  444. Function.update_comp_eq_of_forall_ne

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  445. Function.update_comp_eq_of_forall_ne'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  446. Function.update_comp_eq_of_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  447. Function.update_comp_eq_of_injective'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  448. Function.update_congr

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  449. Function.update_eq_const_of_subsingleton

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  450. Function.update_eq_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  451. Function.update_eq_self

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  452. Function.update_eq_self_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  453. Function.update_idem

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  454. Function.update_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  455. Function.update_ne_self_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  456. Function.update_of_ne

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  457. Function.update_self

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  458. Function.«_aux_Mathlib_Logic_Function_Basic___macroRules_Function_term↿__1»

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  459. Function.«term↿_»

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  460. GE.ge.le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  461. GT.gt.lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  462. HasCompactSupport.rpow_const

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  463. HasSSubset.SSubset.lt

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  464. HasSubset.Subset.le

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  465. Int.dvd_natCast

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  466. Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  467. Int.eq_zero_of_dvd_of_nonneg_of_lt

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  468. Int.gcd_emod

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  469. Int.instNontrivial

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  470. Int.natAbs_le_of_dvd_ne_zero

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  471. Int.natAbs_surjective

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  472. Int.natCast_dvd

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  473. Int.natCast_dvd_ofNat

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  474. Int.ofNat_dvd_natCast

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  475. Int.ofNat_injective

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  476. Int.pow_right_injective

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  477. Int.strongRec_of_ge

    Mathlib.Data.Int.BasicSOURCE_INDEXEDNOT_CHECKED

  478. InvImage.equivalence

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  479. IsClosed.and

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  480. IsClosed.iUnion_of_finite_nonempty

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  481. IsClosed.inter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  482. IsClosed.isLocallyClosed

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  483. IsClosed.not

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  484. IsClosed.sdiff

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  485. IsClosed.union

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  486. IsDomain.to_noZeroDivisors

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  487. IsOpen.and

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  488. IsOpen.iInter_of_finite_ne_univ

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  489. IsOpen.isClosed_compl

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  490. IsOpen.isLocallyClosed

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  491. IsOpen.sdiff

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  492. IsOpen.union

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  493. IsRightCancelAdd.toGrindAddRightCancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  494. IsSelfInv.neg

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  495. IsSelfNeg.inv

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  496. Evidence object · inspect its exact boundary

    L4YAML parser acceptance — pinned source check

    Evidence recordsSOURCE_CHECKWARRANTED_BOUNDED

  497. LE.ext

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  498. LE.ext_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  499. LE.le.antisymm

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  500. LE.le.antisymm'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  501. LE.le.eq_of_not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  502. LE.le.eq_of_not_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  503. LE.le.eq_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  504. LE.le.eq_or_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  505. LE.le.eq_or_lt_dec

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  506. LE.le.eq_or_lt_dec'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  507. LE.le.ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  508. LE.le.ge_iff_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  509. LE.le.ge_iff_eq'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  510. LE.le.ge_or_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  511. LE.le.ge_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  512. LE.le.gt_or_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  513. LE.le.le_or_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  514. LE.le.le_or_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  515. LE.le.lt_iff_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  516. LE.le.lt_iff_ne'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  517. LE.le.lt_of_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  518. LE.le.lt_of_ne'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  519. LE.le.lt_of_not_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  520. LE.le.lt_or_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  521. LE.le.lt_or_eq'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  522. LE.le.lt_or_eq_dec

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  523. LE.le.lt_or_eq_dec'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  524. LE.le.lt_or_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  525. LE.le.not_lt_iff_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  526. LE.le.not_lt_iff_eq'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  527. LE.le.subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  528. LE.le.trans

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  529. LE.le.trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  530. LE.le.trans_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  531. LE.le.trans_eq'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  532. LE.le.trans_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  533. LE.le.trans_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  534. LE.le.trans_strongLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  535. LT.lt.asymm

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  536. LT.lt.false

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  537. LT.lt.gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  538. LT.lt.gt_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  539. LT.lt.le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  540. LT.lt.lt_or_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  541. LT.lt.ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  542. LT.lt.ne'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  543. LT.lt.not_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  544. LT.lt.ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  545. LT.lt.trans

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  546. LT.lt.trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  547. LT.lt.trans_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  548. LT.lt.trans_eq'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  549. LT.lt.trans_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  550. LT.lt.trans_le'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  551. LinearOrder.ext

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  552. LinearOrder.ext_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  553. LinearOrder.lift

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  554. LinearOrder.lift'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  555. LinearOrder.liftWithOrd

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  556. LinearOrder.liftWithOrd'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  557. LinearOrder.ofSubsingleton

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  558. LinearOrder.toPartialOrder_injective

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  559. LinearOrder.toPartialOrder_injective_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  560. List.Aesop.toFinset_nonempty_of_ne

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  561. List.Disjoint.map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  562. List.Disjoint.map_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  563. List.Disjoint.of_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  564. List.Forall.imp

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  565. List.IsPrefix.idxOf_eq_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  566. List.IsPrefix.idxOf_le

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  567. List.IsPrefix.mem_iff_idxOf_lt_length

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  568. List.IsSuffix.idxOf_add_length_le

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  569. List.IsSuffix.idxOf_le

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  570. List.Perm.disjoint_left

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  571. List.Perm.disjoint_right

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  572. List.Sublist.antisymm

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  573. List.Sublist.of_cons_of_ne

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  574. List.append_cons_inj_of_notMem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  575. List.append_eq_has_append

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  576. List.append_left_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  577. List.append_right_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  578. List.append_subset_of_subset_of_subset

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  579. List.bind_eq_flatMap

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  580. List.choose_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  581. List.choose_property

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  582. List.choose_spec

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  583. List.comp_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  584. List.concat_eq_reverse_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  585. List.cons_head!_tail

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  586. List.cons_head?_tail

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  587. List.cons_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  588. List.cons_sublist_cons'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  589. List.cons_subset_of_subset_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  590. List.disjoint_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  591. List.disjoint_pmap

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  592. List.disjoint_reverse_left

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  593. List.disjoint_reverse_right

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  594. List.doubleton_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  595. List.dropLast_append_getLast

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  596. List.dropLast_append_getLast?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  597. List.dropLast_eq_nil_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  598. List.eq_cons_of_length_one

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  599. List.eq_cons_of_mem_head?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  600. List.eq_nil_or_concat'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  601. List.eq_of_head?_eq_of_tail_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  602. List.eq_of_mem_map_const

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  603. List.eq_of_tail_eq_of_dropLast_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  604. List.eq_replicate_length

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  605. List.erase_getElem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  606. List.exists_mem_cons_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  607. List.exists_mem_cons_of

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  608. List.exists_mem_cons_of_exists

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  609. List.exists_mem_iff_get

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  610. List.exists_mem_iff_getElem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  611. List.exists_of_length_succ

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  612. List.ext_getElem!

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  613. List.ext_getElem?'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  614. List.ext_getElem?_iff'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  615. List.ext_get_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  616. List.filterMap_congr

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  617. List.filterMap_eq_flatMap_toList

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  618. List.filterMap_eq_map_iff_forall_eq_some

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  619. List.filterMap_none

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  620. List.filter_attach

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  621. List.filter_attach'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  622. List.filter_comm

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  623. List.filter_eq_foldr

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  624. List.filter_false

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  625. List.filter_singleton

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  626. List.filter_subset'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  627. List.filter_subset_self

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  628. List.filter_toFinset

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  629. List.filter_true

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  630. List.flatMap_congr

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  631. List.flatMap_pure_eq_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  632. List.foldlM_eq_foldl

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  633. List.foldl_concat

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  634. List.foldl_ext

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  635. List.foldl_fixed

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  636. List.foldl_fixed'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  637. List.foldl_hom₂

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  638. List.foldrM_eq_foldr

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  639. List.foldr_concat

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  640. List.foldr_ext

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  641. List.foldr_fixed

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  642. List.foldr_fixed'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  643. List.foldr_hom₂

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  644. List.forall_append

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  645. List.forall_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  646. List.forall_iff_forall_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  647. List.forall_map_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  648. List.forall_mem_iff_get

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  649. List.forall_mem_iff_getElem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  650. List.forall_mem_of_forall_mem_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  651. List.getElem?_idxOf

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  652. List.getElem?_length

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  653. List.getElem?_surjective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  654. List.getElem_fin_surjective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  655. List.getElem_map_rev

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  656. List.getElem_mem_tail

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  657. List.getElem_set_of_ne

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  658. List.getLast?_append_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  659. List.getLast?_append_of_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  660. List.getLast?_eq_getLast_of_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  661. List.getLast?_flatten_replicate

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  662. List.getLastI_eq_getLast?_getD

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  663. List.getLast_append_of_right_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  664. List.getLast_append_singleton

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  665. List.getLast_concat'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  666. List.getLast_congr

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  667. List.getLast_replicate_succ

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  668. List.getLast_singleton'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  669. List.get_attach

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  670. List.get_eq_getElem?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  671. List.get_length_sub_one

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  672. List.get_reverse'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  673. List.get_surjective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  674. List.get_tail

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  675. List.head!_append

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  676. List.head!_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  677. List.head!_eq_head?_getD

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  678. List.head!_mem_head?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  679. List.head!_mem_self

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  680. List.head!_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  681. List.head?_append_of_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  682. List.head?_flatten_replicate

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  683. List.head_eq_getElem_zero

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  684. List.idxOf_append_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  685. List.idxOf_append_of_notMem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  686. List.idxOf_cons_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  687. List.idxOf_cons_ne

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  688. List.idxOf_eq_length_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  689. List.idxOf_eq_zero_iff_eq_nil_or_head_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  690. List.idxOf_eq_zero_iff_head_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  691. List.idxOf_get

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  692. List.idxOf_getLast

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  693. List.idxOf_inj

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  694. List.idxOf_of_notMem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  695. List.idxOf_tail_of_head_ne

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  696. List.infix_flatMap_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  697. List.injective_foldl_comp

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  698. List.insert_neg

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  699. List.insert_pos

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  700. List.instAssociativeAppend_mathlib

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  701. List.instDecidablePredForall

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  702. List.instInsertOfDecidableEq_mathlib

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  703. List.instIsPartialOrderSublist

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  704. List.instIsPreorderSubset

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  705. List.instLawfulIdentityAppendNil_mathlib

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  706. List.instLawfulSingleton_mathlib

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  707. List.instSingletonList

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  708. List.left_le_of_mem_range'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  709. List.length_eq_four

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  710. List.length_eq_length_filter_add

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  711. List.length_eq_succ_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  712. List.length_eq_three

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  713. List.length_eq_two

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  714. List.length_eq_two'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  715. List.length_eraseIdx_add_one

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  716. List.length_eraseP_add_one

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  717. List.length_erase_add_one

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  718. List.length_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  719. List.length_injective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  720. List.length_pos_iff_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  721. List.length_pos_of_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  722. List.lookup_graph

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  723. List.map_bijective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  724. List.map_comp_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  725. List.map_diff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  726. List.map_eq_map

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  727. List.map_erase

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  728. List.map_filter

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  729. List.map_foldl_erase

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  730. List.map_injective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  731. List.map_involutive_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  732. List.map_leftInverse_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  733. List.map_reverseAux

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  734. List.map_rightInverse_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  735. List.map_subset_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  736. List.map_surjective_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  737. List.mem_dropLast_iff_idxOf_lt

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  738. List.mem_dropLast_of_mem_of_ne_getLast

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  739. List.mem_dropLast_of_mem_of_ne_getLast?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  740. List.mem_dropLast_of_mem_of_ne_getLastD

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  741. List.mem_filter_of_mem

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  742. List.mem_getLast?_append_of_mem_getLast?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  743. List.mem_getLast?_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  744. List.mem_getLast?_eq_getLast

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  745. List.mem_head?_append_of_mem_head?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  746. List.mem_map_of_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  747. List.mem_map_of_involutive

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  748. List.mem_of_mem_filter

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  749. List.mem_pair

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  750. List.mem_pure

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  751. List.mem_take_iff_idxOf_lt

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  752. List.monotone_filter_right

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  753. List.notMem_of_subset

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  754. List.of_mem_filter

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  755. List.or_exists_of_exists_mem_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  756. List.perm_reverse

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  757. List.range'_0

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  758. List.replicate_add

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  759. List.replicate_left_inj

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  760. List.replicate_left_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  761. List.replicate_right_inj

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  762. List.replicate_right_inj'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  763. List.replicate_right_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  764. List.replicate_subset_singleton

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  765. List.reverse_bijective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  766. List.reverse_concat'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  767. List.reverse_cons'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  768. List.reverse_foldl

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  769. List.reverse_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  770. List.reverse_involutive

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  771. List.reverse_perm'

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  772. List.reverse_surjective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  773. List.setOfPred_mem_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  774. List.set_of_mem_cons

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  775. List.singleton_eq

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  776. List.singleton_injective

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  777. List.sublist_cons_of_sublist

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  778. List.sublist_singleton

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  779. List.subset_singleton_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  780. List.succ_idxOf_lt_length_of_mem_dropLast

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  781. List.surjective_head!

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  782. List.surjective_head?

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  783. List.surjective_tail

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  784. List.tail_append_singleton_of_ne_nil

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  785. List.tail_eq_nil_iff

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  786. List.toFinset_filter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  787. List.toFinset_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  788. List.toFinset_union

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  789. List.uniqueOfIsEmpty

    Mathlib.Data.List.BasicSOURCE_INDEXEDNOT_CHECKED

  790. Source indexed · proof checking not performed

    Mathlib.Algebra.Group.Basic

    Mathlib.Algebra.Group.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  791. Source indexed · proof checking not performed

    Mathlib.Algebra.Ring.Basic

    Mathlib.Algebra.Ring.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  792. Source indexed · proof checking not performed

    Mathlib.Analysis.SpecialFunctions.Pow.Real

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  793. Source indexed · proof checking not performed

    Mathlib.Combinatorics.SimpleGraph.Basic

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  794. Source indexed · proof checking not performed

    Mathlib.Data.Finset.Basic

    Mathlib.Data.Finset.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  795. Source indexed · proof checking not performed

    Mathlib.Data.Int.Basic

    Mathlib.Data.Int.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  796. Source indexed · proof checking not performed

    Mathlib.Data.List.Basic

    Mathlib.Data.List.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  797. Source indexed · proof checking not performed

    Mathlib.Data.Nat.Basic

    Mathlib.Data.Nat.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  798. Source indexed · proof checking not performed

    Mathlib.Data.Nat.Prime.Basic

    Mathlib.Data.Nat.Prime.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  799. Source indexed · proof checking not performed

    Mathlib.Data.Set.Basic

    Mathlib.Data.Set.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  800. Source indexed · proof checking not performed

    Mathlib.Logic.Function.Basic

    Mathlib.Logic.Function.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  801. Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  802. Mathlib.Meta.NormNum.IsNNRat.rpow_isNNRat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  803. Mathlib.Meta.NormNum.IsNat.rpow_eq_pow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  804. Mathlib.Meta.NormNum.IsNat.rpow_isNNRat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  805. Mathlib.Meta.NormNum.evalRPow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  806. Mathlib.Meta.NormNum.proveIsNatRPowIsNNRat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  807. Mathlib.Meta.NormNum.rpow_isRat_eq_inv_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  808. Mathlib.Meta.Positivity.evalRpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  809. Mathlib.Meta.Positivity.evalRpowZero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  810. Source indexed · proof checking not performed

    Mathlib.Order.Basic

    Mathlib.Order.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  811. Mathlib.Tactic.GCongr.exactLeOfLt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  812. Source indexed · proof checking not performed

    Mathlib.Topology.Basic

    Mathlib.Topology.BasicSOURCE_MODULESOURCE_INDEXEDNOT_CHECKED

  813. MulOpposite.instHasDistribNeg

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  814. Multiset.Aesop.toFinset_nonempty_of_ne

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  815. Multiset.toFinset_add

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  816. Multiset.toFinset_eq_empty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  817. Multiset.toFinset_filter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  818. Multiset.toFinset_inter

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  819. Multiset.toFinset_nonempty

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  820. Multiset.toFinset_replicate

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  821. Multiset.toFinset_union

    Mathlib.Data.Finset.BasicSOURCE_INDEXEDNOT_CHECKED

  822. Nat.Coprime.odd_of_left

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  823. Nat.Coprime.odd_of_right

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  824. Nat.Prime.coprime_pow_of_not_dvd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  825. Nat.Prime.dvd_iff_eq

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  826. Nat.Prime.dvd_iff_not_coprime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  827. Nat.Prime.dvd_mul_of_dvd_ne

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  828. Nat.Prime.dvd_of_dvd_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  829. Nat.Prime.eq_one_of_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  830. Nat.Prime.eq_two_or_odd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  831. Nat.Prime.eq_two_or_odd'

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  832. Nat.Prime.even_iff

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  833. Nat.Prime.even_sub_one

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  834. Nat.Prime.five_le_of_ne_two_of_ne_three

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  835. Nat.Prime.mod_two_eq_one_iff_ne_two

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  836. Nat.Prime.mul_eq_prime_sq_iff

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  837. Nat.Prime.not_coprime_iff_dvd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  838. Nat.Prime.not_dvd_mul

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  839. Nat.Prime.not_prime_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  840. Nat.Prime.not_prime_pow'

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  841. Nat.Prime.odd_iff

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  842. Nat.Prime.odd_of_ne_two

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  843. Nat.Prime.pow_eq_iff

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  844. Nat.Prime.pred_pos

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  845. Nat.coprime_of_dvd'

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  846. Nat.coprime_of_lt_minFac

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  847. Nat.coprime_of_lt_prime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  848. Nat.coprime_or_dvd_of_prime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  849. Nat.coprime_pow_primes

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  850. Nat.coprime_primes

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  851. Nat.coprime_two_left

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  852. Nat.coprime_two_right

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  853. Nat.div_right_comm

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  854. Nat.dvd_antisymm_iff

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  855. Nat.dvd_left_injective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  856. Nat.dvd_of_forall_prime_mul_dvd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  857. Nat.dvd_prime_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  858. Nat.dvd_sub_self_left

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  859. Nat.dvd_sub_self_right

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  860. Nat.eq_one_iff_not_exists_prime_dvd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  861. Nat.eq_or_coprime_of_le_prime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  862. Nat.eq_prime_pow_of_dvd_least_prime_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  863. Nat.exists_dvd_of_not_prime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  864. Nat.exists_dvd_of_not_prime2

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  865. Nat.forall_prime_iff_two_and_odd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  866. Nat.forall_prime_of_two_of_odd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  867. Nat.gcd_eq_one_of_lt_minFac

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  868. Nat.instLinearOrder

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  869. Nat.instNontrivial

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  870. Nat.instPartialOrder

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  871. Nat.instPreorder

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  872. Nat.leRecOn_injective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  873. Nat.leRecOn_surjective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  874. Nat.mul_le_pow

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  875. Nat.ne_one_iff_exists_prime_dvd

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  876. Nat.not_prime_iff_exists_dvd_lt

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  877. Nat.not_prime_iff_exists_dvd_ne

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  878. Nat.not_prime_iff_exists_mul_eq

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  879. Nat.not_prime_mul

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  880. Nat.not_prime_of_dvd_of_lt

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  881. Nat.not_prime_of_dvd_of_ne

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  882. Nat.not_prime_of_mul_eq

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  883. Nat.pow_left_injective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  884. Nat.pow_right_injective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  885. Nat.pow_sub_one

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  886. Nat.prime_eq_prime_of_dvd_pow

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  887. Nat.prime_mul_iff

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  888. Nat.set_induction

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  889. Nat.set_induction_bounded

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  890. Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  891. Nat.succ_injective

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  892. Nat.succ_pred_prime

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  893. Nat.two_mul_sq_add_one_le_two_pow_two_mul

    Mathlib.Data.Nat.BasicSOURCE_INDEXEDNOT_CHECKED

  894. Ne.ge_iff_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  895. Ne.gt_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  896. Ne.instIsEquiv_compl

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  897. Ne.le_iff_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  898. Ne.lt_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  899. Ne.lt_of_le'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  900. Ne.lt_or_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  901. Ne.not_ge_or_not_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  902. Ne.not_le_or_not_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  903. NoZeroDivisors.to_isCancelMulZero

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  904. NoZeroDivisors.to_isDomain

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  905. Odd.coprime_two_left

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  906. Odd.coprime_two_right

    Mathlib.Data.Nat.Prime.BasicSOURCE_INDEXEDNOT_CHECKED

  907. Option.rec_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  908. Order.Preimage

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  909. Order.Preimage.decidable

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  910. PUnit.instDenselyOrdered

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  911. PUnit.instLinearOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  912. PUnit.le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  913. PUnit.max_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  914. PUnit.min_eq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  915. PUnit.not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  916. PartialOrder.ext

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  917. PartialOrder.ext_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  918. PartialOrder.lift

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  919. PartialOrder.toPreorder_injective

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  920. PartialOrder.toPreorder_injective_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  921. Pi.compl_apply

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  922. Pi.compl_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  923. Pi.himp_apply

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  924. Pi.himp_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  925. Pi.hnot_apply

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  926. Pi.hnot_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  927. Pi.instCompl

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  928. Pi.instHImp

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  929. Pi.instHNot

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  930. Pi.instSDiff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  931. Pi.lt_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  932. Pi.map_comp_map

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  933. Pi.map_id

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  934. Pi.map_id'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  935. Pi.map_injective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  936. Pi.map_update

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  937. Pi.partialOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  938. Pi.preorder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  939. Pi.sdiff_apply

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  940. Pi.sdiff_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  941. Preorder.ext

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  942. Preorder.lift

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  943. Preorder.toLE_injective

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  944. Preorder.toLE_injective_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  945. Prod.GCongr.mk_le_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  946. Prod.instDecidableLE

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  947. Prod.instLE_mathlib

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  948. Prod.instPartialOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  949. Prod.instPreorder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  950. Prod.le_def

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  951. Prod.lt_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  952. Prod.lt_of_le_of_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  953. Prod.lt_of_lt_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  954. Prod.mk_le_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  955. Prod.mk_le_mk_iff_left

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  956. Prod.mk_le_mk_iff_right

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  957. Prod.mk_le_swap

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  958. Prod.mk_lt_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  959. Prod.mk_lt_mk_iff_left

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  960. Prod.mk_lt_mk_iff_right

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  961. Prod.mk_lt_mk_of_le_of_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  962. Prod.mk_lt_mk_of_lt_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  963. Prod.mk_lt_swap

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  964. Prod.swap_le_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  965. Prod.swap_le_swap

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  966. Prod.swap_lt_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  967. Prod.swap_lt_swap

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  968. Prop.instCompl

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  969. Prop.partialOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  970. Real.abs_log_mul_self_rpow_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  971. Real.abs_rpow_le_abs_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  972. Real.abs_rpow_le_exp_log_mul

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  973. Real.abs_rpow_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  974. Real.antitoneOn_rpow_Ioi_of_exponent_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  975. Real.antitone_rpow_of_base_le_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  976. Real.div_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  977. Real.eq_rpow_inv

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  978. Real.eq_zero_rpow_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  979. Real.exp_mul

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  980. Real.exp_one_pow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  981. Real.exp_one_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  982. Real.instPow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  983. Real.inv_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  984. Real.le_log_of_pow_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  985. Real.le_log_of_rpow_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  986. Real.le_log_of_zpow_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  987. Real.le_pow_iff_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  988. Real.le_pow_of_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  989. Real.le_rpow_add

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  990. Real.le_rpow_iff_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  991. Real.le_rpow_inv_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  992. Real.le_rpow_inv_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  993. Real.le_rpow_of_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  994. Real.le_zpow_iff_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  995. Real.le_zpow_of_log_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  996. Real.log_le_rpow_div

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  997. Real.log_natCast_le_rpow_div

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  998. Real.log_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  999. Real.lt_log_of_pow_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1000. Real.lt_log_of_rpow_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1001. Real.lt_log_of_zpow_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1002. Real.lt_pow_iff_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1003. Real.lt_pow_of_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1004. Real.lt_rpow_iff_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1005. Real.lt_rpow_inv_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1006. Real.lt_rpow_inv_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1007. Real.lt_rpow_of_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1008. Real.lt_zpow_iff_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1009. Real.lt_zpow_of_log_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1010. Real.monotoneOn_rpow_Ici_of_exponent_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1011. Real.monotone_rpow_of_base_ge_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1012. Real.mul_log_eq_log_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1013. Real.mul_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1014. Real.norm_rpow_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1015. Real.one_le_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1016. Real.one_le_rpow_of_pos_of_le_one_of_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1017. Real.one_lt_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1018. Real.one_lt_rpow_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1019. Real.one_lt_rpow_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1020. Real.one_lt_rpow_of_pos_of_lt_one_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1021. Real.one_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1022. Real.pi_rpow_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1023. Real.pi_rpow_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1024. Real.pow_le_iff_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1025. Real.pow_le_of_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1026. Real.pow_lt_iff_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1027. Real.pow_lt_of_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1028. Real.pow_rpow_inv_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1029. Real.rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1030. Real.rpow_add

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1031. Real.rpow_add'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1032. Real.rpow_add_intCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1033. Real.rpow_add_intCast'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1034. Real.rpow_add_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1035. Real.rpow_add_natCast'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1036. Real.rpow_add_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1037. Real.rpow_add_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1038. Real.rpow_add_one'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1039. Real.rpow_def

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1040. Real.rpow_def_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1041. Real.rpow_def_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1042. Real.rpow_def_of_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1043. Real.rpow_def_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1044. Real.rpow_div_two_eq_sqrt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1045. Real.rpow_eq_pow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1046. Real.rpow_eq_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1047. Real.rpow_eq_zero_iff_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1048. Real.rpow_intCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1049. Real.rpow_intCast_mul

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1050. Real.rpow_inv_eq

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1051. Real.rpow_inv_le_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1052. Real.rpow_inv_le_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1053. Real.rpow_inv_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1054. Real.rpow_inv_log_le_exp_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1055. Real.rpow_inv_lt_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1056. Real.rpow_inv_lt_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1057. Real.rpow_inv_natCast_pow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1058. Real.rpow_inv_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1059. Real.rpow_le_iff_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1060. Real.rpow_le_of_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1061. Real.rpow_le_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1062. Real.rpow_le_one_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1063. Real.rpow_le_one_of_one_le_of_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1064. Real.rpow_le_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1065. Real.rpow_le_rpow_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1066. Real.rpow_le_rpow_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1067. Real.rpow_le_rpow_left_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1068. Real.rpow_le_rpow_left_iff_of_base_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1069. Real.rpow_le_rpow_of_exponent_ge

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1070. Real.rpow_le_rpow_of_exponent_ge'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1071. Real.rpow_le_rpow_of_exponent_ge_of_imp

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1072. Real.rpow_le_rpow_of_exponent_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1073. Real.rpow_le_rpow_of_exponent_le_or_ge

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1074. Real.rpow_le_rpow_of_nonpos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1075. Real.rpow_le_self_of_le_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1076. Real.rpow_le_self_of_one_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1077. Real.rpow_left_inj

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1078. Real.rpow_left_injOn

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1079. Real.rpow_lt_iff_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1080. Real.rpow_lt_of_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1081. Real.rpow_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1082. Real.rpow_lt_one_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1083. Real.rpow_lt_one_iff'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1084. Real.rpow_lt_one_iff_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1085. Real.rpow_lt_one_of_one_lt_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1086. Real.rpow_lt_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1087. Real.rpow_lt_rpow_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1088. Real.rpow_lt_rpow_iff_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1089. Real.rpow_lt_rpow_left_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1090. Real.rpow_lt_rpow_left_iff_of_base_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1091. Real.rpow_lt_rpow_of_exponent_gt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1092. Real.rpow_lt_rpow_of_exponent_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1093. Real.rpow_lt_rpow_of_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1094. Real.rpow_lt_self_of_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1095. Real.rpow_lt_self_of_one_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1096. Real.rpow_max

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1097. Real.rpow_mul

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1098. Real.rpow_mul_intCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1099. Real.rpow_mul_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1100. Real.rpow_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1101. Real.rpow_natCast_mul

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1102. Real.rpow_ne_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1103. Real.rpow_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1104. Real.rpow_neg_eq_inv_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1105. Real.rpow_neg_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1106. Real.rpow_neg_ofNat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1107. Real.rpow_neg_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1108. Real.rpow_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1109. Real.rpow_ofNat

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1110. Real.rpow_of_add_eq

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1111. Real.rpow_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1112. Real.rpow_one_add'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1113. Real.rpow_one_sub'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1114. Real.rpow_pos_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1115. Real.rpow_pow_comm

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1116. Real.rpow_right_inj

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1117. Real.rpow_rpow_inv

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1118. Real.rpow_sub

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1119. Real.rpow_sub'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1120. Real.rpow_sub_intCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1121. Real.rpow_sub_intCast'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1122. Real.rpow_sub_natCast

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1123. Real.rpow_sub_natCast'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1124. Real.rpow_sub_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1125. Real.rpow_sub_one'

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1126. Real.rpow_sum_of_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1127. Real.rpow_sum_of_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1128. Real.rpow_two

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1129. Real.rpow_zero

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1130. Real.rpow_zero_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1131. Real.rpow_zpow_comm

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1132. Real.self_le_rpow_of_le_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1133. Real.self_le_rpow_of_one_le

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1134. Real.self_lt_rpow_of_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1135. Real.self_lt_rpow_of_one_lt

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1136. Real.sqrt_eq_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1137. Real.strictAntiOn_rpow_Ioi_of_exponent_neg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1138. Real.strictAnti_rpow_of_base_lt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1139. Real.strictMonoOn_rpow_Ici_of_exponent_pos

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1140. Real.strictMono_rpow_of_base_gt_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1141. Real.zero_rpow

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1142. Real.zero_rpow_eq_iff

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1143. Real.zero_rpow_le_one

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1144. Real.zero_rpow_nonneg

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1145. Real.zpow_le_iff_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1146. Real.zpow_le_of_le_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1147. Real.zpow_lt_iff_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1148. Real.zpow_lt_of_lt_log

    Mathlib.Analysis.SpecialFunctions.Pow.RealSOURCE_INDEXEDNOT_CHECKED

  1149. Semigroup.to_isAssociative

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1150. Semigroup.to_isLawfulIdentity

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1151. Set.Finite.isClosed_biUnion

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1152. Set.Finite.isClosed_sUnion

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1153. Set.Finite.isOpen_biInter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1154. Set.Finite.isOpen_sInter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1155. Set.MemUnion.elim

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1156. Set.Nonempty.coe_sort

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1157. Set.Nonempty.compl_ssubset_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1158. Set.Nonempty.empty_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1159. Set.Nonempty.eq_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1160. Set.Nonempty.exists_const

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1161. Set.Nonempty.forall_const

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1162. Set.Nonempty.inl

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1163. Set.Nonempty.inr

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1164. Set.Nonempty.left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1165. Set.Nonempty.mono

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1166. Set.Nonempty.ne_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1167. Set.Nonempty.not_subset_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1168. Set.Nonempty.of_diff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1169. Set.Nonempty.of_sdiff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1170. Set.Nonempty.of_subtype

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1171. Set.Nonempty.right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1172. Set.Nonempty.some

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1173. Set.Nonempty.some_mem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1174. Set.Nonempty.ssubset_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1175. Set.Nonempty.to_subtype

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1176. Set.Nonempty.to_type

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1177. Set.PiSetCoe.canLift

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1178. Set.PiSetCoe.canLift'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1179. Set.SeparatesPoints

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1180. Set.Subset.antisymm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1181. Set.Subset.antisymm_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1182. Set.Subset.refl

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1183. Set.Subset.rfl

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1184. Set.Subset.trans

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1185. Set.bot_eq_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1186. Set.coe_eq_subtype

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1187. Set.coe_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1188. Set.coe_setOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1189. Set.compl_ssubset_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1190. Set.decidableCompl

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1191. Set.decidableEmptyset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1192. Set.decidableEq

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1193. Set.decidableInsert

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1194. Set.decidableInter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1195. Set.decidableSdiff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1196. Set.decidableSetOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1197. Set.decidableUnion

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1198. Set.decidableUniv

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1199. Set.empty_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1200. Set.empty_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1201. Set.empty_ne_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1202. Set.empty_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1203. Set.empty_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1204. Set.empty_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1205. Set.eq_empty_iff_forall_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1206. Set.eq_empty_of_forall_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1207. Set.eq_empty_of_isEmpty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1208. Set.eq_empty_of_subset_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1209. Set.eq_empty_or_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1210. Set.eq_of_forall_subset_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1211. Set.eq_of_subset_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1212. Set.eq_or_ssubset_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1213. Set.eq_univ_iff_forall

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1214. Set.eq_univ_of_forall

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1215. Set.eq_univ_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1216. Set.eq_univ_of_univ_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1217. Set.exists_mem_const

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1218. Set.exists_mem_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1219. Set.exists_mem_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1220. Set.exists_mem_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1221. Set.exists_mem_of_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1222. Set.exists_mem_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1223. Set.exists_mem_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1224. Set.exists_mem_univ_of_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1225. Set.exists_of_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1226. Set.forall_mem_const

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1227. Set.forall_mem_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1228. Set.forall_mem_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1229. Set.forall_mem_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1230. Set.forall_mem_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1231. Set.forall_mem_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1232. Set.inf_eq_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1233. Set.instBoundedOrder

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1234. Set.instDistribLattice

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1235. Set.instInhabited

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1236. Set.instIsEmptyElemEmptyCollection

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1237. Set.instNonemptyTop

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1238. Set.inter_assoc

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1239. Set.inter_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1240. Set.inter_congr_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1241. Set.inter_congr_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1242. Set.inter_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1243. Set.inter_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1244. Set.inter_eq_inter_iff_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1245. Set.inter_eq_inter_iff_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1246. Set.inter_eq_inter_mono_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1247. Set.inter_eq_inter_mono_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1248. Set.inter_eq_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1249. Set.inter_eq_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1250. Set.inter_eq_self_of_subset_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1251. Set.inter_eq_self_of_subset_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1252. Set.inter_inter_distrib_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1253. Set.inter_inter_distrib_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1254. Set.inter_inter_inter_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1255. Set.inter_isAssoc

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1256. Set.inter_isComm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1257. Set.inter_left_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1258. Set.inter_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1259. Set.inter_nonempty_iff_exists_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1260. Set.inter_nonempty_iff_exists_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1261. Set.inter_ofPred_eq_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1262. Set.inter_right_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1263. Set.inter_self

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1264. Set.inter_setOf_eq_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1265. Set.inter_ssubset_left_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1266. Set.inter_ssubset_right_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1267. Set.inter_subset_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1268. Set.inter_subset_inter_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1269. Set.inter_subset_inter_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1270. Set.inter_subset_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1271. Set.inter_subset_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1272. Set.inter_union_distrib_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1273. Set.inter_union_distrib_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1274. Set.inter_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1275. Set.isEmpty_coe_sort

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1276. Set.le_eq_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1277. Set.le_iff_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1278. Set.left_eq_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1279. Set.lt_eq_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1280. Set.lt_iff_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1281. Set.mem_bijective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1282. Set.mem_dite_empty_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1283. Set.mem_dite_empty_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1284. Set.mem_dite_univ_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1285. Set.mem_dite_univ_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1286. Set.mem_empty_iff_false

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1287. Set.mem_injective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1288. Set.mem_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1289. Set.mem_inter_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1290. Set.mem_ite_empty_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1291. Set.mem_ite_empty_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1292. Set.mem_ite_univ_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1293. Set.mem_ite_univ_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1294. Set.mem_of_eq_of_mem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1295. Set.mem_of_mem_inter_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1296. Set.mem_of_mem_inter_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1297. Set.mem_of_mem_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1298. Set.mem_of_subset_of_mem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1299. Set.mem_or_mem_of_mem_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1300. Set.mem_powerset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1301. Set.mem_powerset_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1302. Set.mem_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1303. Set.mem_sep_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1304. Set.mem_surjective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1305. Set.mem_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1306. Set.mem_union_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1307. Set.mem_union_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1308. Set.monotone_powerset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1309. Set.ne_univ_iff_exists_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1310. Set.nonempty_coe_sort

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1311. Set.nonempty_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1312. Set.nonempty_iff_empty_ne

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1313. Set.nonempty_iff_ne_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1314. Set.nonempty_iff_ne_empty'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1315. Set.nonempty_iff_univ_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1316. Set.nonempty_of_mem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1317. Set.nonempty_of_not_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1318. Set.nonempty_of_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1319. Set.nonempty_of_ssubset'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1320. Set.nontrivial_of_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1321. Set.notMem_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1322. Set.notMem_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1323. Set.not_nonempty_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1324. Set.not_nonempty_iff_eq_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1325. Set.not_nonempty_iff_eq_empty'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1326. Set.not_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1327. Set.not_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1328. Set.not_subset_iff_exists_mem_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1329. Set.not_top_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1330. Set.not_univ_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1331. Set.ofPred_and

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1332. Set.ofPred_bijective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1333. Set.ofPred_bot

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1334. Set.ofPred_false

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1335. Set.ofPred_inj

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1336. Set.ofPred_injective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1337. Set.ofPred_inter_eq_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1338. Set.ofPred_or

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1339. Set.ofPred_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1340. Set.ofPred_subset_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1341. Set.ofPred_subset_ofPred_of_imp

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1342. Set.ofPred_top

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1343. Set.ofPred_true

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1344. Set.piecewise

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1345. Set.powerset_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1346. Set.powerset_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1347. Set.powerset_mono

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1348. Set.powerset_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1349. Set.powerset_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1350. Set.right_eq_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1351. Set.sep_and

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1352. Set.sep_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1353. Set.sep_eq_empty_iff_mem_false

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1354. Set.sep_eq_inter_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1355. Set.sep_eq_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1356. Set.sep_eq_self_iff_mem_true

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1357. Set.sep_ext_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1358. Set.sep_false

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1359. Set.sep_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1360. Set.sep_mem_eq

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1361. Set.sep_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1362. Set.sep_or

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1363. Set.sep_setOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1364. Set.sep_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1365. Set.sep_subset_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1366. Set.sep_subset_setOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1367. Set.sep_true

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1368. Set.sep_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1369. Set.sep_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1370. Set.separatesPoints_mono

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1371. Set.setOf_and

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1372. Set.setOf_bijective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1373. Set.setOf_bot

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1374. Set.setOf_false

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1375. Set.setOf_inj

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1376. Set.setOf_injective

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1377. Set.setOf_inter_eq_sep

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1378. Set.setOf_or

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1379. Set.setOf_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1380. Set.setOf_subset_setOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1381. Set.setOf_subset_setOf_of_imp

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1382. Set.setOf_top

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1383. Set.setOf_true

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1384. Set.ssubset_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1385. Set.ssubset_iff_exists

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1386. Set.ssubset_iff_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1387. Set.ssubset_iff_subset_ne

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1388. Set.ssubset_of_ssubset_of_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1389. Set.ssubset_of_subset_of_ssubset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1390. Set.ssubset_union_left_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1391. Set.ssubset_union_right_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1392. Set.ssubset_univ_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1393. Set.ssubset_univ_iff_nonempty_compl

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1394. Set.subset_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1395. Set.subset_empty_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1396. Set.subset_eq_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1397. Set.subset_iff_notMem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1398. Set.subset_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1399. Set.subset_inter_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1400. Set.subset_ofPred

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1401. Set.subset_of_mem_powerset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1402. Set.subset_setOf

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1403. Set.subset_union_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1404. Set.subset_union_of_subset_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1405. Set.subset_union_of_subset_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1406. Set.subset_union_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1407. Set.subset_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1408. Set.sup_eq_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1409. Set.top_eq_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1410. Set.union_assoc

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1411. Set.union_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1412. Set.union_congr_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1413. Set.union_congr_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1414. Set.union_def

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1415. Set.union_empty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1416. Set.union_empty_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1417. Set.union_eq_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1418. Set.union_eq_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1419. Set.union_eq_self_of_subset_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1420. Set.union_eq_self_of_subset_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1421. Set.union_eq_union_iff_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1422. Set.union_eq_union_iff_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1423. Set.union_eq_union_mono_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1424. Set.union_eq_union_mono_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1425. Set.union_inter_cancel_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1426. Set.union_inter_cancel_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1427. Set.union_inter_distrib_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1428. Set.union_inter_distrib_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1429. Set.union_isAssoc

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1430. Set.union_isComm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1431. Set.union_left_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1432. Set.union_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1433. Set.union_right_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1434. Set.union_self

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1435. Set.union_subset

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1436. Set.union_subset_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1437. Set.union_subset_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1438. Set.union_subset_union_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1439. Set.union_subset_union_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1440. Set.union_union_distrib_left

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1441. Set.union_union_distrib_right

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1442. Set.union_union_union_comm

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1443. Set.union_univ

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1444. Set.uniqueEmpty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1445. Set.univ.nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1446. Set.univ_eq_empty_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1447. Set.univ_inter

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1448. Set.univ_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1449. Set.univ_subset_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1450. Set.univ_union

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1451. Set.univ_unique

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1452. SetCoe.exists

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1453. SetCoe.exists'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1454. SetCoe.ext

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1455. SetCoe.ext_iff

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1456. SetCoe.forall

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1457. SetCoe.forall'

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1458. SimpleGraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1459. SimpleGraph.Adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1460. SimpleGraph.Adj.left_mem_support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1461. SimpleGraph.Adj.mem_support_left

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1462. SimpleGraph.Adj.mem_support_right

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1463. SimpleGraph.Adj.ne

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1464. SimpleGraph.Adj.ne'

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1465. SimpleGraph.Adj.nontrivial

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1466. SimpleGraph.Adj.not_isIsolated_left

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1467. SimpleGraph.Adj.not_isIsolated_right

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1468. SimpleGraph.Adj.right_mem_support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1469. SimpleGraph.Adj.symm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1470. SimpleGraph.Bot.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1471. SimpleGraph.Compl.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1472. SimpleGraph.Inf.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1473. SimpleGraph.IsCompleteBetween

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1474. SimpleGraph.IsCompleteBetween.completeBipartiteGraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1475. SimpleGraph.IsCompleteBetween.disjoint

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1476. SimpleGraph.IsCompleteBetween.symm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1477. SimpleGraph.IsIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1478. SimpleGraph.IsIsolated.bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1479. SimpleGraph.IsIsolated.neighborSet_eq_empty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1480. SimpleGraph.IsIsolated.not_isUniversal

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1481. SimpleGraph.IsIsolated.of_isUniversal_compl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1482. SimpleGraph.IsIsolated.of_neighborSet_eq_empty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1483. SimpleGraph.IsIsolated.of_subsingleton

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1484. SimpleGraph.IsSubgraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1485. SimpleGraph.IsUniversal

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1486. SimpleGraph.IsUniversal.neighborSet_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1487. SimpleGraph.IsUniversal.not_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1488. SimpleGraph.IsUniversal.of_isIsolated_compl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1489. SimpleGraph.IsUniversal.of_neighborSet_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1490. SimpleGraph.IsUniversal.of_subsingleton

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1491. SimpleGraph.IsUniversal.top

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1492. SimpleGraph.Sdiff.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1493. SimpleGraph.Sup.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1494. SimpleGraph.Top.adjDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1495. SimpleGraph.adj_comm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1496. SimpleGraph.adj_congr_of_sym2

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1497. SimpleGraph.adj_iff_exists_edge

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1498. SimpleGraph.adj_iff_exists_edge_coe

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1499. SimpleGraph.adj_incidenceSet_inter

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1500. SimpleGraph.adj_inj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1501. SimpleGraph.adj_injective

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1502. SimpleGraph.adj_of_mem_incidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1503. SimpleGraph.adj_symm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1504. SimpleGraph.bot_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1505. SimpleGraph.card_neighborSet_union_compl_neighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1506. SimpleGraph.commonNeighbors

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1507. SimpleGraph.commonNeighbors_bot_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1508. SimpleGraph.commonNeighbors_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1509. SimpleGraph.commonNeighbors_subset_neighborSet_left

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1510. SimpleGraph.commonNeighbors_subset_neighborSet_right

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1511. SimpleGraph.commonNeighbors_symm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1512. SimpleGraph.commonNeighbors_top_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1513. SimpleGraph.compl_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1514. SimpleGraph.compl_neighborSet_disjoint

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1515. SimpleGraph.completeAtomicBooleanAlgebra

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1516. SimpleGraph.completeGraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1517. SimpleGraph.completeGraph_eq_top

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1518. SimpleGraph.decidableMemCommonNeighbors

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1519. SimpleGraph.decidableMemEdgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1520. SimpleGraph.decidableMemIncidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1521. SimpleGraph.default_def

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1522. SimpleGraph.disjoint_commonNeighbors

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1523. SimpleGraph.disjoint_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1524. SimpleGraph.disjoint_fromEdgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1525. SimpleGraph.disjoint_incidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1526. SimpleGraph.disjoint_left

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1527. SimpleGraph.disjoint_neighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1528. SimpleGraph.disjoint_of_disjoint_support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1529. SimpleGraph.distribLattice

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1530. SimpleGraph.edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1531. SimpleGraph.edgeSetEmbedding

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1532. SimpleGraph.edgeSet_bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1533. SimpleGraph.edgeSet_eq_empty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1534. SimpleGraph.edgeSet_eq_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1535. SimpleGraph.edgeSet_fromEdgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1536. SimpleGraph.edgeSet_iInf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1537. SimpleGraph.edgeSet_iSup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1538. SimpleGraph.edgeSet_inf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1539. SimpleGraph.edgeSet_inj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1540. SimpleGraph.edgeSet_injective

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1541. SimpleGraph.edgeSet_mono

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1542. SimpleGraph.edgeSet_nonempty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1543. SimpleGraph.edgeSet_sInf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1544. SimpleGraph.edgeSet_sSup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1545. SimpleGraph.edgeSet_sdiff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1546. SimpleGraph.edgeSet_sdiff_sdiff_isDiag

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1547. SimpleGraph.edgeSet_ssubset_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1548. SimpleGraph.edgeSet_strict_mono

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1549. SimpleGraph.edgeSet_subset_compl_diagSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1550. SimpleGraph.edgeSet_subset_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1551. SimpleGraph.edgeSet_subset_sym2_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1552. SimpleGraph.edgeSet_sup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1553. SimpleGraph.edgeSet_top

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1554. SimpleGraph.edge_mem_incidenceSet_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1555. SimpleGraph.edge_other_incident_set

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1556. SimpleGraph.edge_other_ne

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1557. SimpleGraph.emptyGraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1558. SimpleGraph.emptyGraph_eq_bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1559. SimpleGraph.eq_bot_iff_forall_not_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1560. SimpleGraph.eq_bot_iff_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1561. SimpleGraph.eq_top_iff_forall_isUniversal

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1562. SimpleGraph.eq_top_iff_forall_ne_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1563. SimpleGraph.exists_adj_iff_not_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1564. SimpleGraph.ext

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1565. SimpleGraph.ext_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1566. SimpleGraph.fintypeEdgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1567. SimpleGraph.fintypeEdgeSetBot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1568. SimpleGraph.fintypeEdgeSetInf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1569. SimpleGraph.fintypeEdgeSetSdiff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1570. SimpleGraph.fintypeEdgeSetSup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1571. SimpleGraph.fromEdgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1572. SimpleGraph.fromEdgeSet_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1573. SimpleGraph.fromEdgeSet_disjoint

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1574. SimpleGraph.fromEdgeSet_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1575. SimpleGraph.fromEdgeSet_empty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1576. SimpleGraph.fromEdgeSet_iInter

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1577. SimpleGraph.fromEdgeSet_iUnion

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1578. SimpleGraph.fromEdgeSet_inter

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1579. SimpleGraph.fromEdgeSet_le

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1580. SimpleGraph.fromEdgeSet_mono

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1581. SimpleGraph.fromEdgeSet_not_isDiag

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1582. SimpleGraph.fromEdgeSet_sInter

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1583. SimpleGraph.fromEdgeSet_sUnion

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1584. SimpleGraph.fromEdgeSet_sdiff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1585. SimpleGraph.fromEdgeSet_union

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1586. SimpleGraph.fromEdgeSet_univ

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1587. SimpleGraph.fromRel

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1588. SimpleGraph.fromRel_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1589. SimpleGraph.iInf_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1590. SimpleGraph.iInf_adj_of_nonempty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1591. SimpleGraph.iSup_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1592. SimpleGraph.iUnion_incidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1593. SimpleGraph.incidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1594. SimpleGraph.incidenceSetEquivNeighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1595. SimpleGraph.incidenceSetEquivNeighborSet_apply_coe

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1596. SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1597. SimpleGraph.incidenceSet_inter_incidenceSet_of_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1598. SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1599. SimpleGraph.incidenceSet_inter_incidenceSet_subset

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1600. SimpleGraph.incidenceSet_subset

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1601. SimpleGraph.incidence_other_neighbor_edge

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1602. SimpleGraph.incidence_other_prop

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1603. SimpleGraph.infSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1604. SimpleGraph.inf_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1605. SimpleGraph.insert_neighborSet_eq_univ

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1606. SimpleGraph.instCompl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1607. SimpleGraph.instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1608. SimpleGraph.instFinite

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1609. SimpleGraph.instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1610. SimpleGraph.instInfinite

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1611. SimpleGraph.instInhabited

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1612. SimpleGraph.instLE

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1613. SimpleGraph.instMax

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1614. SimpleGraph.instMin

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1615. SimpleGraph.instNontrivial

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1616. SimpleGraph.instPartialOrder

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1617. SimpleGraph.irrefl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1618. SimpleGraph.isCompleteBetween_comm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1619. SimpleGraph.isIsolated_bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1620. SimpleGraph.isIsolated_compl_iff_isUniversal

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1621. SimpleGraph.isIsolated_iff_forall_edgeSet_notMem

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1622. SimpleGraph.isUniversal_compl_iff_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1623. SimpleGraph.le_fromEdgeSet_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1624. SimpleGraph.le_iff_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1625. SimpleGraph.loopless

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1626. SimpleGraph.mem_commonNeighbors

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1627. SimpleGraph.mem_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1628. SimpleGraph.mem_incidenceSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1629. SimpleGraph.mem_incidence_iff_neighbor

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1630. SimpleGraph.mem_neighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1631. SimpleGraph.mem_support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1632. SimpleGraph.mem_support_iff_not_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1633. SimpleGraph.mk

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1634. SimpleGraph.mk'

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1635. SimpleGraph.mk'_apply_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1636. SimpleGraph.mk'_mem_incidenceSet_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1637. SimpleGraph.mk'_mem_incidenceSet_left_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1638. SimpleGraph.mk'_mem_incidenceSet_right_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1639. SimpleGraph.ne_bot_iff_exists_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1640. SimpleGraph.ne_of_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1641. SimpleGraph.ne_of_adj_of_not_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1642. SimpleGraph.ne_top_iff_exists_not_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1643. SimpleGraph.neighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1644. SimpleGraph.neighborSet.memDecidable

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1645. SimpleGraph.neighborSet_bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1646. SimpleGraph.neighborSet_compl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1647. SimpleGraph.neighborSet_eq_compl_singleton

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1648. SimpleGraph.neighborSet_eq_empty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1649. SimpleGraph.neighborSet_iInf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1650. SimpleGraph.neighborSet_iSup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1651. SimpleGraph.neighborSet_inf

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1652. SimpleGraph.neighborSet_mono

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1653. SimpleGraph.neighborSet_ne_univ

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1654. SimpleGraph.neighborSet_nonempty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1655. SimpleGraph.neighborSet_sdiff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1656. SimpleGraph.neighborSet_subset_compl

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1657. SimpleGraph.neighborSet_subset_support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1658. SimpleGraph.neighborSet_sup

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1659. SimpleGraph.neighborSet_top

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1660. SimpleGraph.neighborSet_union_compl_neighborSet_eq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1661. SimpleGraph.nonempty_neighborSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1662. SimpleGraph.nontrivial_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1663. SimpleGraph.nontrivial_of_not_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1664. SimpleGraph.notMem_commonNeighbors_left

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1665. SimpleGraph.notMem_commonNeighbors_right

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1666. SimpleGraph.notMem_neighborSet_self

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1667. SimpleGraph.notMem_support_iff_isIsolated

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1668. SimpleGraph.not_isDiag_of_mem_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1669. SimpleGraph.not_isIsolated_iff_exists_edgeSet_mem

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1670. SimpleGraph.not_mem_edgeSet_of_isDiag

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1671. SimpleGraph.otherVertexOfIncident

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1672. SimpleGraph.sInf_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1673. SimpleGraph.sInf_adj_of_nonempty

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1674. SimpleGraph.sSup_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1675. SimpleGraph.sdiff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1676. SimpleGraph.sdiff_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1677. SimpleGraph.subsingleton_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1678. SimpleGraph.supSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1679. SimpleGraph.sup_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1680. SimpleGraph.support

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1681. SimpleGraph.support_bot

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1682. SimpleGraph.support_eq_bot_iff

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1683. SimpleGraph.support_mono

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1684. SimpleGraph.support_of_subsingleton

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1685. SimpleGraph.support_top_of_nontrivial

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1686. SimpleGraph.symm

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1687. SimpleGraph.symm_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1688. SimpleGraph.top_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1689. SimpleGraph.uniqueOfSubsingleton

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1690. Std.Irrefl.compl

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1691. Std.Refl.compl

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1692. Std.Symm.forall_existsUnique_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1693. Std.Symm.forall_existsUnique_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1694. StrongLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1695. StrongLT.le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1696. StrongLT.lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1697. StrongLT.trans_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1698. Subsingleton.eq_univ_of_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1699. Subsingleton.instDenselyOrdered

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1700. Subsingleton.mem_iff_nonempty

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1701. Subsingleton.set_cases

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1702. Subsingleton.to_isCancelMulZero

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1703. Subsingleton.to_noZeroDivisors

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1704. SubtractionMonoid.toSubNegZeroMonoid

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1705. SubtractionMonoid.toSubNegZeroMonoid._proof_1

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1706. Subtype.coe_le_coe

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1707. Subtype.coe_lt_coe

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1708. Subtype.decidableLE

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1709. Subtype.decidableLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1710. Subtype.instLinearOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1711. Subtype.mem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1712. Subtype.mk_le_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1713. Subtype.mk_lt_mk

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1714. Subtype.partialOrder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1715. Subtype.preorder

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1716. Sum.const_le_elim_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1717. Sum.elim_le_const_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1718. Sum.elim_le_elim_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1719. Sym2.IsDiag.not_mem_edgeSet

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1720. Symmetric.forall_existsUnique_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1721. Symmetric.forall_existsUnique_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1722. TopologicalSpace.ext

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1723. TopologicalSpace.ext_iff

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1724. TopologicalSpace.ext_iff_isClosed

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1725. TopologicalSpace.ext_isClosed

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1726. TopologicalSpace.ofClosed

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  1727. _aux_Mathlib_Combinatorics_SimpleGraph_Basic___macroRules_aesop_graph?_1

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1728. _aux_Mathlib_Combinatorics_SimpleGraph_Basic___macroRules_aesop_graph_1

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1729. _aux_Mathlib_Combinatorics_SimpleGraph_Basic___macroRules_aesop_graph_nonterminal_1

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1730. _aux_Mathlib_Order_Basic___unexpand_Order_Preimage_1

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1731. _private.Mathlib.Algebra.Group.Basic.0.add_add_add_comm'._proof_1_1

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1732. _private.Mathlib.Order.Basic.0._aux_Mathlib_Order_Basic___unexpand_StrongLT_1

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1733. _private.Mathlib.Order.Basic.0.«_aux_Mathlib_Order_Basic___macroRules__private_Mathlib_Order_Basic_0_term_≺__1»

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1734. _private.Mathlib.Order.Basic.0.«term_≺_»

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1735. addConj_eq_zero_iff

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1736. add_add_add_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1737. add_add_add_comm'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1738. add_add_neg_add_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1739. add_add_neg_cancel'_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1740. add_add_sub_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1741. add_comm_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1742. add_eq_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1743. add_eq_of_eq_add_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1744. add_eq_of_eq_neg_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1745. add_eq_of_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1746. add_eq_of_eq_sub'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1747. add_eq_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1748. add_eq_zero_iff_eq_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1749. add_eq_zero_iff_eq_neg'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1750. add_eq_zero_iff_neg_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1751. add_eq_zero_iff_neg_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1752. add_left_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1753. add_left_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1754. add_left_iterate._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1755. add_left_iterate_apply

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1756. add_left_iterate_apply_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1757. add_left_iterate_apply_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1758. add_left_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1759. add_ne_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1760. add_ne_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1761. add_neg_add_add_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1762. add_neg_eq_add_neg_iff_add_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1763. add_neg_eq_iff_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1764. add_neg_eq_of_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1765. add_neg_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1766. add_one_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1767. add_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1768. add_right_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1769. add_right_iterate._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1770. add_right_iterate_apply

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1771. add_right_iterate_apply_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1772. add_right_iterate_apply_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1773. add_right_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1774. add_rotate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1775. add_rotate'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1776. add_self_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1777. add_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1778. add_sub_add_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1779. add_sub_add_left_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1780. add_sub_add_right_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1781. add_sub_assoc'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1782. add_sub_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1783. add_sub_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1784. add_sub_left_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1785. add_sub_one_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1786. add_sub_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1787. add_sub_sub_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1788. add_zero_eq_id

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1789. add_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1790. add_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1791. add_zsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1792. add_zsmul_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1793. additive_of_symm_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1794. additive_of_symmetric_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1795. additive_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1796. aesop_graph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1797. aesop_graph?

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1798. aesop_graph_nonterminal

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1799. associative_of_commutative_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1800. boole_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1801. cast_bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1802. cast_inj

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1803. commutative_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1804. comp_add_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1805. comp_add_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1806. comp_mul_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1807. comp_mul_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1808. compare_of_injective_eq_compareOfLessAndEq

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1809. compl_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1810. compl_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1811. compl_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1812. compl_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1813. completeBipartiteGraph

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1814. completeBipartiteGraph_adj

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1815. conj_eq_one_iff

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1816. const_div_involutive

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1817. const_sub_involutive

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1818. dense_or_discrete

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1819. dense_or_discrete'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1820. dite_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1821. dite_smul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1822. dite_vadd

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1823. div_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1824. div_div_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1825. div_div_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1826. div_div_div_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1827. div_div_div_cancel_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1828. div_div_div_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1829. div_div_div_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1830. div_div_eq_mul_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1831. div_div_self'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1832. div_eq_div_iff_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1833. div_eq_div_iff_div_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1834. div_eq_div_iff_mul_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1835. div_eq_div_mul_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1836. div_eq_iff_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1837. div_eq_iff_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1838. div_eq_iff_eq_mul'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1839. div_eq_inv_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1840. div_eq_inv_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1841. div_eq_mul_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1842. div_eq_of_eq_mul'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1843. div_eq_of_eq_mul''

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1844. div_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1845. div_eq_one_of_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1846. div_eq_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1847. div_inv_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1848. div_left_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1849. div_left_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1850. div_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1851. div_mul_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1852. div_mul_cancel_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1853. div_mul_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1854. div_mul_div_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1855. div_mul_div_cancel'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1856. div_mul_div_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1857. div_mul_eq_div_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1858. div_mul_eq_div_div_swap

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1859. div_mul_eq_div_mul_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1860. div_mul_eq_mul_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1861. div_mul_mul_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1862. div_ne_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1863. div_ne_one_of_ne

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1864. div_neg

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1865. div_neg_eq_neg_div

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1866. div_neg_eq_neg_div'

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1867. div_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1868. div_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1869. div_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1870. div_right_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1871. div_right_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1872. div_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1873. eq_add_neg_iff_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1874. eq_add_neg_of_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1875. eq_add_of_add_neg_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1876. eq_add_of_neg_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1877. eq_add_of_sub_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1878. eq_add_of_sub_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1879. eq_div_iff_mul_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1880. eq_div_iff_mul_eq''

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1881. eq_div_of_mul_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1882. eq_div_of_mul_eq''

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1883. eq_iff_eq_of_add_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1884. eq_iff_eq_of_div_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1885. eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1886. eq_iff_eq_of_mul_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1887. eq_iff_eq_of_sub_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1888. eq_iff_ge_not_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1889. eq_iff_le_not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1890. eq_inv_iff_mul_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1891. eq_inv_mul_iff_mul_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1892. eq_inv_mul_of_mul_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1893. eq_inv_of_mul_eq_one_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1894. eq_mp_bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1895. eq_mpr_bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1896. eq_mul_inv_iff_mul_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1897. eq_mul_inv_of_mul_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1898. eq_mul_of_div_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1899. eq_mul_of_div_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1900. eq_mul_of_inv_mul_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1901. eq_mul_of_mul_inv_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1902. eq_neg_add_iff_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1903. eq_neg_add_of_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1904. eq_neg_iff_add_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1905. eq_neg_of_add_eq_zero_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1906. eq_of_add_neg_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1907. eq_of_div_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1908. eq_of_forall_ge_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1909. eq_of_forall_gt_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1910. eq_of_forall_le_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1911. eq_of_forall_lt_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1912. eq_of_inv_mul_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1913. eq_of_le_of_forall_gt_imp_ge_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1914. eq_of_le_of_forall_lt_imp_le_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1915. eq_of_le_of_not_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1916. eq_of_le_of_not_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1917. eq_of_mul_inv_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1918. eq_of_neg_add_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1919. eq_of_one_div_eq_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1920. eq_of_sub_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1921. eq_of_zero_sub_eq_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1922. eq_one_div_of_mul_eq_one_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1923. eq_one_div_of_mul_eq_one_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1924. eq_one_iff_eq_one_of_mul_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1925. eq_or_eq_or_eq_of_forall_not_lt_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1926. eq_or_lt_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1927. eq_or_lt_of_le'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1928. eq_rec_inj

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1929. eq_rec_on_bijective

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1930. eq_sub_iff_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1931. eq_sub_iff_add_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1932. eq_sub_of_add_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1933. eq_sub_of_add_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1934. eq_zero_iff_eq_zero_of_add_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1935. eq_zero_sub_of_add_eq_zero_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1936. eq_zero_sub_of_add_eq_zero_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1937. exists_between

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1938. exists_between'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1939. exists_forall_ge_and

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1940. exists_forall_le_and

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1941. exists_ge_of_linear

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1942. exists_le_of_linear

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1943. forall_existsUnique_iff

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1944. forall_existsUnique_iff'

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1945. forall_ge_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1946. forall_ge_imp_ne_iff_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1947. forall_gt_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1948. forall_gt_imp_ge_iff_le_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1949. forall_gt_imp_ne_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1950. forall_le_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1951. forall_le_imp_ne_iff_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1952. forall_lt_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1953. forall_lt_imp_le_iff_le_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1954. forall_lt_imp_ne_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1955. ge_imp_ge_of_le_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1956. ge_imp_gt_of_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1957. ge_imp_gt_of_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1958. ge_trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1959. gt_imp_gt_of_le_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1960. gt_trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1961. hom_coe_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1962. hom_coe_nsmul._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1963. hom_coe_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1964. instCoeTCElem

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  1965. instDecidableCurryOfMk_mathlib

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1966. instDecidableRelAdjFromRelOfDecidableEq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1967. instDecidableUncurryOfFstSnd_mathlib

    Mathlib.Logic.Function.BasicSOURCE_INDEXEDNOT_CHECKED

  1968. instDenselyOrderedForall

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1969. instDenselyOrderedProd

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1970. instFintypeSimpleGraphOfDecidableEq

    Mathlib.Combinatorics.SimpleGraph.BasicSOURCE_INDEXEDNOT_CHECKED

  1971. instLinearOrderEmpty

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1972. instLinearOrderPEmpty

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  1973. inv_bijective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1974. inv_comp_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1975. inv_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1976. inv_div'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1977. inv_div_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1978. inv_div_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1979. inv_div_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1980. inv_eq_iff_eq_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1981. inv_eq_iff_mul_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1982. inv_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1983. inv_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1984. inv_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1985. inv_inv_div_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1986. inv_involutive

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1987. inv_mul'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1988. inv_mul_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1989. inv_mul_eq_iff_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1990. inv_mul_eq_inv_mul_iff_mul_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1991. inv_mul_eq_of_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1992. inv_mul_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1993. inv_ne_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1994. inv_neg

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1995. inv_neg_one

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  1996. inv_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1997. inv_pow_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1998. inv_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  1999. inv_unique

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2000. inv_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2001. inv_zpow'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2002. isCancelMulZero_iff_isDomain_or_subsingleton

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2003. isCancelMulZero_iff_noZeroDivisors

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2004. isClosed_biInter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2005. isClosed_biUnion_finset

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2006. isClosed_compl_iff

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2007. isClosed_const

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2008. isClosed_empty

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2009. isClosed_iInter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2010. isClosed_iUnion_of_finite

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2011. isClosed_imp

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2012. isClosed_sInter

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2013. isClosed_univ

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2014. isDomain_iff_cancelMulZero_and_nontrivial

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2015. isDomain_iff_noZeroDivisors_and_nontrivial

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2016. isLeftRegular_iff_right_eq_zero_of_mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2017. isOpen_biInter_finset

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2018. isOpen_biUnion

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2019. isOpen_compl_iff

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2020. isOpen_const

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2021. isOpen_empty

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2022. isOpen_fold

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2023. isOpen_iInter_of_finite

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2024. isOpen_iUnion

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2025. isOpen_iff_of_cover

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2026. isOpen_mk

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2027. isRegular_iff_eq_zero_of_mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2028. isRightRegular_iff_left_eq_zero_of_mul

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2029. isSelfInv_neg_iff

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2030. isSelfNeg_inv_iff

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2031. ite_add_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2032. ite_mul_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2033. ite_one_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2034. ite_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2035. ite_smul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2036. ite_vadd

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2037. ite_zero_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2038. Evidence object · inspect its exact boundary

    jpl.l4yaml.finite_parser_acceptance

    Evidence recordsRESOLVE_CLAIMWARRANTED_BOUNDED

  2039. le_iff_eq_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2040. le_iff_eq_or_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2041. le_iff_le_iff_lt_iff_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2042. le_imp_eq_iff_le_imp_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2043. le_imp_eq_iff_le_imp_ge'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2044. le_imp_le_iff_lt_imp_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2045. le_imp_le_of_le_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2046. le_nhds_lim

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2047. le_of_forall_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2048. le_of_forall_gt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2049. le_of_forall_gt_imp_ge_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2050. le_of_forall_gt_imp_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2051. le_of_forall_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2052. le_of_forall_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2053. le_of_forall_lt_imp_le_of_dense

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2054. le_of_forall_lt_imp_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2055. le_of_strongLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2056. le_of_subsingleton

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2057. le_trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2058. le_update_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2059. le_update_self_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2060. leftInverse_add_left_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2061. leftInverse_add_right_neg_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2062. leftInverse_div_mul_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2063. leftInverse_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2064. leftInverse_inv_mul_mul_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2065. leftInverse_mul_left_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2066. leftInverse_mul_right_inv_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2067. leftInverse_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2068. leftInverse_neg_add_add_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2069. leftInverse_sub_add_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2070. left_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2071. left_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2072. left_ne_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2073. left_ne_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2074. limUnder_of_not_tendsto

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2075. lt_iff_le_and_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2076. lt_iff_le_and_ne'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2077. lt_iff_lt_of_le_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2078. lt_iff_lt_of_le_iff_le'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2079. lt_imp_lt_of_le_imp_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2080. lt_imp_lt_of_le_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2081. lt_of_forall_ge_imp_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2082. lt_of_forall_le_imp_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2083. lt_of_strongLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2084. lt_or_gt_iff_ne'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2085. lt_or_lt_iff_ne

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2086. lt_self_iff_false

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2087. lt_trans'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2088. lt_update_self_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2089. Evidence object · inspect its exact boundary

    mathgraph.l4yaml.48-case-qualification

    Evidence recordsRESOLVE_RECEIPTUNKNOWN

  2090. max_def_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2091. max_def_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2092. max_rec

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2093. max_rec'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2094. Evidence object · inspect its exact boundary

    mg-living-warrant-openai-jpl-20261010

    Evidence recordsRESOLUTION_SNAPSHOTSCOPED_MIXED

  2095. min_def_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2096. min_def_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2097. min_rec

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2098. min_rec'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2099. mul_comm_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2100. mul_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2101. mul_div_assoc'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2102. mul_div_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2103. mul_div_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2104. mul_div_div_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2105. mul_div_left_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2106. mul_div_mul_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2107. mul_div_mul_left_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2108. mul_div_mul_right_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2109. mul_div_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2110. mul_eq_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2111. mul_eq_of_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2112. mul_eq_of_eq_div'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2113. mul_eq_of_eq_inv_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2114. mul_eq_of_eq_mul_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2115. mul_eq_one_iff_eq_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2116. mul_eq_one_iff_eq_inv'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2117. mul_eq_one_iff_inv_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2118. mul_eq_one_iff_inv_eq'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2119. mul_eq_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2120. mul_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2121. mul_inv_eq_iff_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2122. mul_inv_eq_mul_inv_iff_mul_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2123. mul_inv_eq_of_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2124. mul_inv_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2125. mul_inv_mul_mul_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2126. mul_left_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2127. mul_left_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2128. mul_left_iterate_apply

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2129. mul_left_iterate_apply_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2130. mul_left_iterate_apply_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2131. mul_left_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2132. mul_mul_div_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2133. mul_mul_inv_cancel'_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2134. mul_mul_inv_mul_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2135. mul_mul_mul_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2136. mul_mul_mul_comm'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2137. mul_ne_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2138. mul_ne_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2139. mul_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2140. mul_one_eq_id

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2141. mul_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2142. mul_pow_sub_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2143. mul_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2144. mul_right_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2145. mul_right_iterate_apply

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2146. mul_right_iterate_apply_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2147. mul_right_iterate_apply_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2148. mul_right_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2149. mul_rotate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2150. mul_rotate'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2151. mul_self_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2152. mul_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2153. mul_zpow_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2154. mul_zpow_neg_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2155. mul_zpow_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2156. mul_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2157. mul_zsmul'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2158. multiplicative_of_symm_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2159. multiplicative_of_symmetric_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2160. multiplicative_of_total

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2161. natAbs_nsmul_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2162. natCast_sub_natCast_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2163. natCast_sub_one_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2164. ne_iff_gt_iff_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2165. ne_iff_lt_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2166. ne_iff_ne_of_add_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2167. ne_iff_ne_of_mul_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2168. ne_of_not_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2169. ne_of_not_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2170. neg_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2171. neg_add'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2172. neg_add_eq_iff_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2173. neg_add_eq_neg_add_iff_add_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2174. neg_add_eq_of_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2175. neg_add_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2176. neg_add_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2177. neg_bijective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2178. neg_comp_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2179. neg_div

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2180. neg_div'

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2181. neg_div_neg_eq

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2182. neg_eq_iff_add_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2183. neg_eq_iff_eq_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2184. neg_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2185. neg_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2186. neg_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2187. neg_inv

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2188. neg_involutive

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2189. neg_ne_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2190. neg_neg_sub_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2191. neg_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2192. neg_nsmul._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2193. neg_one_zsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2194. neg_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2195. neg_sub'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2196. neg_sub_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2197. neg_sub_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2198. neg_sub_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2199. neg_surjective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2200. neg_unique

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2201. neg_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2202. noZeroDivisors_iff_isDomain_or_subsingleton

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2203. noZeroDivisors_tfae

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2204. not_lt_iff_eq_or_lt

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2205. not_lt_iff_eq_or_lt'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2206. not_lt_iff_le_imp_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2207. not_lt_iff_not_le_or_ge

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2208. not_lt_of_subsingleton

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2209. nsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2210. nsmul_add._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2211. nsmul_add_nsmul_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2212. nsmul_add_nsmul_eq_zero._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2213. nsmul_add_sub_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2214. nsmul_eq_mod_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2215. nsmul_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2216. nsmul_iterate._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2217. nsmul_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2218. nsmul_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2219. one_add_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2220. one_div_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2221. one_div_mul_eq_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2222. one_div_mul_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2223. one_div_mul_one_div_rev

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2224. one_div_neg_eq_neg_one_div

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2225. one_div_neg_one_eq_neg_one

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2226. one_div_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2227. one_div_one_div

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2228. one_div_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2229. one_div_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2230. one_eq_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2231. one_mul_eq_id

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2232. one_sub_natCast_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2233. one_zpow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2234. Evidence object · inspect its exact boundary

    openai.original_publication_receipt.1

    Evidence recordsRESOLVE_RECEIPTUNKNOWN

  2235. Evidence object · inspect its exact boundary

    openai.original_publication_receipt.2

    Evidence recordsRESOLVE_RECEIPTUNKNOWN

  2236. Evidence object · inspect its exact boundary

    openai.original_publication_receipt.3

    Evidence recordsRESOLVE_RECEIPTUNKNOWN

  2237. Evidence object · inspect its exact boundary

    openai.original_support.1

    Evidence recordsRESOLVE_CLAIMSTALE

  2238. Evidence object · inspect its exact boundary

    openai.original_support.2

    Evidence recordsRESOLVE_CLAIMSTALE

  2239. Evidence object · inspect its exact boundary

    openai.original_support.3

    Evidence recordsRESOLVE_CLAIMSTALE

  2240. Evidence object · inspect its exact boundary

    openai.theorem.1

    Evidence recordsRESOLVE_CLAIMUNKNOWN

  2241. Evidence object · inspect its exact boundary

    openai.theorem.2

    Evidence recordsRESOLVE_CLAIMUNKNOWN

  2242. Evidence object · inspect its exact boundary

    openai.theorem.3

    Evidence recordsRESOLVE_CLAIMUNKNOWN

  2243. pow_boole

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2244. pow_dite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2245. pow_eq_pow_mod

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2246. pow_ite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2247. pow_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2248. pow_mul_pow_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2249. pow_mul_pow_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2250. pow_natAbs_eq_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2251. pow_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2252. pow_sub_mul_pow

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2253. pow_sub_one_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2254. pred_ne_self

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2255. rel_imp_eq_of_rel_imp_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2256. rightInverse_inv

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2257. rightInverse_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2258. right_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2259. right_eq_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2260. right_ne_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2261. right_ne_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2262. set_coe_cast

    Mathlib.Data.Set.BasicSOURCE_INDEXEDNOT_CHECKED

  2263. smul_dite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2264. smul_ite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2265. strongLT_of_le_of_strongLT

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2266. strongLT_of_strongLT_of_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2267. sub_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2268. sub_add_add_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2269. sub_add_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2270. sub_add_cancel_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2271. sub_add_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2272. sub_add_eq_add_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2273. sub_add_eq_sub_add_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2274. sub_add_eq_sub_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2275. sub_add_eq_sub_sub_swap

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2276. sub_add_sub_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2277. sub_add_sub_cancel'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2278. sub_add_sub_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2279. sub_eq_add_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2280. sub_eq_iff_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2281. sub_eq_iff_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2282. sub_eq_iff_eq_add'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2283. sub_eq_neg_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2284. sub_eq_neg_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2285. sub_eq_of_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2286. sub_eq_of_eq_add'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2287. sub_eq_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2288. sub_eq_sub_add_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2289. sub_eq_sub_iff_add_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2290. sub_eq_sub_iff_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2291. sub_eq_sub_iff_sub_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2292. sub_eq_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2293. sub_eq_zero_of_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2294. sub_left_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2295. sub_left_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2296. sub_ne_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2297. sub_ne_zero_of_ne

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2298. sub_neg_eq_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2299. sub_nsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2300. sub_nsmul_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2301. sub_nsmul_nsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2302. sub_one_nsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2303. sub_one_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2304. sub_right_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2305. sub_right_inj

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2306. sub_right_injective

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2307. sub_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2308. sub_sub_cancel

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2309. sub_sub_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2310. sub_sub_eq_add_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2311. sub_sub_self

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2312. sub_sub_sub_cancel_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2313. sub_sub_sub_cancel_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2314. sub_sub_sub_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2315. sub_sub_sub_eq

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2316. sub_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2317. sub_zsmul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2318. subrelation_iff_le

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2319. succ_ne_self

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2320. tendsto_nhds_limUnder

    Mathlib.Topology.BasicSOURCE_INDEXEDNOT_CHECKED

  2321. update_le_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2322. update_le_self_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2323. update_le_update_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2324. update_le_update_iff'

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2325. update_lt_self_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2326. update_lt_update_iff

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2327. Qualified bounded capability

    urn:mathgraph:capability:finite-developmental-growth

    CapabilitiesFINITE_CAPABILITYQUALIFIED_BOUNDED

  2328. vadd_dite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2329. vadd_ite

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2330. vieta_formula_quadratic

    Mathlib.Algebra.Ring.BasicSOURCE_INDEXEDNOT_CHECKED

  2331. zero_add_eq_id

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2332. zero_eq_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2333. zero_sub_add_eq_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2334. zero_sub_add_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2335. zero_sub_add_zero_sub_rev

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2336. zero_sub_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2337. zero_sub_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2338. zero_sub_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2339. zpow_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2340. zpow_add_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2341. zpow_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2342. zpow_eq_inv_pow_natAbs

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2343. zpow_eq_zpow_emod

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2344. zpow_eq_zpow_emod'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2345. zpow_induction_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2346. zpow_induction_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2347. zpow_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2348. zpow_mul

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2349. zpow_mul'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2350. zpow_mul_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2351. zpow_natCast_sub_natCast

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2352. zpow_natCast_sub_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2353. zpow_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2354. zpow_one_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2355. zpow_one_sub_natCast

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2356. zpow_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2357. zpow_sub_one

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2358. zsmul_add

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2359. zsmul_add_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2360. zsmul_comm

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2361. zsmul_eq_neg_nsmul_natAbs

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2362. zsmul_induction_left

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2363. zsmul_induction_right

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2364. zsmul_iterate

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2365. zsmul_iterate._f

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2366. zsmul_neg

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2367. zsmul_neg'

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2368. zsmul_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2369. zsmul_zero

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2370. zsmul_zero_sub

    Mathlib.Algebra.Group.BasicSOURCE_INDEXEDNOT_CHECKED

  2371. «_aux_Mathlib_Order_Basic___macroRules_term_⁻¹'o__1»

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

  2372. «term_⁻¹'o_»

    Mathlib.Order.BasicSOURCE_INDEXEDNOT_CHECKED

Verify

Open the boundary, not just the result.

Qualified records expose exact receipts, assumptions, source identities, replay instructions, and unknowns. Historical support never silently becomes current applicability.

Inspect qualified evidence → · See support withdrawal

Discover

Turn an omission into the next inspectable question.

Discover identifies source-grounded residuals and candidate next experiments. Its output is advisory until an appropriate independent verifier qualifies it.

Inspect the current discovery frontier →