Skip to content

Instantly share code, notes, and snippets.

@semorrison

semorrison/gist:633346603746803623f2f59af0511eab

Created August 4, 2020 23:35
Show Gist options
  • Save semorrison/633346603746803623f2f59af0511eab to your computer and use it in GitHub Desktop.
Save semorrison/633346603746803623f2f59af0511eab to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.initial_mono ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.image_to_kernel_map_mono ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @AddCommGroup.category_theory.mono ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.mono_pushout_of_mono_g ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.mono_pushout_of_mono_f ?x_31 ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.category_theory.mono ?x_41 ?x_42 ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.mono_factor_thru_image ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52 ?x_53
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @non_preadditive_abelian.mono_r ?x_54 ?x_55 ?x_56 ?x_57
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_58 : @non_preadditive_abelian C _inst_1 := @abelian.non_preadditive_abelian ?x_59 ?x_60 ?x_61
[class_instances] (1) ?x_61 : @abelian C _inst_1 := AddCommGroup.category_theory.abelian
failed is_def_eq
[class_instances] (1) ?x_61 : @abelian C _inst_1 := @Module.category_theory.abelian ?x_62 ?x_63
failed is_def_eq
[class_instances] caching failure for @abelian C _inst_1
[class_instances] caching failure for @non_preadditive_abelian C _inst_1
[class_instances] caching failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @non_preadditive_abelian.mono_Δ ?x_58 ?x_59 ?x_60 ?x_61
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @non_preadditive_abelian.category_theory.mono ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 ?x_67
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @non_preadditive_abelian.mono_factor_thru_image ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.pullback.snd_of_mono ?x_75 ?x_76 ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.pullback.fst_of_mono ?x_84 ?x_85 ?x_86 ?x_87 ?x_88 ?x_89 ?x_90 ?x_91 ?x_92
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.types.category_theory.mono ?x_93 ?x_94 ?x_95
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @preadditive.category_theory.mono ?x_96 ?x_97 ?x_98 ?x_99 ?x_100 ?x_101 ?x_102
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_103 : @preadditive C _inst_1 := AddCommGroup.category_theory.preadditive
failed is_def_eq
[class_instances] (0) ?x_103 : @preadditive C _inst_1 := @Module.category_theory.preadditive ?x_104 ?x_105
failed is_def_eq
[class_instances] (0) ?x_103 : @preadditive C _inst_1 := @abelian.to_preadditive ?x_106 ?x_107 ?x_108
[class_instances] cached failure for @abelian C _inst_1
[class_instances] caching failure for @preadditive C _inst_1
[class_instances] caching failure for @preadditive C _inst_1
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.kernel.lift_mono ?x_103 ?x_104 ?x_105 ?x_106 ?x_107 ?x_108 ?x_109 ?x_110 ?x_111 ?x_112 ?x_113
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.has_zero_object.category_theory.mono ?x_114 ?x_115 ?x_116 ?x_117 ?x_118
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @differential_object.has_zero_object ?x_120 ?x_121 ?x_122 ?x_123 ?x_124
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @graded_object.has_zero_object ?x_125 ?x_126 ?x_127 ?x_128 ?x_129
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := AddCommGroup.has_zero_object
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := CommGroup.category_theory.limits.has_zero_object
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := AddGroup.has_zero_object
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := Group.category_theory.limits.has_zero_object
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @Module.category_theory.limits.has_zero_object ?x_130 ?x_131
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := limits.has_zero_object_punit
failed is_def_eq
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @non_preadditive_abelian.has_zero_object ?x_132 ?x_133 ?x_134
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @limits.has_zero_object_of_has_terminal_object ?x_120 ?x_121 ?x_122 ?x_123
[class_instances] (1) ?x_123 : @limits.has_terminal C _inst_1 := @limits.category_theory.limits.has_terminal ?x_124 ?x_125 ?x_126
[class_instances] (2) ?x_126 : @limits.has_finite_products C _inst_1 := @abelian.has_finite_products ?x_127 ?x_128 ?x_129
[class_instances] cached failure for @abelian C _inst_1
[class_instances] (2) ?x_126 : @limits.has_finite_products C _inst_1 := @non_preadditive_abelian.has_finite_products ?x_127 ?x_128 ?x_129
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] (2) ?x_126 : @limits.has_finite_products C _inst_1 := @limits.has_finite_products_of_has_finite_biproducts ?x_127 ?x_128 ?x_129 ?x_130
[class_instances] (3) ?x_130 : @limits.has_finite_biproducts C _inst_1 ?x_129 := AddCommGroup.category_theory.limits.has_finite_biproducts
failed is_def_eq
[class_instances] (2) ?x_126 : @limits.has_finite_products C _inst_1 := @limits.has_finite_products_of_has_finite_limits ?x_127 ?x_128 ?x_129
[class_instances] (3) ?x_129 : @limits.has_finite_limits C _inst_1 := @over.has_finite_limits ?x_130 ?x_131 ?x_132 ?x_133
failed is_def_eq
[class_instances] (3) ?x_129 : @limits.has_finite_limits C _inst_1 := @limits.has_finite_limits_of_semilattice_inf_top ?x_134 ?x_135
failed is_def_eq
[class_instances] (3) ?x_129 : @limits.has_finite_limits C _inst_1 := @limits.category_theory.limits.has_finite_limits ?x_136 ?x_137 ?x_138
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := Top.Top_has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @over.has_limits ?x_139 ?x_140 ?x_141 ?x_142
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @under.has_limits ?x_143 ?x_144 ?x_145 ?x_146
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @limits.has_limits_op_of_has_colimits ?x_147 ?x_148 ?x_149
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @limits.functor_category_has_limits ?x_150 ?x_151 ?x_152 ?x_153 ?x_154
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @Algebra.has_limits ?x_155 ?x_156
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := CommRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := Ring.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := CommSemiRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := SemiRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @Module.has_limits ?x_157 ?x_158
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := AddCommGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := CommGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := AddGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := Group.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := AddCommMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := CommMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := AddMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := Mon.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := limits.types.category_theory.limits.has_limits
failed is_def_eq
[class_instances] (4) ?x_138 : @limits.has_limits C _inst_1 := @limits.has_limits_of_complete_lattice ?x_159 ?x_160
failed is_def_eq
[class_instances] caching failure for @limits.has_limits C _inst_1
[class_instances] caching failure for @limits.has_finite_limits C _inst_1
[class_instances] (2) ?x_126 : @limits.has_finite_products C _inst_1 := @limits.has_finite_products_of_has_products ?x_127 ?x_128 ?x_129
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @over.has_connected_limits (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J) (?x_135 J) (?x_136 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @under.has_limits_of_shape (?x_137 J) (?x_138 J) (?x_139 J) (?x_140 J) (?x_141 J) (?x_142 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_products_opposite (?x_143 J) (?x_144 J) (?x_145 J) (?x_146 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_limits_of_shape_op_of_has_colimits_of_shape (?x_147 J) (?x_148 J) (?x_149 J) (?x_150 J) (?x_151 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.functor_category_has_limits_of_shape (?x_152 J) (?x_153 J) (?x_154 J) (?x_155 J) (?x_156 J) (?x_157 J)
(?x_158 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_finite_products.has_limits_of_shape (?x_159 J) (?x_160 J) (?x_161 J) (?x_162 J) (?x_163 J) (?x_164 J)
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.ring2.horner_expr.decidable_eq (?x_165 J a b) (?x_166 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := side.decidable_eq (?x_167 J a b) (?x_168 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nonote.decidable_lt (?x_169 J a b) (?x_170 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nonote.decidable_eq (?x_171 J a b) (?x_172 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := onote.decidable_NF (?x_173 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := onote.decidable_top_below (?x_174 J a b) (?x_175 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := onote.decidable_eq (?x_176 J a b) (?x_177 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finsets.decidable_eq (?x_178 J a b) (?x_179 J a b) (?x_180 J a b) (?x_181 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lists.mem.decidable (?x_182 J a b) (?x_183 J a b) (?x_184 J a b) (?x_185 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lists.subset.decidable (?x_186 J a b) (?x_187 J a b) (?x_188 J a b) (?x_189 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lists.equiv.decidable (?x_190 J a b) (?x_191 J a b) (?x_192 J a b) (?x_193 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lists.decidable_eq (?x_194 J a b) (?x_195 J a b) (?x_196 J a b) (?x_197 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lists'.decidable_eq (?x_198 J a b) (?x_199 J a b) (?x_200 J a b) (?x_201 J a b) (?x_202 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @pgame.equiv_decidable (?x_203 J a b) (?x_204 J a b) (?x_205 J a b) (?x_206 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @pgame.lt_decidable (?x_207 J a b) (?x_208 J a b) (?x_209 J a b) (?x_210 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @pgame.le_decidable (?x_211 J a b) (?x_212 J a b) (?x_213 J a b) (?x_214 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lex.decidable_eq (?x_215 J a b) (?x_216 J a b) (?x_217 J a b) (?x_218 J a b) (?x_219 J a b) (?x_220 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := lucas_lehmer.X.decidable_eq (?x_221 J a b) (?x_222 J a b) (?x_223 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := lucas_lehmer.lucas_lehmer_test.decidable_pred (?x_224 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @decidable_list_all (?x_225 J a b) (?x_226 J a b) (?x_227 J a b) (?x_228 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @uchange.decidable_eq (?x_229 J a b) (?x_230 J a b) (?x_231 J a b) (?x_232 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @semidirect_product.decidable_eq (?x_233 J a b) (?x_234 J a b) (?x_235 J a b) (?x_236 J a b) (?x_237 J a b)
(?x_238 J a b)
(?x_239 J a b)
(?x_240 J a b)
(?x_241 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_245 J a b).decidable_rel (?x_246 J a b) (?x_247 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @mv_polynomial.decidable_restrict_degree (?x_248 J a b) (?x_249 J a b) (?x_250 J a b) (?x_251 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @adjoin_root.decidable_eq (?x_252 J a b) (?x_253 J a b) (?x_254 J a b) (?x_255 J a b) (?x_256 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @function.is_periodic_pt.decidable (?x_257 J a b) (?x_258 J a b) (?x_259 J a b) (?x_260 J a b) (?x_261 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_263 J a b).decidable_le (?x_264 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_266 J a b).decidable_nonneg
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := zsqrtd.decidable_nonnegg (?x_267 J a b) (?x_268 J a b) (?x_269 J a b) (?x_270 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @zsqrtd.decidable_eq (?x_271 J a b) (?x_272 J a b) (?x_273 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := zmod.decidable_eq (?x_274 J a b) (?x_275 J a b) (?x_276 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @sym2.is_diag.decidable_pred (?x_277 J a b) (?x_278 J a b) (?x_279 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := irrational.decidable (?x_280 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := num.decidable_prime (?x_281 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos_num.decidable_prime (?x_282 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @lazy_list.decidable_eq (?x_283 J a b) (?x_284 J a b) (?x_285 J a b) (?x_286 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @thunk.decidable_eq (?x_287 J a b) (?x_288 J a b) (?x_289 J a b) (?x_290 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := int.decidable_pred (?x_291 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fp.dec_valid_finite (?x_292 J a b) (?x_293 J a b) (?x_294 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finmap.decidable_rel (?x_295 J a b) (?x_296 J a b) (?x_297 J a b) (?x_298 J a b) (?x_299 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finmap.decidable (?x_300 J a b) (?x_301 J a b) (?x_302 J a b) (?x_303 J a b) (?x_304 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finmap.has_decidable_eq (?x_305 J a b) (?x_306 J a b) (?x_307 J a b) (?x_308 J a b) (?x_309 J a b) (?x_310 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @alist.decidable (?x_311 J a b) (?x_312 J a b) (?x_313 J a b) (?x_314 J a b) (?x_315 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @alist.decidable_eq (?x_316 J a b) (?x_317 J a b) (?x_318 J a b) (?x_319 J a b) (?x_320 J a b) (?x_321 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @buffer.decidable_eq (?x_322 J a b) (?x_323 J a b) (?x_324 J a b) (?x_325 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := turing.partrec_to_TM2.K'.decidable_eq (?x_326 J a b) (?x_327 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := turing.partrec_to_TM2.Γ'.decidable_eq (?x_328 J a b) (?x_329 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := znum.decidable_rel (?x_330 J a b) (?x_331 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos_num.decidable_dvd (?x_332 J a b) (?x_333 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := num.decidable_dvd (?x_334 J a b) (?x_335 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := snum.decidable_eq (?x_336 J a b) (?x_337 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nzsnum.decidable_eq (?x_338 J a b) (?x_339 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @bitvec.ugt.decidable (?x_340 J a b) (?x_341 J a b) (?x_342 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @bitvec.ult.decidable (?x_343 J a b) (?x_344 J a b) (?x_345 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := turing.dir.decidable_eq (?x_346 J a b) (?x_347 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := expr_lens.dir.decidable_eq (?x_348 J a b) (?x_349 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nat.decidable_pred (?x_350 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := complex.decidable_eq (?x_351 J a b) (?x_352 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_353 J a b).decidable_eq (?x_354 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_355 J a b).decidable_le (?x_356 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_357 J a b).decidable_lt (?x_358 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.decl_reducibility.decidable_eq (?x_359 J a b) (?x_360 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_add_semigroup.decidable_eq (?x_361 J a b) (?x_362 J a b) (?x_363 J a b) (?x_364 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_semigroup.decidable_eq (?x_365 J a b) (?x_366 J a b) (?x_367 J a b) (?x_368 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_add_magma.decidable_eq (?x_369 J a b) (?x_370 J a b) (?x_371 J a b) (?x_372 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_magma.decidable_eq (?x_373 J a b) (?x_374 J a b) (?x_375 J a b) (?x_376 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_378 J a b).terminated_at_decidable (?x_379 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_381 J a b).terminated_at_decidable (?x_382 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @dfinsupp.decidable_eq (?x_383 J a b) (?x_384 J a b) (?x_385 J a b) (?x_386 J a b) (?x_387 J a b) (?x_388 J a b)
(?x_389 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @dfinsupp.decidable_zero (?x_390 J a b) (?x_391 J a b) (?x_392 J a b) (?x_393 J a b) (?x_394 J a b) (?x_395 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @matrix.decidable_rel (?x_396 J a b) (?x_397 J a b) (?x_398 J a b) (?x_399 J a b) (?x_400 J a b) (?x_401 J a b)
(?x_402 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @decidable_gpowers (?x_403 J a b) (?x_404 J a b) (?x_405 J a b) (?x_406 J a b) (?x_407 J a b) (?x_408 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := multiplicity.decidable_int (?x_409 J a b) (?x_410 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := multiplicity.decidable_nat (?x_411 J a b) (?x_412 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := enat.decidable (?x_413 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @roption.of_option_decidable (?x_414 J a b) (?x_415 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @roption.some_decidable (?x_416 J a b) (?x_417 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @roption.none_decidable (?x_418 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @function.is_fixed_pt.decidable (?x_419 J a b) (?x_420 J a b) (?x_421 J a b) (?x_422 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @int.modeq.decidable (?x_423 J a b) (?x_424 J a b) (?x_425 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nat.modeq.decidable (?x_426 J a b) (?x_427 J a b) (?x_428 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_group.red.decidable_rel (?x_429 J a b) (?x_430 J a b) (?x_431 J a b) (?x_432 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @free_group.decidable_eq (?x_433 J a b) (?x_434 J a b) (?x_435 J a b) (?x_436 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fin_category.decidable_eq_hom (?x_437 J a b) (?x_438 J a b) (?x_439 J a b) (?x_440 J a b) (?x_441 J a b) (?x_442 J a b)
(?x_443 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fin_category.decidable_eq_obj (?x_444 J a b) (?x_445 J a b) (?x_446 J a b) (?x_447 J a b) (?x_448 J a b)
[class_instances] (5) ?x_446 J a b : @fin_category J (?x_445 J a b) := @limits.fin_category_wide_pushout (?x_449 J a b) (?x_450 J a b) (?x_451 J a b)
failed is_def_eq
[class_instances] (5) ?x_446 J a b : @fin_category J (?x_445 J a b) := @limits.fin_category_wide_pullback (?x_452 J a b) (?x_453 J a b) (?x_454 J a b)
failed is_def_eq
[class_instances] (5) ?x_446 J a b : @fin_category J (?x_445 J a b) := limits.category_theory.fin_category
failed is_def_eq
[class_instances] (5) ?x_446 J a b : @fin_category J (?x_445 J a b) := @category_theory.fin_category_discrete_of_decidable_fintype (?x_455 J a b) (?x_456 J a b) (?x_457 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @limits.wide_pushout_shape.hom.decidable_eq (?x_165 J a b) (?x_166 J a b) (?x_167 J a b) (?x_168 J a b) (?x_169 J a b)
(?x_170 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @limits.wide_pullback_shape.hom.decidable_eq (?x_171 J a b) (?x_172 J a b) (?x_173 J a b) (?x_174 J a b) (?x_175 J a b)
(?x_176 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @mv_polynomial.decidable_eq_mv_polynomial (?x_177 J a b) (?x_178 J a b) (?x_179 J a b) (?x_180 J a b) (?x_181 J a b)
(?x_182 J a b)
(?x_183 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := omega.nat.preterm.decidable_eq (?x_184 J a b) (?x_185 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @polynomial.decidable (?x_186 J a b) (?x_187 J a b) (?x_188 J a b) (?x_189 J a b) (?x_190 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @polynomial.monic.decidable (?x_191 J a b) (?x_192 J a b) (?x_193 J a b) (?x_194 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := string.decidable_le (?x_195 J a b) (?x_196 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := string.decidable_lt (?x_197 J a b) (?x_198 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.ring_exp.ex_type.decidable_eq (?x_199 J a b) (?x_200 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.ring_exp.coeff.decidable_eq (?x_201 J a b) (?x_202 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @add_con.decidable_eq (?x_203 J a b) (?x_204 J a b) (?x_205 J a b) (?x_206 J a b) (?x_207 J a b) (?x_208 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @con.decidable_eq (?x_209 J a b) (?x_210 J a b) (?x_211 J a b) (?x_212 J a b) (?x_213 J a b) (?x_214 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := finsupp.decidable_le (?x_215 J a b) (?x_216 J a b) (?x_217 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finsupp.finsupp.decidable_eq (?x_218 J a b) (?x_219 J a b) (?x_220 J a b) (?x_221 J a b) (?x_222 J a b) (?x_223 J a b)
(?x_224 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := limits.walking_parallel_pair_hom.decidable_eq (?x_225 J a b) (?x_226 J a b) (?x_227 J a b) (?x_228 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := limits.walking_parallel_pair.decidable_eq (?x_229 J a b) (?x_230 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := limits.walking_pair.decidable_eq (?x_231 J a b) (?x_232 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_right_inverse_fintype (?x_233 J a b) (?x_234 J a b) (?x_235 J a b) (?x_236 J a b) (?x_237 J a b)
(?x_238 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_left_inverse_fintype (?x_239 J a b) (?x_240 J a b) (?x_241 J a b) (?x_242 J a b) (?x_243 J a b)
(?x_244 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_bijective_fintype (?x_245 J a b) (?x_246 J a b) (?x_247 J a b) (?x_248 J a b) (?x_249 J a b)
(?x_250 J a b)
(?x_251 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_surjective_fintype (?x_252 J a b) (?x_253 J a b) (?x_254 J a b) (?x_255 J a b) (?x_256 J a b)
(?x_257 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_injective_fintype (?x_258 J a b) (?x_259 J a b) (?x_260 J a b) (?x_261 J a b) (?x_262 J a b)
(?x_263 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_eq_equiv_fintype (?x_264 J a b) (?x_265 J a b) (?x_266 J a b) (?x_267 J a b) (?x_268 J a b)
(?x_269 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_exists_fintype (?x_270 J a b) (?x_271 J a b) (?x_272 J a b) (?x_273 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_forall_fintype (?x_274 J a b) (?x_275 J a b) (?x_276 J a b) (?x_277 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fintype.decidable_pi_fintype (?x_278 J a b) (?x_279 J a b) (?x_280 J a b) (?x_281 J a b) (?x_282 J a b) (?x_283 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @vector.decidable_eq (?x_284 J a b) (?x_285 J a b) (?x_286 J a b) (?x_287 J a b) (?x_288 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_291 J a b).decidable_disjoint (?x_292 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.decidable_dexists_finset (?x_293 J a b) (?x_294 J a b) (?x_295 J a b) (?x_296 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.decidable_eq_pi_finset (?x_297 J a b) (?x_298 J a b) (?x_299 J a b) (?x_300 J a b) (?x_301 J a b) (?x_302 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.decidable_dforall_finset (?x_303 J a b) (?x_304 J a b) (?x_305 J a b) (?x_306 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.decidable_mem' (?x_307 J a b) (?x_308 J a b) (?x_309 J a b) (?x_310 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.decidable_mem (?x_311 J a b) (?x_312 J a b) (?x_313 J a b) (?x_314 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @finset.has_decidable_eq (?x_315 J a b) (?x_316 J a b) (?x_317 J a b) (?x_318 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.interactive.decidable_eq (?x_319 J a b) (?x_320 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.interactive.mono_selection.decidable_eq (?x_321 J a b) (?x_322 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_325 J a b).nodup_decidable
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @multiset.decidable_dexists_multiset (?x_326 J a b) (?x_327 J a b) (?x_328 J a b) (?x_329 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @multiset.decidable_eq_pi_multiset (?x_330 J a b) (?x_331 J a b) (?x_332 J a b) (?x_333 J a b) (?x_334 J a b)
(?x_335 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @multiset.decidable_dforall_multiset (?x_336 J a b) (?x_337 J a b) (?x_338 J a b) (?x_339 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @multiset.decidable_mem (?x_340 J a b) (?x_341 J a b) (?x_342 J a b) (?x_343 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @multiset.has_decidable_eq (?x_344 J a b) (?x_345 J a b) (?x_346 J a b) (?x_347 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @tree.decidable_eq (?x_348 J a b) (?x_349 J a b) (?x_350 J a b) (?x_351 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := znum.decidable_le (?x_352 J a b) (?x_353 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := znum.decidable_lt (?x_354 J a b) (?x_355 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := num.decidable_le (?x_356 J a b) (?x_357 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := num.decidable_lt (?x_358 J a b) (?x_359 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos_num.decidable_le (?x_360 J a b) (?x_361 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos_num.decidable_lt (?x_362 J a b) (?x_363 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := znum.decidable_eq (?x_364 J a b) (?x_365 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := num.decidable_eq (?x_366 J a b) (?x_367 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos_num.decidable_eq (?x_368 J a b) (?x_369 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := linarith.ineq.decidable_eq (?x_370 J a b) (?x_371 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @int.decidable_lt_le (?x_372 J a b) (?x_373 J a b) (?x_374 J a b) (?x_375 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @int.decidable_lt_lt (?x_376 J a b) (?x_377 J a b) (?x_378 J a b) (?x_379 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @int.decidable_le_le (?x_380 J a b) (?x_381 J a b) (?x_382 J a b) (?x_383 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @int.decidable_le_lt (?x_384 J a b) (?x_385 J a b) (?x_386 J a b) (?x_387 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := rat.decidable_le (?x_388 J a b) (?x_389 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_390 J a b).decidable_nonneg
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := rat.decidable_eq (?x_391 J a b) (?x_392 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @ulower.decidable_eq (?x_393 J a b) (?x_394 J a b) (?x_395 J a b) (?x_396 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @psigma.decidable_eq (?x_397 J a b) (?x_398 J a b) (?x_399 J a b) (?x_400 J a b) (?x_401 J a b) (?x_402 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @sigma.decidable_eq (?x_403 J a b) (?x_404 J a b) (?x_405 J a b) (?x_406 J a b) (?x_407 J a b) (?x_408 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pnat.decidable_eq (?x_409 J a b) (?x_410 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_411 J a b).decidable_prime
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_414 J a b).decidable_perm (?x_415 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_416 J a b).decidable (?x_417 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := int.decidable_dvd (?x_418 J a b) (?x_419 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_422 J a b).decidable_infix (?x_423 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_426 J a b).decidable_suffix (?x_427 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_430 J a b).decidable_prefix (?x_431 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_435 J a b).decidable_exists_mem
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.lex.decidable_rel (?x_436 J a b) (?x_437 J a b) (?x_438 J a b) (?x_439 J a b) (?x_440 J a b) (?x_441 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_444 J a b).decidable_sublist (?x_445 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @nat.decidable_lo_hi_le (?x_446 J a b) (?x_447 J a b) (?x_448 J a b) (?x_449 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @nat.decidable_lo_hi (?x_450 J a b) (?x_451 J a b) (?x_452 J a b) (?x_453 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @nat.decidable_ball_le (?x_454 J a b) (?x_455 J a b) (?x_456 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @nat.decidable_forall_fin (?x_457 J a b) (?x_458 J a b) (?x_459 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @nat.decidable_ball_lt (?x_460 J a b) (?x_461 J a b) (?x_462 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @plift.decidable_eq (?x_463 J a b) (?x_464 J a b) (?x_465 J a b) (?x_466 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @ulift.decidable_eq (?x_467 J a b) (?x_468 J a b) (?x_469 J a b) (?x_470 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @set.univ_decidable (?x_471 J a b) (?x_472 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @set.decidable_set_of (?x_473 J a b) (?x_474 J a b) (?x_475 J a b) (?x_476 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @set.decidable_mem (?x_477 J a b) (?x_478 J a b) (?x_479 J a b) (?x_480 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @with_bot.decidable_lt (?x_481 J a b) (?x_482 J a b) (?x_483 J a b) (?x_484 J a b) (?x_485 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @order.preimage.decidable (?x_486 J a b) (?x_487 J a b) (?x_488 J a b) (?x_489 J a b) (?x_490 J a b) (?x_491 J a b)
(?x_492 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @prod.lex.decidable (?x_493 J a b) (?x_494 J a b) (?x_495 J a b) (?x_496 J a b) (?x_497 J a b) (?x_498 J a b)
(?x_499 J a b)
(?x_500 J a b)
(?x_501 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @add_units.decidable_eq (?x_502 J a b) (?x_503 J a b) (?x_504 J a b) (?x_505 J a b) (?x_506 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @units.decidable_eq (?x_507 J a b) (?x_508 J a b) (?x_509 J a b) (?x_510 J a b) (?x_511 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.suggest.head_symbol_match.decidable_eq (?x_512 J a b) (?x_513 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.simp_arg_type.decidable_eq (?x_514 J a b) (?x_515 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @function.decidable_eq_pfun (?x_516 J a b) (?x_517 J a b) (?x_518 J a b) (?x_519 J a b) (?x_520 J a b) (?x_521 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @sum.decidable_eq (?x_522 J a b) (?x_523 J a b) (?x_524 J a b) (?x_525 J a b) (?x_526 J a b) (?x_527 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := norm_cast.label.decidable_eq (?x_528 J a b) (?x_529 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := auto.case_option.decidable_eq (?x_530 J a b) (?x_531 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := auto.auto_config.decidable_eq (?x_532 J a b) (?x_533 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := lint_verbosity.decidable_eq (?x_534 J a b) (?x_535 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.transparency.decidable_eq (?x_536 J a b) (?x_537 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := widget_override.local_collection.decidable_eq (?x_538 J a b) (?x_539 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := widget_override.filter_type.decidable_eq (?x_540 J a b) (?x_541 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @bool.decidable_exists_bool (?x_542 J a b) (?x_543 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @bool.decidable_forall_bool (?x_544 J a b) (?x_545 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @pexpr.decidable_eq (?x_546 J a b) (?x_547 J a b) (?x_548 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := binder.decidable_eq (?x_549 J a b) (?x_550 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := congr_arg_kind.decidable_eq (?x_551 J a b) (?x_552 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := binder_info.decidable_eq (?x_553 J a b) (?x_554 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_557 J a b).nodup_decidable
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_561 J a b).decidable_chain'
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.decidable_chain (?x_562 J a b) (?x_563 J a b) (?x_564 J a b) (?x_565 J a b) (?x_566 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_570 J a b).decidable_pairwise
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pempty.decidable_eq (?x_571 J a b) (?x_572 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := empty.decidable_eq (?x_573 J a b) (?x_574 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := doc_category.decidable_eq (?x_575 J a b) (?x_576 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_580 J a b).decidable_exists_mem
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_584 J a b).decidable_forall_mem
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := native.float.dec_eq (?x_585 J a b) (?x_586 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := native.float.decidable_le (?x_587 J a b) (?x_588 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := native.float.decidable_lt (?x_589 J a b) (?x_590 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := rbnode.color.decidable_eq (?x_591 J a b) (?x_592 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @array.decidable_eq (?x_593 J a b) (?x_594 J a b) (?x_595 J a b) (?x_596 J a b) (?x_597 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @d_array.decidable_eq (?x_598 J a b) (?x_599 J a b) (?x_600 J a b) (?x_601 J a b) (?x_602 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @subtype.decidable_eq (?x_603 J a b) (?x_604 J a b) (?x_605 J a b) (?x_606 J a b) (?x_607 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_punctuation (?x_608 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_alphanum (?x_609 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_digit (?x_610 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_alpha (?x_611 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_lower (?x_612 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_upper (?x_613 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_is_whitespace (?x_614 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_615 J a b).decidable_lt (?x_616 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_617 J a b).decidable_le (?x_618 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := int.decidable_eq (?x_619 J a b) (?x_620 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.decidable_ball (?x_621 J a b) (?x_622 J a b) (?x_623 J a b) (?x_624 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.decidable_bex (?x_625 J a b) (?x_626 J a b) (?x_627 J a b) (?x_628 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nat.decidable_dvd (?x_629 J a b) (?x_630 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := widget.local_collection.decidable_eq (?x_631 J a b) (?x_632 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := widget.filter_type.decidable_eq (?x_633 J a b) (?x_634 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := expr.address.has_dec_eq (?x_635 J a b) (?x_636 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := expr.coord.has_dec_eq (?x_637 J a b) (?x_638 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @local_context.decidable (?x_639 J a b) (?x_640 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := local_context.decidable_rel (?x_641 J a b) (?x_642 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := local_context.has_decidable_eq (?x_643 J a b) (?x_644 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := vm_obj_kind.decidable_eq (?x_645 J a b) (?x_646 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := tactic.binder_info.has_decidable_eq (?x_647 J a b) (?x_648 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := punit.decidable_eq (?x_649 J a b) (?x_650 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := expr.decidable_rel (?x_651 J a b) (?x_652 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := expr.has_decidable_eq (?x_653 J a b) (?x_654 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := pos.decidable_eq (?x_655 J a b) (?x_656 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := level.has_decidable_eq (?x_657 J a b) (?x_658 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := options.has_decidable_eq (?x_659 J a b) (?x_660 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @option.decidable_eq (?x_661 J a b) (?x_662 J a b) (?x_663 J a b) (?x_664 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := name.has_decidable_eq (?x_665 J a b) (?x_666 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := name.lt.decidable_rel (?x_667 J a b) (?x_668 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := coe_decidable_eq (?x_669 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := ordering.decidable_eq (?x_670 J a b) (?x_671 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := unsigned.decidable_eq (?x_672 J a b) (?x_673 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := fin.decidable_eq (?x_674 J a b) (?x_675 J a b) (?x_676 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_678 J a b).decidable_le (?x_679 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_681 J a b).decidable_lt (?x_682 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := string.has_decidable_eq (?x_683 J a b) (?x_684 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_685 J a b).has_decidable_lt (?x_686 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := char.decidable_eq (?x_687 J a b) (?x_688 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_689 J a b).decidable_le (?x_690 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_691 J a b).decidable_lt (?x_692 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_696 J a b).has_decidable_le (?x_697 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_701 J a b).has_decidable_lt (?x_702 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.decidable_mem (?x_703 J a b) (?x_704 J a b) (?x_705 J a b) (?x_706 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @list.decidable_eq (?x_707 J a b) (?x_708 J a b) (?x_709 J a b) (?x_710 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @quotient.decidable_eq (?x_711 J a b) (?x_712 J a b) (?x_713 J a b) (?x_714 J a b) (?x_715 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_716 J a b).decidable_lt (?x_717 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_718 J a b).decidable_le (?x_719 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := nat.decidable_eq (?x_720 J a b) (?x_721 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @prod_has_decidable_lt (?x_722 J a b) (?x_723 J a b) (?x_724 J a b) (?x_725 J a b) (?x_726 J a b) (?x_727 J a b)
(?x_728 J a b)
(?x_729 J a b)
(?x_730 J a b)
(?x_731 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @prod.decidable_eq (?x_732 J a b) (?x_733 J a b) (?x_734 J a b) (?x_735 J a b) (?x_736 J a b) (?x_737 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @dite.decidable (?x_738 J a b) (?x_739 J a b) (?x_740 J a b) (?x_741 J a b) (?x_742 J a b) (?x_743 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @ite.decidable (?x_744 J a b) (?x_745 J a b) (?x_746 J a b) (?x_747 J a b) (?x_748 J a b) (?x_749 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := bool.decidable_eq (?x_750 J a b) (?x_751 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @ne.decidable (?x_752 J a b) (?x_753 J a b) (?x_754 J a b) (?x_755 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @forall_prop_decidable (?x_756 J a b) (?x_757 J a b) (?x_758 J a b) (?x_759 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @exists_prop_decidable (?x_760 J a b) (?x_761 J a b) (?x_762 J a b) (?x_763 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @xor.decidable (?x_764 J a b) (?x_765 J a b) (?x_766 J a b) (?x_767 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @iff.decidable (?x_768 J a b) (?x_769 J a b) (?x_770 J a b) (?x_771 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @implies.decidable (?x_772 J a b) (?x_773 J a b) (?x_774 J a b) (?x_775 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @not.decidable (?x_776 J a b) (?x_777 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @or.decidable (?x_778 J a b) (?x_779 J a b) (?x_780 J a b) (?x_781 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @and.decidable (?x_782 J a b) (?x_783 J a b) (?x_784 J a b) (?x_785 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := decidable.false
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := decidable.true
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := (?x_789 J a b).decidable_forall_mem
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @fin_enum.dec_eq (?x_790 J a b) (?x_791 J a b) (?x_792 J a b) (?x_793 J a b)
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.pfun_fin_enum (?x_794 J a b) (?x_795 J a b) (?x_796 J a b) (?x_797 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.pi.fin_enum (?x_798 J a b) (?x_799 J a b) (?x_800 J a b) (?x_801 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.psigma.fin_enum_prop_prop (?x_802 J a b) (?x_803 J a b) (?x_804 J a b) (?x_805 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.psigma.fin_enum_prop_right (?x_806 J a b) (?x_807 J a b) (?x_808 J a b) (?x_809 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.psigma.fin_enum_prop_left (?x_810 J a b) (?x_811 J a b) (?x_812 J a b) (?x_813 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.psigma.fin_enum (?x_814 J a b) (?x_815 J a b) (?x_816 J a b) (?x_817 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.fin_enum (?x_818 J a b) (?x_819 J a b) (?x_820 J a b) (?x_821 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.subtype.fin_enum (?x_822 J a b) (?x_823 J a b) (?x_824 J a b) (?x_825 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.finset.fin_enum (?x_826 J a b) (?x_827 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.quotient.enum (?x_828 J a b) (?x_829 J a b) (?x_830 J a b) (?x_831 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.fin (?x_832 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.sum (?x_833 J a b) (?x_834 J a b) (?x_835 J a b) (?x_836 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := @fin_enum.prod (?x_837 J a b) (?x_838 J a b) (?x_839 J a b) (?x_840 J a b)
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := fin_enum.punit
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := fin_enum.empty
failed is_def_eq
[class_instances] (5) ?x_791 J a b : fin_enum J := fin_enum.pempty
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → fin_enum J
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @eq.decidable (?x_165 J a b) (?x_166 J a b) (?x_167 J a b) (?x_168 J a b)
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := nonote.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @dlex_decidable_linear_order (?x_169 J a b) (?x_170 J a b) (?x_171 J a b) (?x_172 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @lex_decidable_linear_order (?x_173 J a b) (?x_174 J a b) (?x_175 J a b) (?x_176 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @zsqrtd.decidable_linear_order (?x_177 J a b) _
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := znum.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := pos_num.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := nnreal.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := real.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := enat.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := ordinal.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := cardinal.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := string.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := char.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @fin.decidable_linear_order (?x_179 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := rat.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := pnat.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @list.decidable_linear_order (?x_180 J a b) (?x_181 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @with_top.decidable_linear_order (?x_182 J a b) (?x_183 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @with_bot.decidable_linear_order (?x_184 J a b) (?x_185 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @subtype.decidable_linear_order (?x_186 J a b) (?x_187 J a b) (?x_188 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @order_dual.decidable_linear_order (?x_189 J a b) (?x_190 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := bool.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := int.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := nat.decidable_linear_order
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @conditionally_complete_linear_order_bot.to_decidable_linear_order (?x_191 J a b) (?x_192 J a b)
[class_instances] (6) ?x_192 J a b : conditionally_complete_linear_order_bot J := nnreal.conditionally_complete_linear_order_bot
failed is_def_eq
[class_instances] (6) ?x_192 J a b : conditionally_complete_linear_order_bot J := nat.conditionally_complete_linear_order_bot
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → conditionally_complete_linear_order_bot J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @conditionally_complete_linear_order.to_decidable_linear_order (?x_169 J a b) (?x_170 J a b)
[class_instances] (6) ?x_170 J a b : conditionally_complete_linear_order J := real.conditionally_complete_linear_order
failed is_def_eq
[class_instances] (6) ?x_170 J a b : conditionally_complete_linear_order J := @order_dual.conditionally_complete_linear_order (?x_171 J a b) (?x_172 J a b)
failed is_def_eq
[class_instances] (6) ?x_170 J a b : conditionally_complete_linear_order J := @conditionally_complete_linear_order_of_complete_linear_order (?x_173 J a b) (?x_174 J a b)
[class_instances] (7) ?x_174 J a b : complete_linear_order J := ennreal.complete_linear_order
failed is_def_eq
[class_instances] (7) ?x_174 J a b : complete_linear_order J := enat.complete_linear_order
failed is_def_eq
[class_instances] (7) ?x_174 J a b : complete_linear_order J := @with_top.complete_linear_order (?x_175 J a b) (?x_176 J a b)
failed is_def_eq
[class_instances] (7) ?x_174 J a b : complete_linear_order J := @order_dual.complete_linear_order (?x_177 J a b) (?x_178 J a b)
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → complete_linear_order J
[class_instances] caching failure for Π (J : Type v), J → J → conditionally_complete_linear_order J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @complete_linear_order.to_decidable_linear_order (?x_169 J a b) (?x_170 J a b)
[class_instances] cached failure for Π (J : Type v), J → J → complete_linear_order J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @decidable_linear_ordered_semiring.to_decidable_linear_order (?x_169 J a b) (?x_170 J a b)
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := @zsqrtd.decidable_linear_ordered_semiring (?x_171 J a b) _
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := num.decidable_linear_ordered_semiring
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := real.decidable_linear_ordered_semiring
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := rat.decidable_linear_ordered_semiring
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := nat.decidable_linear_ordered_semiring
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_semiring J := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring (?x_173 J a b) (?x_174 J a b)
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := @zsqrtd.decidable_linear_ordered_comm_ring (?x_175 J a b) _
failed is_def_eq
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := znum.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := real.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_174 J a b : decidable_linear_ordered_comm_ring J := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_177 J a b) (?x_178 J a b)
[class_instances] (8) ?x_178 J a b : discrete_linear_ordered_field J := hyperreal.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (8) ?x_178 J a b : discrete_linear_ordered_field J := real.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (8) ?x_178 J a b : discrete_linear_ordered_field J := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → discrete_linear_ordered_field J
[class_instances] caching failure for Π (J : Type v), J → J → decidable_linear_ordered_comm_ring J
[class_instances] caching failure for Π (J : Type v), J → J → decidable_linear_ordered_semiring J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @additive.decidable_linear_order (?x_169 J a b) (?x_170 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @multiplicative.decidable_linear_order (?x_171 J a b) (?x_172 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @decidable_linear_ordered_add_comm_group.to_decidable_linear_order (?x_173 J a b) (?x_174 J a b)
[class_instances] (6) ?x_174 J a b : decidable_linear_ordered_add_comm_group J := real.decidable_linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_174 J a b : decidable_linear_ordered_add_comm_group J := rat.decidable_linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_174 J a b : decidable_linear_ordered_add_comm_group J := int.decidable_linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_174 J a b : decidable_linear_ordered_add_comm_group J := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_add_comm_group (?x_175 J a b) (?x_176 J a b)
[class_instances] cached failure for Π (J : Type v), J → J → decidable_linear_ordered_comm_ring J
[class_instances] caching failure for Π (J : Type v), J → J → decidable_linear_ordered_add_comm_group J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @decidable_linear_ordered_cancel_add_comm_monoid.to_decidable_linear_order (?x_169 J a b) (?x_170 J a b)
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_cancel_add_comm_monoid J := punit.decidable_linear_ordered_cancel_add_comm_monoid
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_cancel_add_comm_monoid J := nat.decidable_linear_ordered_cancel_add_comm_monoid
failed is_def_eq
[class_instances] (6) ?x_170 J a b : decidable_linear_ordered_cancel_add_comm_monoid J := @decidable_linear_ordered_add_comm_group.to_decidable_linear_ordered_cancel_add_comm_monoid (?x_171 J a b)
(?x_172 J a b)
[class_instances] cached failure for Π (J : Type v), J → J → decidable_linear_ordered_add_comm_group J
[class_instances] caching failure for Π (J : Type v), J → J → decidable_linear_ordered_cancel_add_comm_monoid J
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @canonically_linear_ordered_add_monoid.to_decidable_linear_order (?x_169 J a b) (?x_170 J a b)
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @with_zero.decidable_linear_order (?x_169 J a b) (?x_170 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @add_units.decidable_linear_order (?x_171 J a b) (?x_172 J a b) (?x_173 J a b)
failed is_def_eq
[class_instances] (5) ?x_166 J a b : decidable_linear_order J := @units.decidable_linear_order (?x_174 J a b) (?x_175 J a b) (?x_176 J a b)
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → decidable_linear_order J
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @has_le.le.decidable (?x_165 J a b) (?x_166 J a b) (?x_167 J a b) (?x_168 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @has_lt.lt.decidable (?x_169 J a b) (?x_170 J a b) (?x_171 J a b) (?x_172 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @decidable_eq_of_decidable_le (?x_173 J a b) (?x_174 J a b) (?x_175 J a b) (?x_176 J a b) (?x_177 J a b)
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.ring2.horner_expr.decidable_eq (?x_178 J a b a_1 b_1) (?x_179 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := side.decidable_eq (?x_180 J a b a_1 b_1) (?x_181 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nonote.decidable_lt (?x_182 J a b a_1 b_1) (?x_183 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nonote.decidable_eq (?x_184 J a b a_1 b_1) (?x_185 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := onote.decidable_NF (?x_186 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := onote.decidable_top_below (?x_187 J a b a_1 b_1) (?x_188 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := onote.decidable_eq (?x_189 J a b a_1 b_1) (?x_190 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finsets.decidable_eq (?x_191 J a b a_1 b_1) (?x_192 J a b a_1 b_1) (?x_193 J a b a_1 b_1) (?x_194 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lists.mem.decidable (?x_195 J a b a_1 b_1) (?x_196 J a b a_1 b_1) (?x_197 J a b a_1 b_1) (?x_198 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lists.subset.decidable (?x_199 J a b a_1 b_1) (?x_200 J a b a_1 b_1) (?x_201 J a b a_1 b_1) (?x_202 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lists.equiv.decidable (?x_203 J a b a_1 b_1) (?x_204 J a b a_1 b_1) (?x_205 J a b a_1 b_1) (?x_206 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lists.decidable_eq (?x_207 J a b a_1 b_1) (?x_208 J a b a_1 b_1) (?x_209 J a b a_1 b_1) (?x_210 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lists'.decidable_eq (?x_211 J a b a_1 b_1) (?x_212 J a b a_1 b_1) (?x_213 J a b a_1 b_1) (?x_214 J a b a_1 b_1)
(?x_215 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @pgame.equiv_decidable (?x_216 J a b a_1 b_1) (?x_217 J a b a_1 b_1) (?x_218 J a b a_1 b_1) (?x_219 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @pgame.lt_decidable (?x_220 J a b a_1 b_1) (?x_221 J a b a_1 b_1) (?x_222 J a b a_1 b_1) (?x_223 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @pgame.le_decidable (?x_224 J a b a_1 b_1) (?x_225 J a b a_1 b_1) (?x_226 J a b a_1 b_1) (?x_227 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lex.decidable_eq (?x_228 J a b a_1 b_1) (?x_229 J a b a_1 b_1) (?x_230 J a b a_1 b_1) (?x_231 J a b a_1 b_1)
(?x_232 J a b a_1 b_1)
(?x_233 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := lucas_lehmer.X.decidable_eq (?x_234 J a b a_1 b_1) (?x_235 J a b a_1 b_1) (?x_236 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := lucas_lehmer.lucas_lehmer_test.decidable_pred (?x_237 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @decidable_list_all (?x_238 J a b a_1 b_1) (?x_239 J a b a_1 b_1) (?x_240 J a b a_1 b_1) (?x_241 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @uchange.decidable_eq (?x_242 J a b a_1 b_1) (?x_243 J a b a_1 b_1) (?x_244 J a b a_1 b_1) (?x_245 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @semidirect_product.decidable_eq (?x_246 J a b a_1 b_1) (?x_247 J a b a_1 b_1) (?x_248 J a b a_1 b_1)
(?x_249 J a b a_1 b_1)
(?x_250 J a b a_1 b_1)
(?x_251 J a b a_1 b_1)
(?x_252 J a b a_1 b_1)
(?x_253 J a b a_1 b_1)
(?x_254 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_258 J a b a_1 b_1).decidable_rel (?x_259 J a b a_1 b_1) (?x_260 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @mv_polynomial.decidable_restrict_degree (?x_261 J a b a_1 b_1) (?x_262 J a b a_1 b_1) (?x_263 J a b a_1 b_1)
(?x_264 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @adjoin_root.decidable_eq (?x_265 J a b a_1 b_1) (?x_266 J a b a_1 b_1) (?x_267 J a b a_1 b_1) (?x_268 J a b a_1 b_1)
(?x_269 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @function.is_periodic_pt.decidable (?x_270 J a b a_1 b_1) (?x_271 J a b a_1 b_1) (?x_272 J a b a_1 b_1)
(?x_273 J a b a_1 b_1)
(?x_274 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_276 J a b a_1 b_1).decidable_le (?x_277 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_279 J a b a_1 b_1).decidable_nonneg
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := zsqrtd.decidable_nonnegg (?x_280 J a b a_1 b_1) (?x_281 J a b a_1 b_1) (?x_282 J a b a_1 b_1) (?x_283 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @zsqrtd.decidable_eq (?x_284 J a b a_1 b_1) (?x_285 J a b a_1 b_1) (?x_286 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := zmod.decidable_eq (?x_287 J a b a_1 b_1) (?x_288 J a b a_1 b_1) (?x_289 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @sym2.is_diag.decidable_pred (?x_290 J a b a_1 b_1) (?x_291 J a b a_1 b_1) (?x_292 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := irrational.decidable (?x_293 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := num.decidable_prime (?x_294 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos_num.decidable_prime (?x_295 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @lazy_list.decidable_eq (?x_296 J a b a_1 b_1) (?x_297 J a b a_1 b_1) (?x_298 J a b a_1 b_1) (?x_299 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @thunk.decidable_eq (?x_300 J a b a_1 b_1) (?x_301 J a b a_1 b_1) (?x_302 J a b a_1 b_1) (?x_303 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := int.decidable_pred (?x_304 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fp.dec_valid_finite (?x_305 J a b a_1 b_1) (?x_306 J a b a_1 b_1) (?x_307 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finmap.decidable_rel (?x_308 J a b a_1 b_1) (?x_309 J a b a_1 b_1) (?x_310 J a b a_1 b_1) (?x_311 J a b a_1 b_1)
(?x_312 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finmap.decidable (?x_313 J a b a_1 b_1) (?x_314 J a b a_1 b_1) (?x_315 J a b a_1 b_1) (?x_316 J a b a_1 b_1)
(?x_317 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finmap.has_decidable_eq (?x_318 J a b a_1 b_1) (?x_319 J a b a_1 b_1) (?x_320 J a b a_1 b_1) (?x_321 J a b a_1 b_1)
(?x_322 J a b a_1 b_1)
(?x_323 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @alist.decidable (?x_324 J a b a_1 b_1) (?x_325 J a b a_1 b_1) (?x_326 J a b a_1 b_1) (?x_327 J a b a_1 b_1)
(?x_328 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @alist.decidable_eq (?x_329 J a b a_1 b_1) (?x_330 J a b a_1 b_1) (?x_331 J a b a_1 b_1) (?x_332 J a b a_1 b_1)
(?x_333 J a b a_1 b_1)
(?x_334 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @buffer.decidable_eq (?x_335 J a b a_1 b_1) (?x_336 J a b a_1 b_1) (?x_337 J a b a_1 b_1) (?x_338 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := turing.partrec_to_TM2.K'.decidable_eq (?x_339 J a b a_1 b_1) (?x_340 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := turing.partrec_to_TM2.Γ'.decidable_eq (?x_341 J a b a_1 b_1) (?x_342 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := znum.decidable_rel (?x_343 J a b a_1 b_1) (?x_344 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos_num.decidable_dvd (?x_345 J a b a_1 b_1) (?x_346 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := num.decidable_dvd (?x_347 J a b a_1 b_1) (?x_348 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := snum.decidable_eq (?x_349 J a b a_1 b_1) (?x_350 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nzsnum.decidable_eq (?x_351 J a b a_1 b_1) (?x_352 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @bitvec.ugt.decidable (?x_353 J a b a_1 b_1) (?x_354 J a b a_1 b_1) (?x_355 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @bitvec.ult.decidable (?x_356 J a b a_1 b_1) (?x_357 J a b a_1 b_1) (?x_358 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := turing.dir.decidable_eq (?x_359 J a b a_1 b_1) (?x_360 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := expr_lens.dir.decidable_eq (?x_361 J a b a_1 b_1) (?x_362 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nat.decidable_pred (?x_363 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := complex.decidable_eq (?x_364 J a b a_1 b_1) (?x_365 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_366 J a b a_1 b_1).decidable_eq (?x_367 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_368 J a b a_1 b_1).decidable_le (?x_369 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_370 J a b a_1 b_1).decidable_lt (?x_371 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.decl_reducibility.decidable_eq (?x_372 J a b a_1 b_1) (?x_373 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_add_semigroup.decidable_eq (?x_374 J a b a_1 b_1) (?x_375 J a b a_1 b_1) (?x_376 J a b a_1 b_1)
(?x_377 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_semigroup.decidable_eq (?x_378 J a b a_1 b_1) (?x_379 J a b a_1 b_1) (?x_380 J a b a_1 b_1) (?x_381 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_add_magma.decidable_eq (?x_382 J a b a_1 b_1) (?x_383 J a b a_1 b_1) (?x_384 J a b a_1 b_1) (?x_385 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_magma.decidable_eq (?x_386 J a b a_1 b_1) (?x_387 J a b a_1 b_1) (?x_388 J a b a_1 b_1) (?x_389 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_391 J a b a_1 b_1).terminated_at_decidable (?x_392 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_394 J a b a_1 b_1).terminated_at_decidable (?x_395 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @dfinsupp.decidable_eq (?x_396 J a b a_1 b_1) (?x_397 J a b a_1 b_1) (?x_398 J a b a_1 b_1) (?x_399 J a b a_1 b_1)
(?x_400 J a b a_1 b_1)
(?x_401 J a b a_1 b_1)
(?x_402 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @dfinsupp.decidable_zero (?x_403 J a b a_1 b_1) (?x_404 J a b a_1 b_1) (?x_405 J a b a_1 b_1) (?x_406 J a b a_1 b_1)
(?x_407 J a b a_1 b_1)
(?x_408 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @matrix.decidable_rel (?x_409 J a b a_1 b_1) (?x_410 J a b a_1 b_1) (?x_411 J a b a_1 b_1) (?x_412 J a b a_1 b_1)
(?x_413 J a b a_1 b_1)
(?x_414 J a b a_1 b_1)
(?x_415 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @decidable_gpowers (?x_416 J a b a_1 b_1) (?x_417 J a b a_1 b_1) (?x_418 J a b a_1 b_1) (?x_419 J a b a_1 b_1)
(?x_420 J a b a_1 b_1)
(?x_421 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := multiplicity.decidable_int (?x_422 J a b a_1 b_1) (?x_423 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := multiplicity.decidable_nat (?x_424 J a b a_1 b_1) (?x_425 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := enat.decidable (?x_426 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @roption.of_option_decidable (?x_427 J a b a_1 b_1) (?x_428 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @roption.some_decidable (?x_429 J a b a_1 b_1) (?x_430 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @roption.none_decidable (?x_431 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @function.is_fixed_pt.decidable (?x_432 J a b a_1 b_1) (?x_433 J a b a_1 b_1) (?x_434 J a b a_1 b_1)
(?x_435 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @int.modeq.decidable (?x_436 J a b a_1 b_1) (?x_437 J a b a_1 b_1) (?x_438 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nat.modeq.decidable (?x_439 J a b a_1 b_1) (?x_440 J a b a_1 b_1) (?x_441 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_group.red.decidable_rel (?x_442 J a b a_1 b_1) (?x_443 J a b a_1 b_1) (?x_444 J a b a_1 b_1)
(?x_445 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @free_group.decidable_eq (?x_446 J a b a_1 b_1) (?x_447 J a b a_1 b_1) (?x_448 J a b a_1 b_1) (?x_449 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fin_category.decidable_eq_hom (?x_450 J a b a_1 b_1) (?x_451 J a b a_1 b_1) (?x_452 J a b a_1 b_1)
(?x_453 J a b a_1 b_1)
(?x_454 J a b a_1 b_1)
(?x_455 J a b a_1 b_1)
(?x_456 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fin_category.decidable_eq_obj (?x_457 J a b a_1 b_1) (?x_458 J a b a_1 b_1) (?x_459 J a b a_1 b_1)
(?x_460 J a b a_1 b_1)
(?x_461 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @limits.wide_pushout_shape.hom.decidable_eq (?x_462 J a b a_1 b_1) (?x_463 J a b a_1 b_1) (?x_464 J a b a_1 b_1)
(?x_465 J a b a_1 b_1)
(?x_466 J a b a_1 b_1)
(?x_467 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @limits.wide_pullback_shape.hom.decidable_eq (?x_468 J a b a_1 b_1) (?x_469 J a b a_1 b_1) (?x_470 J a b a_1 b_1)
(?x_471 J a b a_1 b_1)
(?x_472 J a b a_1 b_1)
(?x_473 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @mv_polynomial.decidable_eq_mv_polynomial (?x_474 J a b a_1 b_1) (?x_475 J a b a_1 b_1) (?x_476 J a b a_1 b_1)
(?x_477 J a b a_1 b_1)
(?x_478 J a b a_1 b_1)
(?x_479 J a b a_1 b_1)
(?x_480 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := omega.nat.preterm.decidable_eq (?x_481 J a b a_1 b_1) (?x_482 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @polynomial.decidable (?x_483 J a b a_1 b_1) (?x_484 J a b a_1 b_1) (?x_485 J a b a_1 b_1) (?x_486 J a b a_1 b_1)
(?x_487 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @polynomial.monic.decidable (?x_488 J a b a_1 b_1) (?x_489 J a b a_1 b_1) (?x_490 J a b a_1 b_1) (?x_491 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := string.decidable_le (?x_492 J a b a_1 b_1) (?x_493 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := string.decidable_lt (?x_494 J a b a_1 b_1) (?x_495 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.ring_exp.ex_type.decidable_eq (?x_496 J a b a_1 b_1) (?x_497 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.ring_exp.coeff.decidable_eq (?x_498 J a b a_1 b_1) (?x_499 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @add_con.decidable_eq (?x_500 J a b a_1 b_1) (?x_501 J a b a_1 b_1) (?x_502 J a b a_1 b_1) (?x_503 J a b a_1 b_1)
(?x_504 J a b a_1 b_1)
(?x_505 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @con.decidable_eq (?x_506 J a b a_1 b_1) (?x_507 J a b a_1 b_1) (?x_508 J a b a_1 b_1) (?x_509 J a b a_1 b_1)
(?x_510 J a b a_1 b_1)
(?x_511 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := finsupp.decidable_le (?x_512 J a b a_1 b_1) (?x_513 J a b a_1 b_1) (?x_514 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finsupp.finsupp.decidable_eq (?x_515 J a b a_1 b_1) (?x_516 J a b a_1 b_1) (?x_517 J a b a_1 b_1)
(?x_518 J a b a_1 b_1)
(?x_519 J a b a_1 b_1)
(?x_520 J a b a_1 b_1)
(?x_521 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := limits.walking_parallel_pair_hom.decidable_eq (?x_522 J a b a_1 b_1) (?x_523 J a b a_1 b_1) (?x_524 J a b a_1 b_1)
(?x_525 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := limits.walking_parallel_pair.decidable_eq (?x_526 J a b a_1 b_1) (?x_527 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := limits.walking_pair.decidable_eq (?x_528 J a b a_1 b_1) (?x_529 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_right_inverse_fintype (?x_530 J a b a_1 b_1) (?x_531 J a b a_1 b_1) (?x_532 J a b a_1 b_1)
(?x_533 J a b a_1 b_1)
(?x_534 J a b a_1 b_1)
(?x_535 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_left_inverse_fintype (?x_536 J a b a_1 b_1) (?x_537 J a b a_1 b_1) (?x_538 J a b a_1 b_1)
(?x_539 J a b a_1 b_1)
(?x_540 J a b a_1 b_1)
(?x_541 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_bijective_fintype (?x_542 J a b a_1 b_1) (?x_543 J a b a_1 b_1) (?x_544 J a b a_1 b_1)
(?x_545 J a b a_1 b_1)
(?x_546 J a b a_1 b_1)
(?x_547 J a b a_1 b_1)
(?x_548 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_surjective_fintype (?x_549 J a b a_1 b_1) (?x_550 J a b a_1 b_1) (?x_551 J a b a_1 b_1)
(?x_552 J a b a_1 b_1)
(?x_553 J a b a_1 b_1)
(?x_554 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_injective_fintype (?x_555 J a b a_1 b_1) (?x_556 J a b a_1 b_1) (?x_557 J a b a_1 b_1)
(?x_558 J a b a_1 b_1)
(?x_559 J a b a_1 b_1)
(?x_560 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_eq_equiv_fintype (?x_561 J a b a_1 b_1) (?x_562 J a b a_1 b_1) (?x_563 J a b a_1 b_1)
(?x_564 J a b a_1 b_1)
(?x_565 J a b a_1 b_1)
(?x_566 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_exists_fintype (?x_567 J a b a_1 b_1) (?x_568 J a b a_1 b_1) (?x_569 J a b a_1 b_1)
(?x_570 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_forall_fintype (?x_571 J a b a_1 b_1) (?x_572 J a b a_1 b_1) (?x_573 J a b a_1 b_1)
(?x_574 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fintype.decidable_pi_fintype (?x_575 J a b a_1 b_1) (?x_576 J a b a_1 b_1) (?x_577 J a b a_1 b_1)
(?x_578 J a b a_1 b_1)
(?x_579 J a b a_1 b_1)
(?x_580 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @vector.decidable_eq (?x_581 J a b a_1 b_1) (?x_582 J a b a_1 b_1) (?x_583 J a b a_1 b_1) (?x_584 J a b a_1 b_1)
(?x_585 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_588 J a b a_1 b_1).decidable_disjoint (?x_589 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.decidable_dexists_finset (?x_590 J a b a_1 b_1) (?x_591 J a b a_1 b_1) (?x_592 J a b a_1 b_1)
(?x_593 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.decidable_eq_pi_finset (?x_594 J a b a_1 b_1) (?x_595 J a b a_1 b_1) (?x_596 J a b a_1 b_1)
(?x_597 J a b a_1 b_1)
(?x_598 J a b a_1 b_1)
(?x_599 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.decidable_dforall_finset (?x_600 J a b a_1 b_1) (?x_601 J a b a_1 b_1) (?x_602 J a b a_1 b_1)
(?x_603 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.decidable_mem' (?x_604 J a b a_1 b_1) (?x_605 J a b a_1 b_1) (?x_606 J a b a_1 b_1) (?x_607 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.decidable_mem (?x_608 J a b a_1 b_1) (?x_609 J a b a_1 b_1) (?x_610 J a b a_1 b_1) (?x_611 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @finset.has_decidable_eq (?x_612 J a b a_1 b_1) (?x_613 J a b a_1 b_1) (?x_614 J a b a_1 b_1) (?x_615 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.interactive.decidable_eq (?x_616 J a b a_1 b_1) (?x_617 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.interactive.mono_selection.decidable_eq (?x_618 J a b a_1 b_1) (?x_619 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_622 J a b a_1 b_1).nodup_decidable
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @multiset.decidable_dexists_multiset (?x_623 J a b a_1 b_1) (?x_624 J a b a_1 b_1) (?x_625 J a b a_1 b_1)
(?x_626 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @multiset.decidable_eq_pi_multiset (?x_627 J a b a_1 b_1) (?x_628 J a b a_1 b_1) (?x_629 J a b a_1 b_1)
(?x_630 J a b a_1 b_1)
(?x_631 J a b a_1 b_1)
(?x_632 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @multiset.decidable_dforall_multiset (?x_633 J a b a_1 b_1) (?x_634 J a b a_1 b_1) (?x_635 J a b a_1 b_1)
(?x_636 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @multiset.decidable_mem (?x_637 J a b a_1 b_1) (?x_638 J a b a_1 b_1) (?x_639 J a b a_1 b_1) (?x_640 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @multiset.has_decidable_eq (?x_641 J a b a_1 b_1) (?x_642 J a b a_1 b_1) (?x_643 J a b a_1 b_1) (?x_644 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @tree.decidable_eq (?x_645 J a b a_1 b_1) (?x_646 J a b a_1 b_1) (?x_647 J a b a_1 b_1) (?x_648 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := znum.decidable_le (?x_649 J a b a_1 b_1) (?x_650 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := znum.decidable_lt (?x_651 J a b a_1 b_1) (?x_652 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := num.decidable_le (?x_653 J a b a_1 b_1) (?x_654 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := num.decidable_lt (?x_655 J a b a_1 b_1) (?x_656 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos_num.decidable_le (?x_657 J a b a_1 b_1) (?x_658 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos_num.decidable_lt (?x_659 J a b a_1 b_1) (?x_660 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := znum.decidable_eq (?x_661 J a b a_1 b_1) (?x_662 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := num.decidable_eq (?x_663 J a b a_1 b_1) (?x_664 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos_num.decidable_eq (?x_665 J a b a_1 b_1) (?x_666 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := linarith.ineq.decidable_eq (?x_667 J a b a_1 b_1) (?x_668 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @int.decidable_lt_le (?x_669 J a b a_1 b_1) (?x_670 J a b a_1 b_1) (?x_671 J a b a_1 b_1) (?x_672 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @int.decidable_lt_lt (?x_673 J a b a_1 b_1) (?x_674 J a b a_1 b_1) (?x_675 J a b a_1 b_1) (?x_676 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @int.decidable_le_le (?x_677 J a b a_1 b_1) (?x_678 J a b a_1 b_1) (?x_679 J a b a_1 b_1) (?x_680 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @int.decidable_le_lt (?x_681 J a b a_1 b_1) (?x_682 J a b a_1 b_1) (?x_683 J a b a_1 b_1) (?x_684 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := rat.decidable_le (?x_685 J a b a_1 b_1) (?x_686 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_687 J a b a_1 b_1).decidable_nonneg
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := rat.decidable_eq (?x_688 J a b a_1 b_1) (?x_689 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @ulower.decidable_eq (?x_690 J a b a_1 b_1) (?x_691 J a b a_1 b_1) (?x_692 J a b a_1 b_1) (?x_693 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @psigma.decidable_eq (?x_694 J a b a_1 b_1) (?x_695 J a b a_1 b_1) (?x_696 J a b a_1 b_1) (?x_697 J a b a_1 b_1)
(?x_698 J a b a_1 b_1)
(?x_699 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @sigma.decidable_eq (?x_700 J a b a_1 b_1) (?x_701 J a b a_1 b_1) (?x_702 J a b a_1 b_1) (?x_703 J a b a_1 b_1)
(?x_704 J a b a_1 b_1)
(?x_705 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pnat.decidable_eq (?x_706 J a b a_1 b_1) (?x_707 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_708 J a b a_1 b_1).decidable_prime
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_711 J a b a_1 b_1).decidable_perm (?x_712 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_713 J a b a_1 b_1).decidable (?x_714 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := int.decidable_dvd (?x_715 J a b a_1 b_1) (?x_716 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_719 J a b a_1 b_1).decidable_infix (?x_720 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_723 J a b a_1 b_1).decidable_suffix (?x_724 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_727 J a b a_1 b_1).decidable_prefix (?x_728 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_732 J a b a_1 b_1).decidable_exists_mem
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.lex.decidable_rel (?x_733 J a b a_1 b_1) (?x_734 J a b a_1 b_1) (?x_735 J a b a_1 b_1) (?x_736 J a b a_1 b_1)
(?x_737 J a b a_1 b_1)
(?x_738 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_741 J a b a_1 b_1).decidable_sublist (?x_742 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @nat.decidable_lo_hi_le (?x_743 J a b a_1 b_1) (?x_744 J a b a_1 b_1) (?x_745 J a b a_1 b_1) (?x_746 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @nat.decidable_lo_hi (?x_747 J a b a_1 b_1) (?x_748 J a b a_1 b_1) (?x_749 J a b a_1 b_1) (?x_750 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @nat.decidable_ball_le (?x_751 J a b a_1 b_1) (?x_752 J a b a_1 b_1) (?x_753 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @nat.decidable_forall_fin (?x_754 J a b a_1 b_1) (?x_755 J a b a_1 b_1) (?x_756 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @nat.decidable_ball_lt (?x_757 J a b a_1 b_1) (?x_758 J a b a_1 b_1) (?x_759 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @plift.decidable_eq (?x_760 J a b a_1 b_1) (?x_761 J a b a_1 b_1) (?x_762 J a b a_1 b_1) (?x_763 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @ulift.decidable_eq (?x_764 J a b a_1 b_1) (?x_765 J a b a_1 b_1) (?x_766 J a b a_1 b_1) (?x_767 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @set.univ_decidable (?x_768 J a b a_1 b_1) (?x_769 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @set.decidable_set_of (?x_770 J a b a_1 b_1) (?x_771 J a b a_1 b_1) (?x_772 J a b a_1 b_1) (?x_773 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @set.decidable_mem (?x_774 J a b a_1 b_1) (?x_775 J a b a_1 b_1) (?x_776 J a b a_1 b_1) (?x_777 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @with_bot.decidable_lt (?x_778 J a b a_1 b_1) (?x_779 J a b a_1 b_1) (?x_780 J a b a_1 b_1) (?x_781 J a b a_1 b_1)
(?x_782 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @order.preimage.decidable (?x_783 J a b a_1 b_1) (?x_784 J a b a_1 b_1) (?x_785 J a b a_1 b_1) (?x_786 J a b a_1 b_1)
(?x_787 J a b a_1 b_1)
(?x_788 J a b a_1 b_1)
(?x_789 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @prod.lex.decidable (?x_790 J a b a_1 b_1) (?x_791 J a b a_1 b_1) (?x_792 J a b a_1 b_1) (?x_793 J a b a_1 b_1)
(?x_794 J a b a_1 b_1)
(?x_795 J a b a_1 b_1)
(?x_796 J a b a_1 b_1)
(?x_797 J a b a_1 b_1)
(?x_798 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @add_units.decidable_eq (?x_799 J a b a_1 b_1) (?x_800 J a b a_1 b_1) (?x_801 J a b a_1 b_1) (?x_802 J a b a_1 b_1)
(?x_803 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @units.decidable_eq (?x_804 J a b a_1 b_1) (?x_805 J a b a_1 b_1) (?x_806 J a b a_1 b_1) (?x_807 J a b a_1 b_1)
(?x_808 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.suggest.head_symbol_match.decidable_eq (?x_809 J a b a_1 b_1) (?x_810 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.simp_arg_type.decidable_eq (?x_811 J a b a_1 b_1) (?x_812 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @function.decidable_eq_pfun (?x_813 J a b a_1 b_1) (?x_814 J a b a_1 b_1) (?x_815 J a b a_1 b_1) (?x_816 J a b a_1 b_1)
(?x_817 J a b a_1 b_1)
(?x_818 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @sum.decidable_eq (?x_819 J a b a_1 b_1) (?x_820 J a b a_1 b_1) (?x_821 J a b a_1 b_1) (?x_822 J a b a_1 b_1)
(?x_823 J a b a_1 b_1)
(?x_824 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := norm_cast.label.decidable_eq (?x_825 J a b a_1 b_1) (?x_826 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := auto.case_option.decidable_eq (?x_827 J a b a_1 b_1) (?x_828 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := auto.auto_config.decidable_eq (?x_829 J a b a_1 b_1) (?x_830 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := lint_verbosity.decidable_eq (?x_831 J a b a_1 b_1) (?x_832 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.transparency.decidable_eq (?x_833 J a b a_1 b_1) (?x_834 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := widget_override.local_collection.decidable_eq (?x_835 J a b a_1 b_1) (?x_836 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := widget_override.filter_type.decidable_eq (?x_837 J a b a_1 b_1) (?x_838 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @bool.decidable_exists_bool (?x_839 J a b a_1 b_1) (?x_840 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @bool.decidable_forall_bool (?x_841 J a b a_1 b_1) (?x_842 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @pexpr.decidable_eq (?x_843 J a b a_1 b_1) (?x_844 J a b a_1 b_1) (?x_845 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := binder.decidable_eq (?x_846 J a b a_1 b_1) (?x_847 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := congr_arg_kind.decidable_eq (?x_848 J a b a_1 b_1) (?x_849 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := binder_info.decidable_eq (?x_850 J a b a_1 b_1) (?x_851 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_854 J a b a_1 b_1).nodup_decidable
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_858 J a b a_1 b_1).decidable_chain'
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.decidable_chain (?x_859 J a b a_1 b_1) (?x_860 J a b a_1 b_1) (?x_861 J a b a_1 b_1) (?x_862 J a b a_1 b_1)
(?x_863 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_867 J a b a_1 b_1).decidable_pairwise
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pempty.decidable_eq (?x_868 J a b a_1 b_1) (?x_869 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := empty.decidable_eq (?x_870 J a b a_1 b_1) (?x_871 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := doc_category.decidable_eq (?x_872 J a b a_1 b_1) (?x_873 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_877 J a b a_1 b_1).decidable_exists_mem
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_881 J a b a_1 b_1).decidable_forall_mem
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := native.float.dec_eq (?x_882 J a b a_1 b_1) (?x_883 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := native.float.decidable_le (?x_884 J a b a_1 b_1) (?x_885 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := native.float.decidable_lt (?x_886 J a b a_1 b_1) (?x_887 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := rbnode.color.decidable_eq (?x_888 J a b a_1 b_1) (?x_889 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @array.decidable_eq (?x_890 J a b a_1 b_1) (?x_891 J a b a_1 b_1) (?x_892 J a b a_1 b_1) (?x_893 J a b a_1 b_1)
(?x_894 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @d_array.decidable_eq (?x_895 J a b a_1 b_1) (?x_896 J a b a_1 b_1) (?x_897 J a b a_1 b_1) (?x_898 J a b a_1 b_1)
(?x_899 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @subtype.decidable_eq (?x_900 J a b a_1 b_1) (?x_901 J a b a_1 b_1) (?x_902 J a b a_1 b_1) (?x_903 J a b a_1 b_1)
(?x_904 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_punctuation (?x_905 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_alphanum (?x_906 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_digit (?x_907 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_alpha (?x_908 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_lower (?x_909 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_upper (?x_910 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_is_whitespace (?x_911 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_912 J a b a_1 b_1).decidable_lt (?x_913 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_914 J a b a_1 b_1).decidable_le (?x_915 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := int.decidable_eq (?x_916 J a b a_1 b_1) (?x_917 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.decidable_ball (?x_918 J a b a_1 b_1) (?x_919 J a b a_1 b_1) (?x_920 J a b a_1 b_1) (?x_921 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.decidable_bex (?x_922 J a b a_1 b_1) (?x_923 J a b a_1 b_1) (?x_924 J a b a_1 b_1) (?x_925 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nat.decidable_dvd (?x_926 J a b a_1 b_1) (?x_927 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := widget.local_collection.decidable_eq (?x_928 J a b a_1 b_1) (?x_929 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := widget.filter_type.decidable_eq (?x_930 J a b a_1 b_1) (?x_931 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := expr.address.has_dec_eq (?x_932 J a b a_1 b_1) (?x_933 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := expr.coord.has_dec_eq (?x_934 J a b a_1 b_1) (?x_935 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @local_context.decidable (?x_936 J a b a_1 b_1) (?x_937 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := local_context.decidable_rel (?x_938 J a b a_1 b_1) (?x_939 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := local_context.has_decidable_eq (?x_940 J a b a_1 b_1) (?x_941 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := vm_obj_kind.decidable_eq (?x_942 J a b a_1 b_1) (?x_943 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := tactic.binder_info.has_decidable_eq (?x_944 J a b a_1 b_1) (?x_945 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := punit.decidable_eq (?x_946 J a b a_1 b_1) (?x_947 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := expr.decidable_rel (?x_948 J a b a_1 b_1) (?x_949 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := expr.has_decidable_eq (?x_950 J a b a_1 b_1) (?x_951 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := pos.decidable_eq (?x_952 J a b a_1 b_1) (?x_953 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := level.has_decidable_eq (?x_954 J a b a_1 b_1) (?x_955 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := options.has_decidable_eq (?x_956 J a b a_1 b_1) (?x_957 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @option.decidable_eq (?x_958 J a b a_1 b_1) (?x_959 J a b a_1 b_1) (?x_960 J a b a_1 b_1) (?x_961 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := name.has_decidable_eq (?x_962 J a b a_1 b_1) (?x_963 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := name.lt.decidable_rel (?x_964 J a b a_1 b_1) (?x_965 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := coe_decidable_eq (?x_966 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := ordering.decidable_eq (?x_967 J a b a_1 b_1) (?x_968 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := unsigned.decidable_eq (?x_969 J a b a_1 b_1) (?x_970 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := fin.decidable_eq (?x_971 J a b a_1 b_1) (?x_972 J a b a_1 b_1) (?x_973 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_975 J a b a_1 b_1).decidable_le (?x_976 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_978 J a b a_1 b_1).decidable_lt (?x_979 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := string.has_decidable_eq (?x_980 J a b a_1 b_1) (?x_981 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_982 J a b a_1 b_1).has_decidable_lt (?x_983 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := char.decidable_eq (?x_984 J a b a_1 b_1) (?x_985 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_986 J a b a_1 b_1).decidable_le (?x_987 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_988 J a b a_1 b_1).decidable_lt (?x_989 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_993 J a b a_1 b_1).has_decidable_le (?x_994 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_998 J a b a_1 b_1).has_decidable_lt (?x_999 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.decidable_mem (?x_1000 J a b a_1 b_1) (?x_1001 J a b a_1 b_1) (?x_1002 J a b a_1 b_1) (?x_1003 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @list.decidable_eq (?x_1004 J a b a_1 b_1) (?x_1005 J a b a_1 b_1) (?x_1006 J a b a_1 b_1) (?x_1007 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @quotient.decidable_eq (?x_1008 J a b a_1 b_1) (?x_1009 J a b a_1 b_1) (?x_1010 J a b a_1 b_1) (?x_1011 J a b a_1 b_1)
(?x_1012 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_1013 J a b a_1 b_1).decidable_lt (?x_1014 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_1015 J a b a_1 b_1).decidable_le (?x_1016 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := nat.decidable_eq (?x_1017 J a b a_1 b_1) (?x_1018 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @prod_has_decidable_lt (?x_1019 J a b a_1 b_1) (?x_1020 J a b a_1 b_1) (?x_1021 J a b a_1 b_1) (?x_1022 J a b a_1 b_1)
(?x_1023 J a b a_1 b_1)
(?x_1024 J a b a_1 b_1)
(?x_1025 J a b a_1 b_1)
(?x_1026 J a b a_1 b_1)
(?x_1027 J a b a_1 b_1)
(?x_1028 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @prod.decidable_eq (?x_1029 J a b a_1 b_1) (?x_1030 J a b a_1 b_1) (?x_1031 J a b a_1 b_1) (?x_1032 J a b a_1 b_1)
(?x_1033 J a b a_1 b_1)
(?x_1034 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @dite.decidable (?x_1035 J a b a_1 b_1) (?x_1036 J a b a_1 b_1) (?x_1037 J a b a_1 b_1) (?x_1038 J a b a_1 b_1)
(?x_1039 J a b a_1 b_1)
(?x_1040 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @ite.decidable (?x_1041 J a b a_1 b_1) (?x_1042 J a b a_1 b_1) (?x_1043 J a b a_1 b_1) (?x_1044 J a b a_1 b_1)
(?x_1045 J a b a_1 b_1)
(?x_1046 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := bool.decidable_eq (?x_1047 J a b a_1 b_1) (?x_1048 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @ne.decidable (?x_1049 J a b a_1 b_1) (?x_1050 J a b a_1 b_1) (?x_1051 J a b a_1 b_1) (?x_1052 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @forall_prop_decidable (?x_1053 J a b a_1 b_1) (?x_1054 J a b a_1 b_1) (?x_1055 J a b a_1 b_1) (?x_1056 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @exists_prop_decidable (?x_1057 J a b a_1 b_1) (?x_1058 J a b a_1 b_1) (?x_1059 J a b a_1 b_1) (?x_1060 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @xor.decidable (?x_1061 J a b a_1 b_1) (?x_1062 J a b a_1 b_1) (?x_1063 J a b a_1 b_1) (?x_1064 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @iff.decidable (?x_1065 J a b a_1 b_1) (?x_1066 J a b a_1 b_1) (?x_1067 J a b a_1 b_1) (?x_1068 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @implies.decidable (?x_1069 J a b a_1 b_1) (?x_1070 J a b a_1 b_1) (?x_1071 J a b a_1 b_1) (?x_1072 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @not.decidable (?x_1073 J a b a_1 b_1) (?x_1074 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @or.decidable (?x_1075 J a b a_1 b_1) (?x_1076 J a b a_1 b_1) (?x_1077 J a b a_1 b_1) (?x_1078 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @and.decidable (?x_1079 J a b a_1 b_1) (?x_1080 J a b a_1 b_1) (?x_1081 J a b a_1 b_1) (?x_1082 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := decidable.false
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := decidable.true
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := (?x_1086 J a b a_1 b_1).decidable_forall_mem
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @fin_enum.dec_eq (?x_1087 J a b a_1 b_1) (?x_1088 J a b a_1 b_1) (?x_1089 J a b a_1 b_1) (?x_1090 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @eq.decidable (?x_1091 J a b a_1 b_1) (?x_1092 J a b a_1 b_1) (?x_1093 J a b a_1 b_1) (?x_1094 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @has_le.le.decidable (?x_1095 J a b a_1 b_1) (?x_1096 J a b a_1 b_1) (?x_1097 J a b a_1 b_1) (?x_1098 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @has_lt.lt.decidable (?x_1099 J a b a_1 b_1) (?x_1100 J a b a_1 b_1) (?x_1101 J a b a_1 b_1) (?x_1102 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @decidable_eq_of_decidable_le (?x_1103 J a b a_1 b_1) (?x_1104 J a b a_1 b_1) (?x_1105 J a b a_1 b_1)
(?x_1106 J a b a_1 b_1)
(?x_1107 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @decidable_lt_of_decidable_le (?x_1108 J a b a_1 b_1) (?x_1109 J a b a_1 b_1) (?x_1110 J a b a_1 b_1)
(?x_1111 J a b a_1 b_1)
(?x_1112 J a b a_1 b_1)
failed is_def_eq
[class_instances] (5) ?x_175 J a b a_1 b_1 : decidable (a_1 ≤ b_1) := @decidable_eq_of_subsingleton (?x_1113 J a b a_1 b_1) _ (?x_1115 J a b a_1 b_1) (?x_1116 J a b a_1 b_1)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @decidable_lt_of_decidable_le (?x_165 J a b) (?x_166 J a b) (?x_167 J a b) (?x_168 J a b) (?x_169 J a b)
failed is_def_eq
[class_instances] (4) ?x_164 J a b : decidable (a = b) := @decidable_eq_of_subsingleton (?x_170 J a b) _ (?x_172 J a b) (?x_173 J a b)
[class_instances] (5) ?x_171 J a b : subsingleton J := (?x_174 J a b).subsingleton_short
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @zmod.subsingleton_ring_hom (?x_175 J a b) (?x_176 J a b) (?x_177 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := zmod.subsingleton_units
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @sym2.subsingleton (?x_178 J a b) (?x_179 J a b) (?x_180 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @pfunctor.approx.subsingleton (?x_181 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := typevec.subsingleton0
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @category_theory.subsingleton_simple (?x_182 J a b) (?x_183 J a b) (?x_184 J a b) (?x_185 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @invertible.subsingleton (?x_186 J a b) (?x_187 J a b) (?x_188 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @principal_seg.subsingleton (?x_189 J a b) (?x_190 J a b) (?x_191 J a b) (?x_192 J a b) (?x_193 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @initial_seg.subsingleton (?x_194 J a b) (?x_195 J a b) (?x_196 J a b) (?x_197 J a b) (?x_198 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := (?x_199 J a b).subsingleton (?x_200 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := (?x_201 J a b).subsingleton (?x_202 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := (?x_204 J a b).subsingleton_hom (?x_205 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := (?x_207 J a b).subsingleton_hom (?x_208 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := subsingleton_fin_one
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := subsingleton_fin_zero
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @polynomial.subsingleton (?x_209 J a b) (?x_210 J a b) (?x_211 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_colimits_subsingleton (?x_212 J a b) (?x_213 J a b) (?x_214 J a b) (?x_215 J a b) (?x_216 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_limits_subsingleton (?x_217 J a b) (?x_218 J a b) (?x_219 J a b) (?x_220 J a b) (?x_221 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_colimits_of_shape_subsingleton (?x_222 J a b) (?x_223 J a b) (?x_224 J a b) (?x_225 J a b)
(?x_226 J a b)
(?x_227 J a b)
(?x_228 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_limits_of_shape_subsingleton (?x_229 J a b) (?x_230 J a b) (?x_231 J a b) (?x_232 J a b) (?x_233 J a b)
(?x_234 J a b)
(?x_235 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_colimit_subsingleton (?x_236 J a b) (?x_237 J a b) (?x_238 J a b) (?x_239 J a b) (?x_240 J a b)
(?x_241 J a b)
(?x_242 J a b)
(?x_243 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.reflects_limit_subsingleton (?x_244 J a b) (?x_245 J a b) (?x_246 J a b) (?x_247 J a b) (?x_248 J a b)
(?x_249 J a b)
(?x_250 J a b)
(?x_251 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_colimits_subsingleton (?x_252 J a b) (?x_253 J a b) (?x_254 J a b) (?x_255 J a b) (?x_256 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_limits_subsingleton (?x_257 J a b) (?x_258 J a b) (?x_259 J a b) (?x_260 J a b) (?x_261 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_colimits_of_shape_subsingleton (?x_262 J a b) (?x_263 J a b) (?x_264 J a b) (?x_265 J a b)
(?x_266 J a b)
(?x_267 J a b)
(?x_268 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_limits_of_shape_subsingleton (?x_269 J a b) (?x_270 J a b) (?x_271 J a b) (?x_272 J a b)
(?x_273 J a b)
(?x_274 J a b)
(?x_275 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_colimit_subsingleton (?x_276 J a b) (?x_277 J a b) (?x_278 J a b) (?x_279 J a b) (?x_280 J a b)
(?x_281 J a b)
(?x_282 J a b)
(?x_283 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.preserves_limit_subsingleton (?x_284 J a b) (?x_285 J a b) (?x_286 J a b) (?x_287 J a b) (?x_288 J a b)
(?x_289 J a b)
(?x_290 J a b)
(?x_291 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @nat_algebra_subsingleton (?x_292 J a b) (?x_293 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @int_algebra_subsingleton (?x_294 J a b) (?x_295 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @Module.subsingleton (?x_296 J a b) (?x_297 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.has_zero_object.subsingleton (?x_298 J a b) (?x_299 J a b) (?x_300 J a b) (?x_301 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.has_zero_morphisms.subsingleton (?x_302 J a b) (?x_303 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.subsingleton (?x_304 J a b) (?x_305 J a b) (?x_306 J a b) (?x_307 J a b) (?x_308 J a b) (?x_309 J a b)
(?x_310 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @arrow.subsingleton_has_lift_of_mono (?x_311 J a b) (?x_312 J a b) (?x_313 J a b) (?x_314 J a b) (?x_315 J a b)
(?x_316 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @arrow.subsingleton_has_lift_of_epi (?x_317 J a b) (?x_318 J a b) (?x_319 J a b) (?x_320 J a b) (?x_321 J a b)
(?x_322 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.is_colimit.subsingleton (?x_323 J a b) (?x_324 J a b) (?x_325 J a b) (?x_326 J a b) (?x_327 J a b)
(?x_328 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @limits.is_limit.subsingleton (?x_329 J a b) (?x_330 J a b) (?x_331 J a b) (?x_332 J a b) (?x_333 J a b) (?x_334 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @discrete.subsingleton (?x_335 J a b) (?x_336 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @add_comm_group.subsingleton (?x_337 J a b) (?x_338 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @category_theory.subsingleton (?x_339 J a b) (?x_340 J a b) (?x_341 J a b) (?x_342 J a b) (?x_343 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := fintype.subsingleton (?x_344 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @vector.zero_subsingleton (?x_345 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @rat.subsingleton_ring_hom (?x_346 J a b) (?x_347 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @ring_hom.int.subsingleton_ring_hom (?x_348 J a b) (?x_349 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @nat.subsingleton_ring_hom (?x_350 J a b) (?x_351 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @plift.subsingleton (?x_352 J a b) (?x_353 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @ulift.subsingleton (?x_354 J a b) (?x_355 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @unique.subsingleton_unique (?x_356 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @trunc.subsingleton (?x_357 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := subsingleton_pempty
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @subsingleton.prod (?x_358 J a b) (?x_359 J a b) (?x_360 J a b) (?x_361 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := empty.subsingleton
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := punit.subsingleton
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @pi.subsingleton (?x_362 J a b) (?x_363 J a b) (?x_364 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := decidable.subsingleton (?x_365 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := subsingleton_prop (?x_366 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @char_p.subsingleton (?x_367 J a b) (?x_368 J a b) (?x_369 J a b)
[class_instances] (6) ?x_369 J a b : @char_p J (?x_368 J a b) 1 := @perfect_closure.char_p (?x_370 J a b) (?x_371 J a b) (?x_372 J a b) (?x_373 J a b) (?x_374 J a b)
failed is_def_eq
[class_instances] (6) ?x_369 J a b : @char_p J (?x_368 J a b) 1 := @mv_polynomial.char_p (?x_375 J a b) (?x_376 J a b) (?x_377 J a b) (?x_378 J a b) (?x_379 J a b)
failed is_def_eq
[class_instances] (6) ?x_369 J a b : @char_p J (?x_368 J a b) 1 := @polynomial.char_p (?x_380 J a b) (?x_381 J a b) (?x_382 J a b) (?x_383 J a b)
failed is_def_eq
[class_instances] (6) ?x_369 J a b : @char_p J (?x_368 J a b) 1 := zmod.char_p (?x_384 J a b)
failed is_def_eq
[class_instances] (6) ?x_369 J a b : @char_p J (?x_368 J a b) 1 := @char_p.of_char_zero (?x_385 J a b) (?x_386 J a b) (?x_387 J a b)
failed is_def_eq
[class_instances] (5) ?x_171 J a b : subsingleton J := @unique.subsingleton (?x_174 J a b) (?x_175 J a b)
[class_instances] (6) ?x_175 J a b : unique J := @limits.unique_from_initial (?x_176 J a b) (?x_177 J a b) (?x_178 J a b) (?x_179 J a b)
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := @limits.unique_to_terminal (?x_180 J a b) (?x_181 J a b) (?x_182 J a b) (?x_183 J a b)
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := AddCommGroup.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := CommGroup.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := AddGroup.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := Group.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := fin.tuple0_unique (?x_184 J a b)
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := @set.unique_singleton (?x_185 J a b) (?x_186 J a b)
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := fin.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := punit.unique
failed is_def_eq
[class_instances] (6) ?x_175 J a b : unique J := @subsingleton.unique_topological_space (?x_187 J a b) _
failed is_def_eq
[class_instances] caching failure for Π (J : Type v), J → J → unique J
[class_instances] caching failure for ∀ (J : Type v), J → J → subsingleton J
[class_instances] caching failure for Π (J : Type v), decidable_eq J
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.category_theory.limits.has_limits_of_shape (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J) (@?x_135 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_terminal.has_limits_of_shape (?x_136 J) (?x_137 J) (?x_138 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @non_preadditive_abelian.category_theory.limits.has_equalizers (?x_139 J) (?x_140 J) (?x_141 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_binary_products_of_has_binary_biproducts (?x_142 J) (?x_143 J) (?x_144 J) (?x_145 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_limits_of_shape_walking_pair (?x_146 J) (?x_147 J) (?x_148 J) (?x_149 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_finite_limits.has_limits_of_shape (?x_150 J) (?x_151 J) (?x_152 J) (?x_153 J) (?x_154 J) (?x_155 J)
[class_instances] (4) ?x_155 J : @fin_category (discrete J) (category_theory.discrete_category J) := @limits.fin_category_wide_pushout (?x_156 J) (?x_157 J) (?x_158 J)
failed is_def_eq
[class_instances] (4) ?x_155 J : @fin_category (discrete J) (category_theory.discrete_category J) := @limits.fin_category_wide_pullback (?x_159 J) (?x_160 J) (?x_161 J)
failed is_def_eq
[class_instances] (4) ?x_155 J : @fin_category (discrete J) (category_theory.discrete_category J) := limits.category_theory.fin_category
failed is_def_eq
[class_instances] (4) ?x_155 J : @fin_category (discrete J) (category_theory.discrete_category J) := @category_theory.fin_category_discrete_of_decidable_fintype (?x_162 J) (?x_163 J) (?x_164 J)
[class_instances] cached failure for Π (J : Type v), decidable_eq J
[class_instances] caching failure for Π (J : Type v), @fin_category (discrete J) (category_theory.discrete_category J)
[class_instances] (3) ?x_129 J : @limits.has_limits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_limits_of_shape_of_has_limits (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J)
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := Top.Top_has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @over.has_limits (?x_135 J) (?x_136 J) (?x_137 J) (?x_138 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @under.has_limits (?x_139 J) (?x_140 J) (?x_141 J) (?x_142 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @limits.has_limits_op_of_has_colimits (?x_143 J) (?x_144 J) (?x_145 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @limits.functor_category_has_limits (?x_146 J) (?x_147 J) (?x_148 J) (?x_149 J) (?x_150 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @Algebra.has_limits (?x_151 J) (?x_152 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := CommRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := Ring.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := CommSemiRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := SemiRing.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @Module.has_limits (?x_153 J) (?x_154 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := AddCommGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := CommGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := AddGroup.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := Group.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := AddCommMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := CommMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := AddMon.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := Mon.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := limits.types.category_theory.limits.has_limits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_limits C _inst_1 := @limits.has_limits_of_complete_lattice (?x_155 J) (?x_156 J)
failed is_def_eq
[class_instances] caching failure for Type v → @limits.has_limits C _inst_1
[class_instances] caching failure for @limits.has_products C _inst_1
[class_instances] caching failure for @limits.has_finite_products C _inst_1
[class_instances] caching failure for @limits.has_terminal C _inst_1
[class_instances] (0) ?x_119 : @limits.has_zero_object C _inst_1 := @limits.has_zero_object_of_has_initial_object ?x_120 ?x_121 ?x_122 ?x_123
[class_instances] (1) ?x_123 : @limits.has_initial C _inst_1 := @limits.category_theory.limits.has_initial ?x_124 ?x_125 ?x_126
[class_instances] (2) ?x_126 : @limits.has_finite_coproducts C _inst_1 := @non_preadditive_abelian.has_finite_coproducts ?x_127 ?x_128 ?x_129
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] (2) ?x_126 : @limits.has_finite_coproducts C _inst_1 := @limits.has_finite_coproducts_of_has_finite_biproducts ?x_127 ?x_128 ?x_129 ?x_130
[class_instances] (3) ?x_130 : @limits.has_finite_biproducts C _inst_1 ?x_129 := AddCommGroup.category_theory.limits.has_finite_biproducts
failed is_def_eq
[class_instances] (2) ?x_126 : @limits.has_finite_coproducts C _inst_1 := @limits.has_finite_coproducts_of_has_finite_colimits ?x_127 ?x_128 ?x_129
[class_instances] (3) ?x_129 : @limits.has_finite_colimits C _inst_1 := @limits.has_finite_colimits_of_semilattice_sup_bot ?x_130 ?x_131
failed is_def_eq
[class_instances] (3) ?x_129 : @limits.has_finite_colimits C _inst_1 := @limits.category_theory.limits.has_finite_colimits ?x_132 ?x_133 ?x_134
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := Top.Top_has_colimits
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := @over.has_colimits ?x_135 ?x_136 ?x_137 ?x_138
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := @limits.has_colimits_op_of_has_limits ?x_139 ?x_140 ?x_141
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := @limits.functor_category_has_colimits ?x_142 ?x_143 ?x_144 ?x_145 ?x_146
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := Mon.colimits.has_colimits_Mon
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := AddCommGroup.colimits.has_colimits_AddCommGroup
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := CommRing.colimits.has_colimits_CommRing
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := limits.types.category_theory.limits.has_colimits
failed is_def_eq
[class_instances] (4) ?x_134 : @limits.has_colimits C _inst_1 := @limits.has_colimits_of_complete_lattice ?x_147 ?x_148
failed is_def_eq
[class_instances] caching failure for @limits.has_colimits C _inst_1
[class_instances] caching failure for @limits.has_finite_colimits C _inst_1
[class_instances] (2) ?x_126 : @limits.has_finite_coproducts C _inst_1 := @limits.has_finite_coproducts_of_has_coproducts ?x_127 ?x_128 ?x_129
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @over.has_colimits_of_shape (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J) (?x_135 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_coproducts_opposite (?x_136 J) (?x_137 J) (?x_138 J) (?x_139 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_colimits_of_shape_op_of_has_limits_of_shape (?x_140 J) (?x_141 J) (?x_142 J) (?x_143 J) (?x_144 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.functor_category_has_colimits_of_shape (?x_145 J) (?x_146 J) (?x_147 J) (?x_148 J) (?x_149 J) (?x_150 J)
(?x_151 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_finite_coproducts.has_colimits_of_shape (?x_152 J) (?x_153 J) (?x_154 J) (?x_155 J) (?x_156 J) (?x_157 J)
[class_instances] cached failure for Π (J : Type v), decidable_eq J
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.category_theory.limits.has_colimits_of_shape (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J) (@?x_135 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_initial.has_colimits_of_shape (?x_136 J) (?x_137 J) (?x_138 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @non_preadditive_abelian.category_theory.limits.has_coequalizers (?x_139 J) (?x_140 J) (?x_141 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_binary_coproducts_of_has_binary_biproducts (?x_142 J) (?x_143 J) (?x_144 J) (?x_145 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_colimits_of_shape_walking_pair (?x_146 J) (?x_147 J) (?x_148 J) (?x_149 J)
failed is_def_eq
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_finite_colimits.has_colimits_of_shape (?x_150 J) (?x_151 J) (?x_152 J) (?x_153 J) (?x_154 J) (?x_155 J)
[class_instances] cached failure for Π (J : Type v), @fin_category (discrete J) (category_theory.discrete_category J)
[class_instances] (3) ?x_129 J : @limits.has_colimits_of_shape (discrete J) (category_theory.discrete_category J) C _inst_1 := @limits.has_colimits_of_shape_of_has_colimits (?x_130 J) (?x_131 J) (?x_132 J) (?x_133 J) (?x_134 J)
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := Top.Top_has_colimits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := @over.has_colimits (?x_135 J) (?x_136 J) (?x_137 J) (?x_138 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := @limits.has_colimits_op_of_has_limits (?x_139 J) (?x_140 J) (?x_141 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := @limits.functor_category_has_colimits (?x_142 J) (?x_143 J) (?x_144 J) (?x_145 J) (?x_146 J)
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := Mon.colimits.has_colimits_Mon
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := AddCommGroup.colimits.has_colimits_AddCommGroup
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := CommRing.colimits.has_colimits_CommRing
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := limits.types.category_theory.limits.has_colimits
failed is_def_eq
[class_instances] (4) ?x_134 J : @limits.has_colimits C _inst_1 := @limits.has_colimits_of_complete_lattice (?x_147 J) (?x_148 J)
failed is_def_eq
[class_instances] caching failure for Type v → @limits.has_colimits C _inst_1
[class_instances] caching failure for @limits.has_coproducts C _inst_1
[class_instances] caching failure for @limits.has_finite_coproducts C _inst_1
[class_instances] caching failure for @limits.has_initial C _inst_1
[class_instances] caching failure for @limits.has_zero_object C _inst_1
[class_instances] caching failure for @limits.has_zero_object C _inst_1
[class_instances] cached failure for @limits.has_zero_object C _inst_1
[class_instances] cached failure for @limits.has_zero_object C _inst_1
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.lift_mono ?x_119 ?x_120 ?x_121 ?x_122 ?x_123 ?x_124 ?x_125
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.category_theory.mono ?x_126 ?x_127 ?x_128 ?x_129 ?x_130 ?x_131
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := ?x_137.m_mono
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.equalizer.ι_mono ?x_138 ?x_139 ?x_140 ?x_141 ?x_142 ?x_143 ?x_144
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.prod.mono_lift_of_mono_right ?x_145 ?x_146 ?x_147 ?x_148 ?x_149 ?x_150 ?x_151 ?x_152 ?x_153
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @limits.prod.mono_lift_of_mono_left ?x_154 ?x_155 ?x_156 ?x_157 ?x_158 ?x_159 ?x_160 ?x_161 ?x_162
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.op_mono_of_epi ?x_163 ?x_164 ?x_165 ?x_166 ?x_167 ?x_168
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.unop_mono_of_epi ?x_169 ?x_170 ?x_171 ?x_172 ?x_173 ?x_174
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.mono ?x_175 ?x_176 ?x_177
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @regular_mono.mono ?x_178 ?x_179 ?x_180 ?x_181 ?x_182 ?x_183
[class_instances] (1) ?x_183 : @regular_mono C _inst_1 X Y f := @category_theory.equalizer_regular ?x_184 ?x_185 ?x_186 ?x_187 ?x_188 ?x_189 ?x_190
failed is_def_eq
[class_instances] (1) ?x_183 : @regular_mono C _inst_1 X Y f := @normal_mono.regular_mono ?x_191 ?x_192 ?x_193 ?x_194 ?x_195 ?x_196 ?x_197
[class_instances] (1) ?x_183 : @regular_mono C _inst_1 X Y f := @regular_mono.of_split_mono ?x_184 ?x_185 ?x_186 ?x_187 ?x_188 ?x_189
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.biprod.inr_mono ?x_190 ?x_191 ?x_192 ?x_193 ?x_194 ?x_195
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.biprod.inl_mono ?x_196 ?x_197 ?x_198 ?x_199 ?x_200 ?x_201
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.biproduct.ι_mono ?x_202 ?x_203 ?x_204 ?x_205 ?x_206 ?x_207 ?x_208 ?x_209
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.split_mono_coprod_inr ?x_210 ?x_211 ?x_212 ?x_213 ?x_214 ?x_215
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.split_mono_coprod_inl ?x_216 ?x_217 ?x_218 ?x_219 ?x_220 ?x_221
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @limits.split_mono_sigma_ι ?x_222 ?x_223 ?x_224 ?x_225 ?x_226 ?x_227 ?x_228 ?x_229
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @category_theory.split_mono ?x_230 ?x_231 ?x_232 ?x_233 ?x_234 ?x_235 ?x_236 ?x_237 ?x_238
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @category_theory.section_split_mono ?x_239 ?x_240 ?x_241 ?x_242 ?x_243 ?x_244
failed is_def_eq
[class_instances] (2) ?x_189 : @split_mono C _inst_1 X Y f := @split_mono.of_iso ?x_245 ?x_246 ?x_247 ?x_248 ?x_249 ?x_250
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @reflective.category_theory.is_iso ?x_251 ?x_252 ?x_253 ?x_254 ?x_255 ?x_256 ?x_257
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.μ_iso_of_reflective ?x_258 ?x_259 ?x_260 ?x_261 ?x_262 ?x_263
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.strict_initial ?x_264 ?x_265 ?x_266 ?x_267 ?x_268 ?x_269 ?x_270
[class_instances] cached failure for @limits.has_initial C _inst_1
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := ?x_277.μ_is_iso ?x_278 ?x_279
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_280 : @monoidal_category C _inst_1 := monoidal.types_monoidal
failed is_def_eq
[class_instances] (0) ?x_280 : @monoidal_category C _inst_1 := @monoidal.functor_category_monoidal ?x_281 ?x_282 ?x_283 ?x_284 ?x_285
failed is_def_eq
[class_instances] (0) ?x_280 : @monoidal_category C _inst_1 := @Module.Module.monoidal_category ?x_286 ?x_287
failed is_def_eq
[class_instances] caching failure for @monoidal_category C _inst_1
[class_instances] caching failure for @monoidal_category C _inst_1
[class_instances] cached failure for @monoidal_category C _inst_1
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := ?x_286.ε_is_iso
[class_instances] cached failure for @monoidal_category C _inst_1
[class_instances] cached failure for @monoidal_category C _inst_1
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.prod_comparison_iso_of_preserves_binary_prods ?x_287 ?x_288 ?x_289 ?x_290 ?x_291 ?x_292 ?x_293 ?x_294 ?x_295
?x_296
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.counit_is_iso_of_R_fully_faithful ?x_297 ?x_298 ?x_299 ?x_300 ?x_301 ?x_302 ?x_303 ?x_304 ?x_305
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.unit_is_iso_of_L_fully_faithful ?x_306 ?x_307 ?x_308 ?x_309 ?x_310 ?x_311 ?x_312 ?x_313 ?x_314
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @monoidal_category.tensor_is_iso ?x_315 ?x_316 ?x_317 ?x_318 ?x_319 ?x_320 ?x_321 ?x_322 ?x_323 ?x_324 ?x_325
[class_instances] cached failure for @monoidal_category C _inst_1
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @abelian.is_iso_factor_thru_coimage ?x_326 ?x_327 ?x_328 ?x_329 ?x_330 ?x_331 ?x_332
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @abelian.is_iso_factor_thru_image ?x_333 ?x_334 ?x_335 ?x_336 ?x_337 ?x_338 ?x_339
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @non_preadditive_abelian.is_iso_r ?x_340 ?x_341 ?x_342 ?x_343
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
[class_instances] cached failure for @non_preadditive_abelian C _inst_1
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @non_preadditive_abelian.is_iso_factor_thru_coimage ?x_344 ?x_345 ?x_346 ?x_347 ?x_348 ?x_349 ?x_350
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @non_preadditive_abelian.is_iso_factor_thru_image ?x_351 ?x_352 ?x_353 ?x_354 ?x_355 ?x_356 ?x_357
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.cokernel.of_kernel_of_mono ?x_358 ?x_359 ?x_360 ?x_361 ?x_362 ?x_363 ?x_364 ?x_365 ?x_366 ?x_367
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.kernel.of_cokernel_of_epi ?x_368 ?x_369 ?x_370 ?x_371 ?x_372 ?x_373 ?x_374 ?x_375 ?x_376 ?x_377
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.cokernel.π_zero_is_iso ?x_378 ?x_379 ?x_380 ?x_381 ?x_382 ?x_383
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.kernel.ι_zero_is_iso ?x_384 ?x_385 ?x_386 ?x_387 ?x_388 ?x_389
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.category_theory.is_iso ?x_390 ?x_391 ?x_392 ?x_393 ?x_394 ?x_395 ?x_396 ?x_397 ?x_398
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.coequalizer.π_of_self ?x_399 ?x_400 ?x_401 ?x_402 ?x_403 ?x_404
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @limits.equalizer.ι_of_self ?x_405 ?x_406 ?x_407 ?x_408 ?x_409 ?x_410
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.is_iso_whisker_right ?x_411 ?x_412 ?x_413 ?x_414 ?x_415 ?x_416 ?x_417 ?x_418 ?x_419 ?x_420 ?x_421
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @category_theory.is_iso_whisker_left ?x_422 ?x_423 ?x_424 ?x_425 ?x_426 ?x_427 ?x_428 ?x_429 ?x_430 ?x_431 ?x_432
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @nat_iso.is_iso_of_is_iso_app' ?x_433 ?x_434 ?x_435 ?x_436 ?x_437 ?x_438 ?x_439 ?x_440
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @nat_iso.inv_app_is_iso ?x_441 ?x_442 ?x_443 ?x_444 ?x_445 ?x_446 ?x_447 ?x_448
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @nat_iso.hom_app_is_iso ?x_449 ?x_450 ?x_451 ?x_452 ?x_453 ?x_454 ?x_455 ?x_456
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @functor.map_is_iso ?x_457 ?x_458 ?x_459 ?x_460 ?x_461 ?x_462 ?x_463 ?x_464 ?x_465
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.comp_is_iso ?x_466 ?x_467 ?x_468 ?x_469 ?x_470 ?x_471 ?x_472 ?x_473 ?x_474
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.inv_is_iso ?x_475 ?x_476 ?x_477 ?x_478 ?x_479 ?x_480
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.of_iso_inverse ?x_481 ?x_482 ?x_483 ?x_484 ?x_485
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.of_iso ?x_486 ?x_487 ?x_488 ?x_489 ?x_490
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.category_theory.is_iso ?x_491 ?x_492 ?x_493
failed is_def_eq
[class_instances] (3) ?x_250 : @is_iso C _inst_1 X Y f := @is_iso.of_groupoid ?x_494 ?x_495 ?x_496 ?x_497 ?x_498
[class_instances] class-instance resolution trace
[class_instances] (0) ?x_499 : groupoid C := @category_theory.core_category ?x_500 ?x_501
failed is_def_eq
[class_instances] (0) ?x_499 : groupoid C := ?x_502.str
failed is_def_eq
[class_instances] (0) ?x_499 : groupoid C := @action_category.category_theory.groupoid ?x_503 ?x_504 ?x_505 ?x_506
failed is_def_eq
[class_instances] (0) ?x_499 : groupoid C := @single_obj.groupoid ?x_507 ?x_508
failed is_def_eq
[class_instances] (0) ?x_499 : groupoid C := @category_theory.groupoid_of_elements ?x_509 ?x_510 ?x_511
failed is_def_eq
[class_instances] (0) ?x_499 : groupoid C := @induced_category.groupoid ?x_512 ?x_513 ?x_514 ?x_515
failed is_def_eq
[class_instances] caching failure for groupoid C
[class_instances] caching failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
[class_instances] cached failure for groupoid C
failed is_def_eq
[class_instances] caching failure for @is_iso C _inst_1 X Y f
[class_instances] caching failure for @split_mono C _inst_1 X Y f
[class_instances] caching failure for @regular_mono C _inst_1 X Y f
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @split_mono.mono ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
[class_instances] cached failure for @split_mono C _inst_1 X Y f
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @is_iso.mono_of_iso ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
[class_instances] cached failure for @is_iso C _inst_1 X Y f
[class_instances] caching failure for @mono C _inst_1 X Y f
[class_instances] caching failure for @mono C _inst_1 X Y f
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment