kbuzzard/gist:226abffabe7ee22f464977128b9157ed

## gistfile1.txt
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := coe_sort_bool
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @coe_sort_trans ?x_12 ?x_13 ?x_14 ?x_15
[class_instances] (1) ?x_15 : has_coe_t_aux
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_13 := @coe_base_aux ?x_16 ?x_17 ?x_18
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := real.angle.angle.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @polynomial.coe_to_power_series ?x_19 ?x_20
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mv_polynomial.coe_to_mv_power_series ?x_21 ?x_22 ?x_23
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alternating_map.multilinear_map.has_coe ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.norm_fin.eval_fin_m.has_coe ?x_34
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @topological_space.opens.set.has_coe ?x_35 ?x_36
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @valuation.monoid_with_zero_hom.has_coe ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := complex.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_equiv.continuous_linear_map.has_coe ?x_41 ?x_42 ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_map.linear_map.has_coe ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.has_coe_initial_seg ?x_61 ?x_62 ?x_63 ?x_64 ?x_65
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.rel_embedding.has_coe ?x_66 ?x_67 ?x_68 ?x_69
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @initial_seg.rel_embedding.has_coe ?x_70 ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := ennreal.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nnreal.real.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_map.coe_is_scalar_tower ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86 ?x_87
  ?x_88
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_alg_hom ?x_89 ?x_90 ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_ring_equiv ?x_97 ?x_98 ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 ?x_104
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_add_monoid_hom ?x_105 ?x_106 ?x_107 ?x_108 ?x_109 ?x_110 ?x_111 ?x_112
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_monoid_hom ?x_113 ?x_114 ?x_115 ?x_116 ?x_117 ?x_118 ?x_119 ?x_120
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_ring_hom ?x_121 ?x_122 ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 ?x_128
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @omega_complete_partial_order.preorder_hom.has_coe ?x_129 ?x_130 ?x_131 ?x_132
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := enat.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @pfun.has_coe ?x_133 ?x_134
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @roption.has_coe ?x_135
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_con.to_add_submonoid ?x_136 ?x_137
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @con.to_submonoid ?x_138 ?x_139
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_equiv.linear_map.has_coe ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe' ?x_148 ?x_149 ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe ?x_156 ?x_157 ?x_158 ?x_159 ?x_160 ?x_161 ?x_162 ?x_163
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe' ?x_164 ?x_165 ?x_166 ?x_167 ?x_168 ?x_169 ?x_170 ?x_171
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe ?x_172 ?x_173 ?x_174 ?x_175 ?x_176 ?x_177 ?x_178 ?x_179
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_ring_hom ?x_180 ?x_181 ?x_182 ?x_183
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_add_equiv ?x_184 ?x_185 ?x_186 ?x_187 ?x_188 ?x_189
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_mul_equiv ?x_190 ?x_191 ?x_192 ?x_193 ?x_194 ?x_195
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.abel.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.global_preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.ring.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat.primes.coe_nat
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := fin.fin_to_nat ?x_196
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @multiset.has_coe ?x_197
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_pnat_nat
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_iso.rel_embedding.has_coe ?x_198 ?x_199 ?x_200 ?x_201
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_embedding.rel_hom.has_coe ?x_202 ?x_203 ?x_204 ?x_205
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_add_monoid_hom ?x_206 ?x_207 ?x_208 ?x_209
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_monoid_hom ?x_210 ?x_211 ?x_212 ?x_213
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_zero_hom ?x_214 ?x_215 ?x_216 ?x_217
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_monoid_hom ?x_218 ?x_219 ?x_220 ?x_221
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_add_hom ?x_222 ?x_223 ?x_224 ?x_225
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_mul_hom ?x_226 ?x_227 ?x_228 ?x_229
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_zero_hom ?x_230 ?x_231 ?x_232 ?x_233
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_one_hom ?x_234 ?x_235 ?x_236 ?x_237
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_units.has_coe ?x_238 ?x_239
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @units.has_coe ?x_240 ?x_241
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.html.list_coe ?x_242
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.component.has_coe ?x_243 ?x_244
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.array_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.bool_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.float_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.int_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.string_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_int_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_nat_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := int.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @list.bin_tree_to_list ?x_245
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := smt_tactic.has_coe ?x_246
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @lean.parser.has_coe ?x_247
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.ex_to_tac ?x_248
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.opt_to_tac ?x_249
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @expr.has_coe ?x_250 ?x_251
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_name
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @coe_subtype ?x_252 ?x_253
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_bool_to_Prop
failed is_def_eq
[class_instances] (1) ?x_15 : has_coe_t_aux
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_13 := @coe_trans_aux ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := real.angle.angle.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @polynomial.coe_to_power_series ?x_21 ?x_22
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mv_polynomial.coe_to_mv_power_series ?x_23 ?x_24 ?x_25
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alternating_map.multilinear_map.has_coe ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34 ?x_35
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.norm_fin.eval_fin_m.has_coe ?x_36
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @topological_space.opens.set.has_coe ?x_37 ?x_38
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @valuation.monoid_with_zero_hom.has_coe ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := complex.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_equiv.continuous_linear_map.has_coe ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_map.linear_map.has_coe ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.has_coe_initial_seg ?x_63 ?x_64 ?x_65 ?x_66 ?x_67
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.rel_embedding.has_coe ?x_68 ?x_69 ?x_70 ?x_71
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @initial_seg.rel_embedding.has_coe ?x_72 ?x_73 ?x_74 ?x_75
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := ennreal.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nnreal.real.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_map.coe_is_scalar_tower ?x_76 ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86 ?x_87 ?x_88 ?x_89
  ?x_90
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_alg_hom ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97 ?x_98
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_ring_equiv ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 ?x_104 ?x_105 ?x_106
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_add_monoid_hom ?x_107 ?x_108 ?x_109 ?x_110 ?x_111 ?x_112 ?x_113 ?x_114
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_monoid_hom ?x_115 ?x_116 ?x_117 ?x_118 ?x_119 ?x_120 ?x_121 ?x_122
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_ring_hom ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 ?x_128 ?x_129 ?x_130
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @omega_complete_partial_order.preorder_hom.has_coe ?x_131 ?x_132 ?x_133 ?x_134
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := enat.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @pfun.has_coe ?x_135 ?x_136
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @roption.has_coe ?x_137
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_con.to_add_submonoid ?x_138 ?x_139
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @con.to_submonoid ?x_140 ?x_141
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_equiv.linear_map.has_coe ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147 ?x_148 ?x_149
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe' ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155 ?x_156 ?x_157
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe ?x_158 ?x_159 ?x_160 ?x_161 ?x_162 ?x_163 ?x_164 ?x_165
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe' ?x_166 ?x_167 ?x_168 ?x_169 ?x_170 ?x_171 ?x_172 ?x_173
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe ?x_174 ?x_175 ?x_176 ?x_177 ?x_178 ?x_179 ?x_180 ?x_181
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_ring_hom ?x_182 ?x_183 ?x_184 ?x_185
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_add_equiv ?x_186 ?x_187 ?x_188 ?x_189 ?x_190 ?x_191
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_mul_equiv ?x_192 ?x_193 ?x_194 ?x_195 ?x_196 ?x_197
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.abel.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.global_preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.ring.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat.primes.coe_nat
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := fin.fin_to_nat ?x_198
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @multiset.has_coe ?x_199
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_pnat_nat
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_iso.rel_embedding.has_coe ?x_200 ?x_201 ?x_202 ?x_203
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_embedding.rel_hom.has_coe ?x_204 ?x_205 ?x_206 ?x_207
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_add_monoid_hom ?x_208 ?x_209 ?x_210 ?x_211
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_monoid_hom ?x_212 ?x_213 ?x_214 ?x_215
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_zero_hom ?x_216 ?x_217 ?x_218 ?x_219
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_monoid_hom ?x_220 ?x_221 ?x_222 ?x_223
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_add_hom ?x_224 ?x_225 ?x_226 ?x_227
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_mul_hom ?x_228 ?x_229 ?x_230 ?x_231
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_zero_hom ?x_232 ?x_233 ?x_234 ?x_235
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_one_hom ?x_236 ?x_237 ?x_238 ?x_239
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_units.has_coe ?x_240 ?x_241
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @units.has_coe ?x_242 ?x_243
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.html.list_coe ?x_244
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.component.has_coe ?x_245 ?x_246
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.array_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.bool_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.float_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.int_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.string_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_int_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_nat_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := int.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @list.bin_tree_to_list ?x_247
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := smt_tactic.has_coe ?x_248
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @lean.parser.has_coe ?x_249
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.ex_to_tac ?x_250
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.opt_to_tac ?x_251
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @expr.has_coe ?x_252 ?x_253
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_name
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @coe_subtype ?x_254 ?x_255
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_bool_to_Prop
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set_like.has_coe_to_sort ?x_4 ?x_5 ?x_6
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subalgebra.set_like ?x_7 ?x_8 ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subring.set_like ?x_12 ?x_13
failed is_def_eq
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subsemiring.set_like ?x_14 ?x_15
[class_instances] caching instance for set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  (ℕ → R)
@subsemiring.set_like (ℕ → R)
  (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))
[class_instances] caching instance for has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
@set_like.has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  (ℕ → R)
  (@subsemiring.set_like (ℕ → R)
     (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := coe_sort_bool
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @coe_sort_trans ?x_12 ?x_13 ?x_14 ?x_15
[class_instances] (1) ?x_15 : has_coe_t_aux
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_13 := @coe_base_aux ?x_16 ?x_17 ?x_18
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := real.angle.angle.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @polynomial.coe_to_power_series ?x_19 ?x_20
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mv_polynomial.coe_to_mv_power_series ?x_21 ?x_22 ?x_23
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alternating_map.multilinear_map.has_coe ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.norm_fin.eval_fin_m.has_coe ?x_34
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @topological_space.opens.set.has_coe ?x_35 ?x_36
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @valuation.monoid_with_zero_hom.has_coe ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := complex.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_equiv.continuous_linear_map.has_coe ?x_41 ?x_42 ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_map.linear_map.has_coe ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.has_coe_initial_seg ?x_61 ?x_62 ?x_63 ?x_64 ?x_65
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.rel_embedding.has_coe ?x_66 ?x_67 ?x_68 ?x_69
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @initial_seg.rel_embedding.has_coe ?x_70 ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := ennreal.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nnreal.real.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_map.coe_is_scalar_tower ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86 ?x_87
  ?x_88
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_alg_hom ?x_89 ?x_90 ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_ring_equiv ?x_97 ?x_98 ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 ?x_104
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_add_monoid_hom ?x_105 ?x_106 ?x_107 ?x_108 ?x_109 ?x_110 ?x_111 ?x_112
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_monoid_hom ?x_113 ?x_114 ?x_115 ?x_116 ?x_117 ?x_118 ?x_119 ?x_120
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_ring_hom ?x_121 ?x_122 ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 ?x_128
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @omega_complete_partial_order.preorder_hom.has_coe ?x_129 ?x_130 ?x_131 ?x_132
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := enat.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @pfun.has_coe ?x_133 ?x_134
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @roption.has_coe ?x_135
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_con.to_add_submonoid ?x_136 ?x_137
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @con.to_submonoid ?x_138 ?x_139
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_equiv.linear_map.has_coe ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe' ?x_148 ?x_149 ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe ?x_156 ?x_157 ?x_158 ?x_159 ?x_160 ?x_161 ?x_162 ?x_163
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe' ?x_164 ?x_165 ?x_166 ?x_167 ?x_168 ?x_169 ?x_170 ?x_171
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe ?x_172 ?x_173 ?x_174 ?x_175 ?x_176 ?x_177 ?x_178 ?x_179
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_ring_hom ?x_180 ?x_181 ?x_182 ?x_183
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_add_equiv ?x_184 ?x_185 ?x_186 ?x_187 ?x_188 ?x_189
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_mul_equiv ?x_190 ?x_191 ?x_192 ?x_193 ?x_194 ?x_195
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.abel.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.global_preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.ring.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat.primes.coe_nat
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := fin.fin_to_nat ?x_196
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @multiset.has_coe ?x_197
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_pnat_nat
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_iso.rel_embedding.has_coe ?x_198 ?x_199 ?x_200 ?x_201
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_embedding.rel_hom.has_coe ?x_202 ?x_203 ?x_204 ?x_205
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_add_monoid_hom ?x_206 ?x_207 ?x_208 ?x_209
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_monoid_hom ?x_210 ?x_211 ?x_212 ?x_213
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_zero_hom ?x_214 ?x_215 ?x_216 ?x_217
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_monoid_hom ?x_218 ?x_219 ?x_220 ?x_221
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_add_hom ?x_222 ?x_223 ?x_224 ?x_225
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_mul_hom ?x_226 ?x_227 ?x_228 ?x_229
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_zero_hom ?x_230 ?x_231 ?x_232 ?x_233
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_one_hom ?x_234 ?x_235 ?x_236 ?x_237
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_units.has_coe ?x_238 ?x_239
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @units.has_coe ?x_240 ?x_241
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.html.list_coe ?x_242
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.component.has_coe ?x_243 ?x_244
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.array_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.bool_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.float_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.int_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.string_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_int_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_nat_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := int.has_coe
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @list.bin_tree_to_list ?x_245
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := smt_tactic.has_coe ?x_246
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @lean.parser.has_coe ?x_247
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.ex_to_tac ?x_248
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.opt_to_tac ?x_249
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @expr.has_coe ?x_250 ?x_251
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_name
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @coe_subtype ?x_252 ?x_253
failed is_def_eq
[class_instances] (2) ?x_18 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_bool_to_Prop
failed is_def_eq
[class_instances] (1) ?x_15 : has_coe_t_aux
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_13 := @coe_trans_aux ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := real.angle.angle.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @polynomial.coe_to_power_series ?x_21 ?x_22
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mv_polynomial.coe_to_mv_power_series ?x_23 ?x_24 ?x_25
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alternating_map.multilinear_map.has_coe ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34 ?x_35
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.norm_fin.eval_fin_m.has_coe ?x_36
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @topological_space.opens.set.has_coe ?x_37 ?x_38
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @valuation.monoid_with_zero_hom.has_coe ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := complex.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_equiv.continuous_linear_map.has_coe ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @continuous_linear_map.linear_map.has_coe ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.has_coe_initial_seg ?x_63 ?x_64 ?x_65 ?x_66 ?x_67
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @principal_seg.rel_embedding.has_coe ?x_68 ?x_69 ?x_70 ?x_71
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @initial_seg.rel_embedding.has_coe ?x_72 ?x_73 ?x_74 ?x_75
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := ennreal.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nnreal.real.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_map.coe_is_scalar_tower ?x_76 ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86 ?x_87 ?x_88 ?x_89
  ?x_90
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_alg_hom ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97 ?x_98
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_equiv.has_coe_to_ring_equiv ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 ?x_104 ?x_105 ?x_106
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_add_monoid_hom ?x_107 ?x_108 ?x_109 ?x_110 ?x_111 ?x_112 ?x_113 ?x_114
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_monoid_hom ?x_115 ?x_116 ?x_117 ?x_118 ?x_119 ?x_120 ?x_121 ?x_122
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @alg_hom.coe_ring_hom ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 ?x_128 ?x_129 ?x_130
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @omega_complete_partial_order.preorder_hom.has_coe ?x_131 ?x_132 ?x_133 ?x_134
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := enat.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @pfun.has_coe ?x_135 ?x_136
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @roption.has_coe ?x_137
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_con.to_add_submonoid ?x_138 ?x_139
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @con.to_submonoid ?x_140 ?x_141
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @linear_equiv.linear_map.has_coe ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147 ?x_148 ?x_149
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe' ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155 ?x_156 ?x_157
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @mul_semiring_action_hom.has_coe ?x_158 ?x_159 ?x_160 ?x_161 ?x_162 ?x_163 ?x_164 ?x_165
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe' ?x_166 ?x_167 ?x_168 ?x_169 ?x_170 ?x_171 ?x_172 ?x_173
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @distrib_mul_action_hom.has_coe ?x_174 ?x_175 ?x_176 ?x_177 ?x_178 ?x_179 ?x_180 ?x_181
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_ring_hom ?x_182 ?x_183 ?x_184 ?x_185
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_add_equiv ?x_186 ?x_187 ?x_188 ?x_189 ?x_190 ?x_191
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_equiv.has_coe_to_mul_equiv ?x_192 ?x_193 ?x_194 ?x_195 ?x_196 ?x_197
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.abel.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.global_preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := linarith.preprocessor_to_gb_preprocessor
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := tactic.ring.expr.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat.primes.coe_nat
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := fin.fin_to_nat ?x_198
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @multiset.has_coe ?x_199
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_pnat_nat
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_iso.rel_embedding.has_coe ?x_200 ?x_201 ?x_202 ?x_203
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @rel_embedding.rel_hom.has_coe ?x_204 ?x_205 ?x_206 ?x_207
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_add_monoid_hom ?x_208 ?x_209 ?x_210 ?x_211
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @ring_hom.has_coe_monoid_hom ?x_212 ?x_213 ?x_214 ?x_215
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_zero_hom ?x_216 ?x_217 ?x_218 ?x_219
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_with_zero_hom.has_coe_to_monoid_hom ?x_220 ?x_221 ?x_222 ?x_223
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_add_hom ?x_224 ?x_225 ?x_226 ?x_227
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_mul_hom ?x_228 ?x_229 ?x_230 ?x_231
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_monoid_hom.has_coe_to_zero_hom ?x_232 ?x_233 ?x_234 ?x_235
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @monoid_hom.has_coe_to_one_hom ?x_236 ?x_237 ?x_238 ?x_239
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @add_units.has_coe ?x_240 ?x_241
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @units.has_coe ?x_242 ?x_243
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.html.list_coe ?x_244
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @widget.component.has_coe ?x_245 ?x_246
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.array_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.bool_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.float_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.int_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := json.string_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_int_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := native.float.of_nat_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := int.has_coe
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @list.bin_tree_to_list ?x_247
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := smt_tactic.has_coe ?x_248
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @lean.parser.has_coe ?x_249
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.ex_to_tac ?x_250
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @tactic.opt_to_tac ?x_251
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @expr.has_coe ?x_252 ?x_253
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := string_to_name
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := @coe_subtype ?x_254 ?x_255
failed is_def_eq
[class_instances] (2) ?x_20 : has_coe
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_17 := coe_bool_to_Prop
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set_like.has_coe_to_sort ?x_4 ?x_5 ?x_6
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subalgebra.set_like ?x_7 ?x_8 ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subring.set_like ?x_12 ?x_13
failed is_def_eq
[class_instances] (1) ?x_6 : set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  ?x_5 := @subsemiring.set_like ?x_14 ?x_15
[class_instances] caching instance for set_like
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  (ℕ → R)
@subsemiring.set_like (ℕ → R)
  (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))
[class_instances] caching instance for has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
@set_like.has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
  (ℕ → R)
  (@subsemiring.set_like (ℕ → R)
     (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1)))
perfection.lean:110:0
declaration 'perfection.frobenius_pth_root' uses sorry
perfection.lean:110:28
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := _inst_1
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @power_series.comm_semiring ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @mv_power_series.comm_semiring ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @ideal.comm_semiring ?x_6 ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @mv_polynomial.comm_semiring ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @polynomial.comm_semiring ?x_11 ?x_12
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @add_monoid_algebra.comm_semiring ?x_13 ?x_14 ?x_15 ?x_16
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @monoid_algebra.comm_semiring ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := ?x_26.to_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @submodule.comm_semiring ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := cardinal.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := nnreal.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := real.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @ring_quot.comm_semiring ?x_32 ?x_33 ?x_34
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @algebra.comap.comm_semiring ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := ?x_41.to_comm_semiring
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := _inst_1
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @power_series.comm_semiring ?x_43 ?x_44
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @mv_power_series.comm_semiring ?x_45 ?x_46 ?x_47
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @ideal.comm_semiring ?x_48 ?x_49
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @mv_polynomial.comm_semiring ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @polynomial.comm_semiring ?x_53 ?x_54
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @add_monoid_algebra.comm_semiring ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @monoid_algebra.comm_semiring ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := ?x_68.to_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @submodule.comm_semiring ?x_69 ?x_70 ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := cardinal.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := nnreal.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := real.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @ring_quot.comm_semiring ?x_74 ?x_75 ?x_76
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @algebra.comap.comm_semiring ?x_77 ?x_78 ?x_79 ?x_80
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := ?x_83.to_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @prod.comm_semiring ?x_84 ?x_85 ?x_86 ?x_87
failed is_def_eq
[class_instances] (0) ?x_42 : comm_semiring (ℕ → R) := @pi.comm_semiring ?x_88 ?x_89 ?x_90
[class_instances] (1) ?x_90 i : comm_semiring R := _inst_1
[class_instances] caching instance for ℕ → comm_semiring R
λ (i : ℕ), _inst_1
[class_instances] caching instance for comm_semiring (ℕ → R)
@pi.comm_semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), _inst_1)
[class_instances] caching instance for comm_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
(@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring
perfection.lean:110:28
[class_instances] cached instance for fact (nat.prime p)
hp
perfection.lean:110:28
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := _inst_2
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := @perfect_closure.char_p ?x_1 ?x_2 ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := zmod.char_p ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := @polynomial.char_p ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := @char_p.subring' ?x_11 ?x_12 ?x_13 ?x_14 ?x_15
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := @char_p.subring ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p := @char_p.subsemiring ?x_21 ?x_22 ?x_23 ?x_24 ?x_25
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := _inst_2
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @perfect_closure.char_p ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := zmod.char_p ?x_31
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @polynomial.char_p ?x_32 ?x_33 ?x_34 ?x_35
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @char_p.subring' ?x_36 ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @char_p.subring ?x_41 ?x_42 ?x_43 ?x_44 ?x_45
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @char_p.subsemiring ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @char_p.pi' ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_57 : comm_ring R := @localization.comm_ring ?x_58 ?x_59 ?x_60
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @localization_map.codomain.comm_ring ?x_61 ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @perfect_closure.comm_ring ?x_67 ?x_68 ?x_69 ?x_70 ?x_71
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @power_series.comm_ring ?x_72 ?x_73
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @mv_power_series.comm_ring ?x_74 ?x_75 ?x_76
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @algebra.tensor_product.tensor_product.comm_ring ?x_77 ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := zmod.comm_ring ?x_85
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := fin.comm_ring ?x_86
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := punit.comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @mv_polynomial.comm_ring ?x_87 ?x_88 ?x_89
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @polynomial.comm_ring ?x_90 ?x_91
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @add_monoid_algebra.comm_ring ?x_92 ?x_93 ?x_94 ?x_95
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @monoid_algebra.comm_ring ?x_96 ?x_97 ?x_98 ?x_99
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := ?x_105.to_comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := complex.comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := real.comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @cau_seq.completion.Cauchy.comm_ring ?x_106 ?x_107 ?x_108 ?x_109 ?x_110 ?x_111
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @cau_seq.comm_ring ?x_112 ?x_113 ?x_114 ?x_115 ?x_116 ?x_117
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @ring_quot.comm_ring ?x_118 ?x_119 ?x_120
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @ideal.quotient.comm_ring ?x_121 ?x_122 ?x_123
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @algebra.comap.comm_ring ?x_124 ?x_125 ?x_126 ?x_127
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := ?x_130.to_comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @prod.comm_ring ?x_131 ?x_132 ?x_133 ?x_134
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @pi.comm_ring ?x_135 ?x_136 ?x_137
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := rat.comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := int.comm_ring
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @opposite.comm_ring ?x_138 ?x_139
failed is_def_eq
[class_instances] (0) ?x_57 : comm_ring R := @semi_normed_comm_ring.to_comm_ring ?x_140 ?x_141
[class_instances] (1) ?x_141 : semi_normed_comm_ring R := @normed_comm_ring.to_semi_normed_comm_ring ?x_142 ?x_143
[class_instances] (2) ?x_143 : normed_comm_ring R := int.normed_comm_ring
failed is_def_eq
[class_instances] (2) ?x_143 : normed_comm_ring R := @normed_field.to_normed_comm_ring ?x_144 ?x_145
[class_instances] (3) ?x_145 : normed_field R := complex.normed_field
failed is_def_eq
[class_instances] (3) ?x_145 : normed_field R := rat.normed_field
failed is_def_eq
[class_instances] (3) ?x_145 : normed_field R := real.normed_field
failed is_def_eq
[class_instances] (3) ?x_145 : normed_field R := @normed_linear_ordered_field.to_normed_field ?x_146 ?x_147
[class_instances] (4) ?x_147 : normed_linear_ordered_field R := real.normed_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_147 : normed_linear_ordered_field R := rat.normed_linear_ordered_field
failed is_def_eq
[class_instances] caching failure for normed_linear_ordered_field R
[class_instances] (3) ?x_145 : normed_field R := @nondiscrete_normed_field.to_normed_field ?x_146 ?x_147
[class_instances] (4) ?x_147 : nondiscrete_normed_field R := complex.nondiscrete_normed_field
failed is_def_eq
[class_instances] (4) ?x_147 : nondiscrete_normed_field R := rat.nondiscrete_normed_field
failed is_def_eq
[class_instances] (4) ?x_147 : nondiscrete_normed_field R := real.nondiscrete_normed_field
failed is_def_eq
[class_instances] (4) ?x_147 : nondiscrete_normed_field R := @is_R_or_C.to_nondiscrete_normed_field ?x_148 ?x_149
[class_instances] (5) ?x_149 : is_R_or_C R := complex.is_R_or_C
failed is_def_eq
[class_instances] (5) ?x_149 : is_R_or_C R := real.is_R_or_C
failed is_def_eq
[class_instances] caching failure for is_R_or_C R
[class_instances] caching failure for nondiscrete_normed_field R
[class_instances] caching failure for normed_field R
[class_instances] caching failure for normed_comm_ring R
[class_instances] caching failure for semi_normed_comm_ring R
[class_instances] (0) ?x_57 : comm_ring R := @euclidean_domain.to_comm_ring ?x_58 ?x_59
[class_instances] (1) ?x_59 : euclidean_domain R := @polynomial.euclidean_domain ?x_60 ?x_61
failed is_def_eq
[class_instances] (1) ?x_59 : euclidean_domain R := int.euclidean_domain
failed is_def_eq
[class_instances] (1) ?x_59 : euclidean_domain R := @field.to_euclidean_domain ?x_62 ?x_63
[class_instances] (2) ?x_63 : field R := @fraction_ring.field ?x_64 ?x_65
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @localization_map.codomain.field ?x_66 ?x_67 ?x_68 ?x_69 ?x_70 ?x_71
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @perfect_closure.field ?x_72 ?x_73 ?x_74 ?x_75 ?x_76
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @zmod.field ?x_77 ?x_78
failed is_def_eq
[class_instances] (2) ?x_63 : field R := complex.field
failed is_def_eq
[class_instances] (2) ?x_63 : field R := real.field
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @local_ring.residue_field.field ?x_79 ?x_80 ?x_81
failed is_def_eq
[class_instances] (2) ?x_63 : field R := rat.field
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @opposite.field ?x_82 ?x_83
failed is_def_eq
[class_instances] (2) ?x_63 : field R := @normed_field.to_field ?x_84 ?x_85
[class_instances] cached failure for normed_field R
[class_instances] (2) ?x_63 : field R := @linear_ordered_field.to_field ?x_64 ?x_65
[class_instances] (3) ?x_65 : linear_ordered_field R := real.linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_65 : linear_ordered_field R := rat.linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_65 : linear_ordered_field R := @normed_linear_ordered_field.to_linear_ordered_field ?x_66 ?x_67
[class_instances] cached failure for normed_linear_ordered_field R
[class_instances] caching failure for linear_ordered_field R
[class_instances] caching failure for field R
[class_instances] caching failure for euclidean_domain R
[class_instances] (0) ?x_57 : comm_ring R := @ordered_comm_ring.to_comm_ring ?x_58 ?x_59
[class_instances] (1) ?x_59 : ordered_comm_ring R := ?x_65.to_ordered_comm_ring
failed is_def_eq
[class_instances] (1) ?x_59 : ordered_comm_ring R := ?x_68.to_ordered_comm_ring
failed is_def_eq
[class_instances] (1) ?x_59 : ordered_comm_ring R := @linear_ordered_comm_ring.to_ordered_comm_ring ?x_69 ?x_70
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := ?x_76.to_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := real.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := ?x_79.to_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := int.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_70 : linear_ordered_comm_ring R := @linear_ordered_field.to_linear_ordered_comm_ring ?x_80 ?x_81
[class_instances] cached failure for linear_ordered_field R
[class_instances] caching failure for linear_ordered_comm_ring R
[class_instances] caching failure for ordered_comm_ring R
[class_instances] (0) ?x_57 : comm_ring R := @field.to_comm_ring ?x_58 ?x_59
[class_instances] cached failure for field R
[class_instances] (0) ?x_57 : comm_ring R := @integral_domain.to_comm_ring ?x_58 ?x_59
[class_instances] (1) ?x_59 : integral_domain R := @localization_map.integral_domain_of_local_at_prime ?x_60 ?x_61 ?x_62 ?x_63
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @integral_closure.integral_domain ?x_64 ?x_65 ?x_66 ?x_67 ?x_68
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @power_series.integral_domain ?x_69 ?x_70
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @mv_polynomial.integral_domain ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @polynomial.integral_domain ?x_74 ?x_75
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := ?x_81.integral_domain
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := real.integral_domain
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @ideal.quotient.integral_domain ?x_82 ?x_83 ?x_84 ?x_85
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := ?x_88.integral_domain
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := rat.integral_domain
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @opposite.integral_domain ?x_89 ?x_90
failed is_def_eq
[class_instances] (1) ?x_59 : integral_domain R := @linear_ordered_comm_ring.to_integral_domain ?x_91 ?x_92
[class_instances] cached failure for linear_ordered_comm_ring R
[class_instances] (1) ?x_59 : integral_domain R := @field.to_integral_domain ?x_60 ?x_61
[class_instances] cached failure for field R
[class_instances] (1) ?x_59 : integral_domain R := @euclidean_domain.integral_domain ?x_60 ?x_61
[class_instances] cached failure for euclidean_domain R
[class_instances] caching failure for integral_domain R
[class_instances] caching failure for comm_ring R
[class_instances] caching failure for comm_ring R
[class_instances] cached failure for comm_ring R
failed is_def_eq
[class_instances] (1) ?x_24 : @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p := @char_p.pi ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 ?x_62
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_63 : semiring R := @power_series.semiring ?x_64 ?x_65
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @mv_power_series.semiring ?x_66 ?x_67 ?x_68
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @algebra.tensor_product.tensor_product.semiring ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74 ?x_75 ?x_76
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @polynomial.semiring ?x_77 ?x_78
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @add_monoid_algebra.semiring ?x_79 ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @monoid_algebra.semiring ?x_83 ?x_84 ?x_85 ?x_86
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := ?x_92.to_semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @submodule.semiring ?x_93 ?x_94 ?x_95 ?x_96 ?x_97
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := real.semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @ring_quot.semiring ?x_98 ?x_99 ?x_100
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @algebra.comap.semiring ?x_101 ?x_102 ?x_103 ?x_104
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := ?x_107.to_semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @prod.semiring ?x_108 ?x_109 ?x_110 ?x_111
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @linear_map.endomorphism_semiring ?x_112 ?x_113 ?x_114 ?x_115 ?x_116
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @matrix.semiring ?x_117 ?x_118 ?x_119 ?x_120 ?x_121
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @pi.semiring ?x_122 ?x_123 ?x_124
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @set.set_semiring.semiring ?x_125 ?x_126
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := rat.semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := int.semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := nat.semiring
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @opposite.semiring ?x_127 ?x_128
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @with_zero.semiring ?x_129 ?x_130
failed is_def_eq
[class_instances] (0) ?x_63 : semiring R := @ring.to_semiring ?x_131 ?x_132
[class_instances] (1) ?x_132 : ring R := @power_series.ring ?x_133 ?x_134
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @mv_power_series.ring ?x_135 ?x_136 ?x_137
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @algebra.tensor_product.tensor_product.ring ?x_138 ?x_139 ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @polynomial.ring ?x_146 ?x_147
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @add_monoid_algebra.ring ?x_148 ?x_149 ?x_150 ?x_151
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @monoid_algebra.ring ?x_152 ?x_153 ?x_154 ?x_155
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := ?x_161.to_ring
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @continuous_linear_map.ring ?x_162 ?x_163 ?x_164 ?x_165 ?x_166 ?x_167 ?x_168
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := real.ring
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @cau_seq.ring ?x_169 ?x_170 ?x_171 ?x_172 ?x_173 ?x_174
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @ring_quot.ring ?x_175 ?x_176 ?x_177
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @algebra.comap.ring ?x_178 ?x_179 ?x_180 ?x_181
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := ?x_184.to_ring
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @prod.ring ?x_185 ?x_186 ?x_187 ?x_188
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @linear_map.endomorphism_ring ?x_189 ?x_190 ?x_191 ?x_192 ?x_193
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @matrix.ring ?x_194 ?x_195 ?x_196 ?x_197 ?x_198
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @pi.ring ?x_199 ?x_200 ?x_201
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := int.ring
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @opposite.ring ?x_202 ?x_203
failed is_def_eq
[class_instances] (1) ?x_132 : ring R := @normed_ring.to_ring ?x_204 ?x_205
[class_instances] (2) ?x_205 : normed_ring R := @continuous_linear_map.to_normed_ring ?x_206 ?x_207 ?x_208 ?x_209 ?x_210
failed is_def_eq
[class_instances] (2) ?x_205 : normed_ring R := @prod.normed_ring ?x_211 ?x_212 ?x_213 ?x_214
failed is_def_eq
[class_instances] (2) ?x_205 : normed_ring R := ?x_220.normed_ring
failed is_def_eq
[class_instances] (2) ?x_205 : normed_ring R := @normed_comm_ring.to_normed_ring ?x_221 ?x_222
[class_instances] cached failure for normed_comm_ring R
[class_instances] caching failure for normed_ring R
[class_instances] (1) ?x_132 : ring R := @semi_normed_ring.to_ring ?x_133 ?x_134
[class_instances] (2) ?x_134 : semi_normed_ring R := @continuous_linear_map.to_semi_normed_ring ?x_135 ?x_136 ?x_137 ?x_138 ?x_139
failed is_def_eq
[class_instances] (2) ?x_134 : semi_normed_ring R := @prod.semi_normed_ring ?x_140 ?x_141 ?x_142 ?x_143
failed is_def_eq
[class_instances] (2) ?x_134 : semi_normed_ring R := ?x_149.semi_normed_ring
failed is_def_eq
[class_instances] (2) ?x_134 : semi_normed_ring R := @semi_normed_comm_ring.to_semi_normed_ring ?x_150 ?x_151
[class_instances] cached failure for semi_normed_comm_ring R
[class_instances] (2) ?x_134 : semi_normed_ring R := @normed_ring.to_semi_normed_ring ?x_135 ?x_136
[class_instances] cached failure for normed_ring R
[class_instances] caching failure for semi_normed_ring R
[class_instances] (1) ?x_132 : ring R := @nonneg_ring.to_ring ?x_133 ?x_134
[class_instances] (2) ?x_134 : nonneg_ring R := @linear_nonneg_ring.to_nonneg_ring ?x_135 ?x_136
[class_instances] caching failure for nonneg_ring R
[class_instances] (1) ?x_132 : ring R := @ordered_ring.to_ring ?x_133 ?x_134
[class_instances] (2) ?x_134 : ordered_ring R := ?x_140.to_ordered_ring
failed is_def_eq
[class_instances] (2) ?x_134 : ordered_ring R := real.ordered_ring
failed is_def_eq
[class_instances] (2) ?x_134 : ordered_ring R := ?x_143.to_ordered_ring
failed is_def_eq
[class_instances] (2) ?x_134 : ordered_ring R := rat.ordered_ring
failed is_def_eq
[class_instances] (2) ?x_134 : ordered_ring R := @linear_ordered_ring.to_ordered_ring ?x_144 ?x_145
[class_instances] (3) ?x_145 : linear_ordered_ring R := ?x_151.to_linear_ordered_ring
failed is_def_eq
[class_instances] (3) ?x_145 : linear_ordered_ring R := real.linear_ordered_ring
failed is_def_eq
[class_instances] (3) ?x_145 : linear_ordered_ring R := ?x_154.to_linear_ordered_ring
failed is_def_eq
[class_instances] (3) ?x_145 : linear_ordered_ring R := rat.linear_ordered_ring
failed is_def_eq
[class_instances] (3) ?x_145 : linear_ordered_ring R := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_155 ?x_156
[class_instances] cached failure for linear_ordered_comm_ring R
[class_instances] caching failure for linear_ordered_ring R
[class_instances] (2) ?x_134 : ordered_ring R := @ordered_comm_ring.to_ordered_ring ?x_135 ?x_136
[class_instances] cached failure for ordered_comm_ring R
[class_instances] caching failure for ordered_ring R
[class_instances] (1) ?x_132 : ring R := @division_ring.to_ring ?x_133 ?x_134
[class_instances] (2) ?x_134 : division_ring R := real.division_ring
failed is_def_eq
[class_instances] (2) ?x_134 : division_ring R := rat.division_ring
failed is_def_eq
[class_instances] (2) ?x_134 : division_ring R := @field.to_division_ring ?x_135 ?x_136
[class_instances] cached failure for field R
[class_instances] caching failure for division_ring R
[class_instances] (1) ?x_132 : ring R := @domain.to_ring ?x_133 ?x_134
[class_instances] (2) ?x_134 : domain R := real.domain
failed is_def_eq
[class_instances] (2) ?x_134 : domain R := @linear_nonneg_ring.to_domain ?x_135 ?x_136
[class_instances] (2) ?x_134 : domain R := @linear_ordered_ring.to_domain ?x_135 ?x_136
[class_instances] cached failure for linear_ordered_ring R
[class_instances] (2) ?x_134 : domain R := @division_ring.to_domain ?x_135 ?x_136
[class_instances] cached failure for division_ring R
[class_instances] (2) ?x_134 : domain R := @integral_domain.to_domain ?x_135 ?x_136
[class_instances] cached failure for integral_domain R
[class_instances] caching failure for domain R
[class_instances] (1) ?x_132 : ring R := @comm_ring.to_ring ?x_133 ?x_134
[class_instances] cached failure for comm_ring R
[class_instances] caching failure for ring R
[class_instances] (0) ?x_63 : semiring R := @ordered_semiring.to_semiring ?x_64 ?x_65
[class_instances] (1) ?x_65 : ordered_semiring R := ?x_71.to_ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_65 : ordered_semiring R := real.ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_65 : ordered_semiring R := ?x_74.to_ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_65 : ordered_semiring R := rat.ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_65 : ordered_semiring R := nat.ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_65 : ordered_semiring R := @ordered_ring.to_ordered_semiring ?x_75 ?x_76
[class_instances] cached failure for ordered_ring R
[class_instances] (1) ?x_65 : ordered_semiring R := @linear_ordered_semiring.to_ordered_semiring ?x_66 ?x_67
[class_instances] (2) ?x_67 : linear_ordered_semiring R := ?x_73.to_linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := nnreal.linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := real.linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := ?x_76.to_linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := rat.linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := nat.linear_ordered_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : linear_ordered_semiring R := @linear_ordered_comm_ring.to_linear_ordered_semiring ?x_77 ?x_78
[class_instances] cached failure for linear_ordered_comm_ring R
[class_instances] (2) ?x_67 : linear_ordered_semiring R := @linear_ordered_ring.to_linear_ordered_semiring ?x_68 ?x_69
[class_instances] cached failure for linear_ordered_ring R
[class_instances] caching failure for linear_ordered_semiring R
[class_instances] (1) ?x_65 : ordered_semiring R := @ordered_comm_semiring.to_ordered_semiring ?x_66 ?x_67
[class_instances] (2) ?x_67 : ordered_comm_semiring R := ?x_73.to_ordered_comm_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : ordered_comm_semiring R := ?x_76.to_ordered_comm_semiring
failed is_def_eq
[class_instances] (2) ?x_67 : ordered_comm_semiring R := @ordered_comm_ring.to_ordered_comm_semiring ?x_77 ?x_78
[class_instances] cached failure for ordered_comm_ring R
[class_instances] caching failure for ordered_comm_semiring R
[class_instances] caching failure for ordered_semiring R
[class_instances] (0) ?x_63 : semiring R := @comm_semiring.to_semiring ?x_64 ?x_65
[class_instances] cached instance for comm_semiring R
_inst_1
[class_instances] caching instance for semiring R
@comm_semiring.to_semiring R _inst_1
[class_instances] cached instance for @char_p R
  (@add_comm_monoid.to_add_monoid R
     (@non_unital_non_assoc_semiring.to_add_comm_monoid R
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  (@mul_one_class.to_has_one R
     (@mul_zero_one_class.to_mul_one_class R
        (@non_assoc_semiring.to_mul_zero_one_class R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  p
_inst_2
[class_instances] (2) ?x_58 : nonempty ℕ := unit_interval.nonempty
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @affine_map.nonempty ?x_66 ?x_67 ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74 ?x_75 ?x_76 ?x_77
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @quiver.rooted_connected.nonempty_path ?x_78 ?x_79 ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := ?x_84.nonempty_sets
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @finset.has_insert.insert.nonempty ?x_85 ?x_86 ?x_87 ?x_88
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Iio_subtype ?x_89 ?x_90 ?x_91 ?x_92
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Ioi_subtype ?x_93 ?x_94 ?x_95 ?x_96
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Iic_subtype ?x_97 ?x_98 ?x_99
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Ici_subtype ?x_100 ?x_101 ?x_102
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.range.nonempty ?x_103 ?x_104 ?x_105 ?x_106
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.image.nonempty ?x_107 ?x_108 ?x_109 ?x_110 ?x_111
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.has_insert.insert.nonempty ?x_112 ?x_113 ?x_114
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.univ.nonempty ?x_115 ?x_116
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @nonempty_lt ?x_117 ?x_118 ?x_119 ?x_120
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @nonempty_gt ?x_121 ?x_122 ?x_123 ?x_124
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @order_dual.nonempty ?x_125 ?x_126
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @prod.nonempty ?x_127 ?x_128 ?x_129 ?x_130
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @add_torsor.nonempty ?x_131 ?x_132 ?x_133 ?x_134
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @affine_map.add_torsor ?x_135 ?x_136 ?x_137 ?x_138 ?x_139 ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @pi.add_torsor ?x_147 ?x_148 ?x_149 ?x_150 ?x_151
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @prod.add_torsor ?x_152 ?x_153 ?x_154 ?x_155 ?x_156 ?x_157 ?x_158 ?x_159
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @add_group_is_add_torsor ?x_160 ?x_161
[class_instances] (4) ?x_161 : add_group ℕ := @power_series.add_group ?x_162 ?x_163
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @mv_power_series.add_group ?x_164 ?x_165 ?x_166
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_monoid_algebra.add_group ?x_167 ?x_168 ?x_169
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @monoid_algebra.add_group ?x_170 ?x_171 ?x_172
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @quotient_add_group.add_group ?x_173 ?x_174 ?x_175 ?x_176
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := real.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @dfinsupp.add_group ?x_177 ?x_178 ?x_179
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @finsupp.add_group ?x_180 ?x_181 ?x_182
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := ?x_185.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @matrix.add_group ?x_186 ?x_187 ?x_188 ?x_189 ?x_190 ?x_191
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @dmatrix.add_group ?x_192 ?x_193 ?x_194 ?x_195 ?x_196 ?x_197
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := ?x_200.to_add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @pi.add_group ?x_201 ?x_202 ?x_203
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := rat.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @prod.add_group ?x_204 ?x_205 ?x_206 ?x_207
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @opposite.add_group ?x_208 ?x_209
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @additive.add_group ?x_210 ?x_211
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_units.add_group ?x_212 ?x_213
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_comm_group.to_add_group ?x_214 ?x_215
[class_instances] (5) ?x_215 : add_comm_group ℕ := real.angle.angle.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @formal_multilinear_series.add_comm_group ?x_216 ?x_217 ?x_218 ?x_219 ?x_220 ?x_221 ?x_222 ?x_223
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @power_series.add_comm_group ?x_224 ?x_225
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @mv_power_series.add_comm_group ?x_226 ?x_227 ?x_228
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @continuous_multilinear_map.add_comm_group ?x_229 ?x_230 ?x_231 ?x_232 ?x_233 ?x_234 ?x_235 ?x_236 ?x_237 ?x_238 ?x_239
  ?x_240
  ?x_241
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @normed_group_hom.add_comm_group ?x_242 ?x_243 ?x_244 ?x_245
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @affine_map.add_comm_group ?x_246 ?x_247 ?x_248 ?x_249 ?x_250 ?x_251 ?x_252 ?x_253 ?x_254 ?x_255
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @module.dual.add_comm_group ?x_256 ?x_257 ?x_258 ?x_259 ?x_260
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @alternating_map.add_comm_group ?x_261 ?x_262 ?x_263 ?x_264 ?x_265 ?x_266 ?x_267 ?x_268 ?x_269 ?x_270
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @multilinear_map.add_comm_group ?x_271 ?x_272 ?x_273 ?x_274 ?x_275 ?x_276 ?x_277 ?x_278 ?x_279 ?x_280
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := punit.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @continuous_linear_map.add_comm_group ?x_281 ?x_282 ?x_283 ?x_284 ?x_285 ?x_286 ?x_287 ?x_288 ?x_289 ?x_290 ?x_291
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @quotient_add_group.add_comm_group ?x_292 ?x_293 ?x_294
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := real.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @restrict_scalars.add_comm_group ?x_295 ?x_296 ?x_297 ?x_298
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @tensor_product.add_comm_group ?x_299 ?x_300 ?x_301 ?x_302 ?x_303 ?x_304 ?x_305 ?x_306
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @submodule.quotient.add_comm_group ?x_307 ?x_308 ?x_309 ?x_310 ?x_311 ?x_312
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @linear_map.add_comm_group ?x_313 ?x_314 ?x_315 ?x_316 ?x_317 ?x_318 ?x_319 ?x_320
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @dfinsupp.add_comm_group ?x_321 ?x_322 ?x_323
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @finsupp.add_comm_group ?x_324 ?x_325 ?x_326
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := ?x_332.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @matrix.add_comm_group ?x_333 ?x_334 ?x_335 ?x_336 ?x_337 ?x_338
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @dmatrix.add_comm_group ?x_339 ?x_340 ?x_341 ?x_342 ?x_343 ?x_344
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := ?x_347.to_add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @pi.add_comm_group ?x_348 ?x_349 ?x_350
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := fin.add_comm_group ?x_351
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := rat.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @add_monoid_hom.add_comm_group ?x_352 ?x_353 ?x_354 ?x_355
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @prod.add_comm_group ?x_356 ?x_357 ?x_358 ?x_359
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @opposite.add_comm_group ?x_360 ?x_361
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @additive.add_comm_group ?x_362 ?x_363
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @add_units.add_comm_group ?x_364 ?x_365
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @normed_group.to_add_comm_group ?x_366 ?x_367
[class_instances] (6) ?x_367 : normed_group ℕ := complex.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @continuous_multilinear_map.to_normed_group ?x_368 ?x_369 ?x_370 ?x_371 ?x_372 ?x_373 ?x_374 ?x_375 ?x_376 ?x_377 ?x_378
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @continuous_linear_map.to_normed_group ?x_379 ?x_380 ?x_381 ?x_382 ?x_383 ?x_384 ?x_385 ?x_386
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @normed_group_hom.to_normed_group ?x_387 ?x_388 ?x_389 ?x_390
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @restrict_scalars.normed_group ?x_391 ?x_392 ?x_393 ?x_394
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @pi.normed_group ?x_395 ?x_396 ?x_397 ?x_398
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @prod.normed_group ?x_399 ?x_400 ?x_401 ?x_402
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := ?x_408.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := ?x_411.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := real.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @normed_linear_ordered_group.to_normed_group ?x_412 ?x_413
[class_instances] (7) ?x_413 : normed_linear_ordered_group ℕ := @normed_linear_ordered_field.to_normed_linear_ordered_group ?x_414 ?x_415
[class_instances] (8) ?x_415 : normed_linear_ordered_field ℕ := real.normed_linear_ordered_field
failed is_def_eq
[class_instances] (8) ?x_415 : normed_linear_ordered_field ℕ := rat.normed_linear_ordered_field
failed is_def_eq
[class_instances] caching failure for normed_linear_ordered_field ℕ
[class_instances] caching failure for normed_linear_ordered_group ℕ
[class_instances] (6) ?x_367 : normed_group ℕ := @normed_ring.to_normed_group ?x_368 ?x_369
[class_instances] (7) ?x_369 : normed_ring ℕ := @continuous_linear_map.to_normed_ring ?x_370 ?x_371 ?x_372 ?x_373 ?x_374
failed is_def_eq
[class_instances] (7) ?x_369 : normed_ring ℕ := @prod.normed_ring ?x_375 ?x_376 ?x_377 ?x_378
failed is_def_eq
[class_instances] (7) ?x_369 : normed_ring ℕ := ?x_384.normed_ring
failed is_def_eq
[class_instances] (7) ?x_369 : normed_ring ℕ := @normed_comm_ring.to_normed_ring ?x_385 ?x_386
[class_instances] (8) ?x_386 : normed_comm_ring ℕ := int.normed_comm_ring
failed is_def_eq
[class_instances] (8) ?x_386 : normed_comm_ring ℕ := @normed_field.to_normed_comm_ring ?x_387 ?x_388
[class_instances] (9) ?x_388 : normed_field ℕ := complex.normed_field
failed is_def_eq
[class_instances] (9) ?x_388 : normed_field ℕ := rat.normed_field
failed is_def_eq
[class_instances] (9) ?x_388 : normed_field ℕ := real.normed_field
failed is_def_eq
[class_instances] (9) ?x_388 : normed_field ℕ := @normed_linear_ordered_field.to_normed_field ?x_389 ?x_390
[class_instances] cached failure for normed_linear_ordered_field ℕ
[class_instances] (9) ?x_388 : normed_field ℕ := @nondiscrete_normed_field.to_normed_field ?x_389 ?x_390
[class_instances] (10) ?x_390 : nondiscrete_normed_field ℕ := complex.nondiscrete_normed_field
failed is_def_eq
[class_instances] (10) ?x_390 : nondiscrete_normed_field ℕ := rat.nondiscrete_normed_field
failed is_def_eq
[class_instances] (10) ?x_390 : nondiscrete_normed_field ℕ := real.nondiscrete_normed_field
failed is_def_eq
[class_instances] (10) ?x_390 : nondiscrete_normed_field ℕ := @is_R_or_C.to_nondiscrete_normed_field ?x_391 ?x_392
[class_instances] (11) ?x_392 : is_R_or_C ℕ := complex.is_R_or_C
failed is_def_eq
[class_instances] (11) ?x_392 : is_R_or_C ℕ := real.is_R_or_C
failed is_def_eq
[class_instances] caching failure for is_R_or_C ℕ
[class_instances] caching failure for nondiscrete_normed_field ℕ
[class_instances] caching failure for normed_field ℕ
[class_instances] caching failure for normed_comm_ring ℕ
[class_instances] caching failure for normed_ring ℕ
[class_instances] caching failure for normed_group ℕ
[class_instances] (5) ?x_215 : add_comm_group ℕ := @semi_normed_group.to_add_comm_group ?x_216 ?x_217
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @continuous_linear_map.to_semi_normed_group ?x_218 ?x_219 ?x_220 ?x_221 ?x_222 ?x_223 ?x_224 ?x_225
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @normed_group_hom.to_semi_normed_group ?x_226 ?x_227 ?x_228 ?x_229
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @restrict_scalars.semi_normed_group ?x_230 ?x_231 ?x_232 ?x_233
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @pi.semi_normed_group ?x_234 ?x_235 ?x_236 ?x_237
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @prod.semi_normed_group ?x_238 ?x_239 ?x_240 ?x_241
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := ?x_247.semi_normed_group
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := ?x_250.semi_normed_group
failed is_def_eq
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @semi_normed_ring.to_semi_normed_group ?x_251 ?x_252
[class_instances] (7) ?x_252 : semi_normed_ring ℕ := @continuous_linear_map.to_semi_normed_ring ?x_253 ?x_254 ?x_255 ?x_256 ?x_257
failed is_def_eq
[class_instances] (7) ?x_252 : semi_normed_ring ℕ := @prod.semi_normed_ring ?x_258 ?x_259 ?x_260 ?x_261
failed is_def_eq
[class_instances] (7) ?x_252 : semi_normed_ring ℕ := ?x_267.semi_normed_ring
failed is_def_eq
[class_instances] (7) ?x_252 : semi_normed_ring ℕ := @semi_normed_comm_ring.to_semi_normed_ring ?x_268 ?x_269
[class_instances] (8) ?x_269 : semi_normed_comm_ring ℕ := @normed_comm_ring.to_semi_normed_comm_ring ?x_270 ?x_271
[class_instances] cached failure for normed_comm_ring ℕ
[class_instances] caching failure for semi_normed_comm_ring ℕ
[class_instances] (7) ?x_252 : semi_normed_ring ℕ := @normed_ring.to_semi_normed_ring ?x_253 ?x_254
[class_instances] cached failure for normed_ring ℕ
[class_instances] caching failure for semi_normed_ring ℕ
[class_instances] (6) ?x_217 : semi_normed_group ℕ := @normed_group.to_semi_normed_group ?x_218 ?x_219
[class_instances] cached failure for normed_group ℕ
[class_instances] caching failure for semi_normed_group ℕ
[class_instances] (5) ?x_215 : add_comm_group ℕ := @add_group_with_zero_nhd.to_add_comm_group ?x_216 ?x_217
[class_instances] (5) ?x_215 : add_comm_group ℕ := @nonneg_add_comm_group.to_add_comm_group ?x_216 ?x_217
[class_instances] (6) ?x_217 : nonneg_add_comm_group ℕ := @linear_nonneg_ring.to_nonneg_add_comm_group ?x_218 ?x_219
[class_instances] (6) ?x_217 : nonneg_add_comm_group ℕ := @nonneg_ring.to_nonneg_add_comm_group ?x_218 ?x_219
[class_instances] (7) ?x_219 : nonneg_ring ℕ := @linear_nonneg_ring.to_nonneg_ring ?x_220 ?x_221
[class_instances] caching failure for nonneg_ring ℕ
[class_instances] caching failure for nonneg_add_comm_group ℕ
[class_instances] (5) ?x_215 : add_comm_group ℕ := @linear_ordered_add_comm_group.to_add_comm_group ?x_216 ?x_217
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := real.linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := ?x_223.to_linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := ?x_226.to_linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := rat.linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := int.linear_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := @additive.linear_ordered_add_comm_group ?x_227 ?x_228
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := @order_dual.linear_ordered_add_comm_group ?x_229 ?x_230
failed is_def_eq
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := @normed_linear_ordered_group.to_linear_ordered_add_comm_group ?x_231 ?x_232
[class_instances] cached failure for normed_linear_ordered_group ℕ
[class_instances] (6) ?x_217 : linear_ordered_add_comm_group ℕ := @linear_ordered_ring.to_linear_ordered_add_comm_group ?x_218 ?x_219
[class_instances] (7) ?x_219 : linear_ordered_ring ℕ := ?x_225.to_linear_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_219 : linear_ordered_ring ℕ := real.linear_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_219 : linear_ordered_ring ℕ := ?x_228.to_linear_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_219 : linear_ordered_ring ℕ := rat.linear_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_219 : linear_ordered_ring ℕ := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_229 ?x_230
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := ?x_236.to_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := real.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := ?x_239.to_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := int.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_230 : linear_ordered_comm_ring ℕ := @linear_ordered_field.to_linear_ordered_comm_ring ?x_240 ?x_241
[class_instances] (9) ?x_241 : linear_ordered_field ℕ := real.linear_ordered_field
failed is_def_eq
[class_instances] (9) ?x_241 : linear_ordered_field ℕ := rat.linear_ordered_field
failed is_def_eq
[class_instances] (9) ?x_241 : linear_ordered_field ℕ := @normed_linear_ordered_field.to_linear_ordered_field ?x_242 ?x_243
[class_instances] cached failure for normed_linear_ordered_field ℕ
[class_instances] caching failure for linear_ordered_field ℕ
[class_instances] caching failure for linear_ordered_comm_ring ℕ
[class_instances] caching failure for linear_ordered_ring ℕ
[class_instances] caching failure for linear_ordered_add_comm_group ℕ
[class_instances] (5) ?x_215 : add_comm_group ℕ := @ordered_add_comm_group.to_add_comm_group ?x_216 ?x_217
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @pi.ordered_add_comm_group ?x_218 ?x_219 ?x_220
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := real.ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := ?x_226.to_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := ?x_229.to_ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := rat.ordered_add_comm_group
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @additive.ordered_add_comm_group ?x_230 ?x_231
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @prod.ordered_add_comm_group ?x_232 ?x_233 ?x_234 ?x_235
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @order_dual.ordered_add_comm_group ?x_236 ?x_237
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @add_units.ordered_add_comm_group ?x_238 ?x_239
failed is_def_eq
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @ordered_ring.to_ordered_add_comm_group ?x_240 ?x_241
[class_instances] (7) ?x_241 : ordered_ring ℕ := ?x_247.to_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_241 : ordered_ring ℕ := real.ordered_ring
failed is_def_eq
[class_instances] (7) ?x_241 : ordered_ring ℕ := ?x_250.to_ordered_ring
failed is_def_eq
[class_instances] (7) ?x_241 : ordered_ring ℕ := rat.ordered_ring
failed is_def_eq
[class_instances] (7) ?x_241 : ordered_ring ℕ := @linear_ordered_ring.to_ordered_ring ?x_251 ?x_252
[class_instances] cached failure for linear_ordered_ring ℕ
[class_instances] (7) ?x_241 : ordered_ring ℕ := @ordered_comm_ring.to_ordered_ring ?x_242 ?x_243
[class_instances] (8) ?x_243 : ordered_comm_ring ℕ := ?x_249.to_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_243 : ordered_comm_ring ℕ := ?x_252.to_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_243 : ordered_comm_ring ℕ := @linear_ordered_comm_ring.to_ordered_comm_ring ?x_253 ?x_254
[class_instances] cached failure for linear_ordered_comm_ring ℕ
[class_instances] caching failure for ordered_comm_ring ℕ
[class_instances] caching failure for ordered_ring ℕ
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @nonneg_add_comm_group.to_ordered_add_comm_group ?x_218 ?x_219
[class_instances] cached failure for nonneg_add_comm_group ℕ
[class_instances] (6) ?x_217 : ordered_add_comm_group ℕ := @linear_ordered_add_comm_group.to_ordered_add_comm_group ?x_218 ?x_219
[class_instances] cached failure for linear_ordered_add_comm_group ℕ
[class_instances] caching failure for ordered_add_comm_group ℕ
[class_instances] (5) ?x_215 : add_comm_group ℕ := @ring.to_add_comm_group ?x_216 ?x_217
[class_instances] (6) ?x_217 : ring ℕ := @power_series.ring ?x_218 ?x_219
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @mv_power_series.ring ?x_220 ?x_221 ?x_222
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @algebra.tensor_product.tensor_product.ring ?x_223 ?x_224 ?x_225 ?x_226 ?x_227 ?x_228 ?x_229 ?x_230
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @polynomial.ring ?x_231 ?x_232
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @add_monoid_algebra.ring ?x_233 ?x_234 ?x_235 ?x_236
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @monoid_algebra.ring ?x_237 ?x_238 ?x_239 ?x_240
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := ?x_246.to_ring
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @continuous_linear_map.ring ?x_247 ?x_248 ?x_249 ?x_250 ?x_251 ?x_252 ?x_253
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := real.ring
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @cau_seq.ring ?x_254 ?x_255 ?x_256 ?x_257 ?x_258 ?x_259
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @ring_quot.ring ?x_260 ?x_261 ?x_262
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @algebra.comap.ring ?x_263 ?x_264 ?x_265 ?x_266
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := ?x_269.to_ring
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @prod.ring ?x_270 ?x_271 ?x_272 ?x_273
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @linear_map.endomorphism_ring ?x_274 ?x_275 ?x_276 ?x_277 ?x_278
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @matrix.ring ?x_279 ?x_280 ?x_281 ?x_282 ?x_283
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @pi.ring ?x_284 ?x_285 ?x_286
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := int.ring
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @opposite.ring ?x_287 ?x_288
failed is_def_eq
[class_instances] (6) ?x_217 : ring ℕ := @normed_ring.to_ring ?x_289 ?x_290
[class_instances] cached failure for normed_ring ℕ
[class_instances] (6) ?x_217 : ring ℕ := @semi_normed_ring.to_ring ?x_218 ?x_219
[class_instances] cached failure for semi_normed_ring ℕ
[class_instances] (6) ?x_217 : ring ℕ := @nonneg_ring.to_ring ?x_218 ?x_219
[class_instances] cached failure for nonneg_ring ℕ
[class_instances] (6) ?x_217 : ring ℕ := @ordered_ring.to_ring ?x_218 ?x_219
[class_instances] cached failure for ordered_ring ℕ
[class_instances] (6) ?x_217 : ring ℕ := @division_ring.to_ring ?x_218 ?x_219
[class_instances] (7) ?x_219 : division_ring ℕ := real.division_ring
failed is_def_eq
[class_instances] (7) ?x_219 : division_ring ℕ := rat.division_ring
failed is_def_eq
[class_instances] (7) ?x_219 : division_ring ℕ := @field.to_division_ring ?x_220 ?x_221
[class_instances] (8) ?x_221 : field ℕ := @fraction_ring.field ?x_222 ?x_223
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @localization_map.codomain.field ?x_224 ?x_225 ?x_226 ?x_227 ?x_228 ?x_229
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @perfect_closure.field ?x_230 ?x_231 ?x_232 ?x_233 ?x_234
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @zmod.field ?x_235 ?x_236
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := complex.field
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := real.field
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @local_ring.residue_field.field ?x_237 ?x_238 ?x_239
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := rat.field
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @opposite.field ?x_240 ?x_241
failed is_def_eq
[class_instances] (8) ?x_221 : field ℕ := @normed_field.to_field ?x_242 ?x_243
[class_instances] cached failure for normed_field ℕ
[class_instances] (8) ?x_221 : field ℕ := @linear_ordered_field.to_field ?x_222 ?x_223
[class_instances] cached failure for linear_ordered_field ℕ
[class_instances] caching failure for field ℕ
[class_instances] caching failure for division_ring ℕ
[class_instances] (6) ?x_217 : ring ℕ := @domain.to_ring ?x_218 ?x_219
[class_instances] (7) ?x_219 : domain ℕ := real.domain
failed is_def_eq
[class_instances] (7) ?x_219 : domain ℕ := @linear_nonneg_ring.to_domain ?x_220 ?x_221
[class_instances] (7) ?x_219 : domain ℕ := @linear_ordered_ring.to_domain ?x_220 ?x_221
[class_instances] cached failure for linear_ordered_ring ℕ
[class_instances] (7) ?x_219 : domain ℕ := @division_ring.to_domain ?x_220 ?x_221
[class_instances] cached failure for division_ring ℕ
[class_instances] (7) ?x_219 : domain ℕ := @integral_domain.to_domain ?x_220 ?x_221
[class_instances] (8) ?x_221 : integral_domain ℕ := @localization_map.integral_domain_of_local_at_prime ?x_222 ?x_223 ?x_224 ?x_225
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @integral_closure.integral_domain ?x_226 ?x_227 ?x_228 ?x_229 ?x_230
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @power_series.integral_domain ?x_231 ?x_232
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @mv_polynomial.integral_domain ?x_233 ?x_234 ?x_235
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @polynomial.integral_domain ?x_236 ?x_237
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := ?x_243.integral_domain
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := real.integral_domain
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @ideal.quotient.integral_domain ?x_244 ?x_245 ?x_246 ?x_247
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := ?x_250.integral_domain
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := rat.integral_domain
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @opposite.integral_domain ?x_251 ?x_252
failed is_def_eq
[class_instances] (8) ?x_221 : integral_domain ℕ := @linear_ordered_comm_ring.to_integral_domain ?x_253 ?x_254
[class_instances] cached failure for linear_ordered_comm_ring ℕ
[class_instances] (8) ?x_221 : integral_domain ℕ := @field.to_integral_domain ?x_222 ?x_223
[class_instances] cached failure for field ℕ
[class_instances] (8) ?x_221 : integral_domain ℕ := @euclidean_domain.integral_domain ?x_222 ?x_223
[class_instances] (9) ?x_223 : euclidean_domain ℕ := @polynomial.euclidean_domain ?x_224 ?x_225
failed is_def_eq
[class_instances] (9) ?x_223 : euclidean_domain ℕ := int.euclidean_domain
failed is_def_eq
[class_instances] (9) ?x_223 : euclidean_domain ℕ := @field.to_euclidean_domain ?x_226 ?x_227
[class_instances] cached failure for field ℕ
[class_instances] caching failure for euclidean_domain ℕ
[class_instances] caching failure for integral_domain ℕ
[class_instances] caching failure for domain ℕ
[class_instances] (6) ?x_217 : ring ℕ := @comm_ring.to_ring ?x_218 ?x_219
[class_instances] (7) ?x_219 : comm_ring ℕ := @localization.comm_ring ?x_220 ?x_221 ?x_222
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @localization_map.codomain.comm_ring ?x_223 ?x_224 ?x_225 ?x_226 ?x_227 ?x_228
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @perfect_closure.comm_ring ?x_229 ?x_230 ?x_231 ?x_232 ?x_233
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @power_series.comm_ring ?x_234 ?x_235
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @mv_power_series.comm_ring ?x_236 ?x_237 ?x_238
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @algebra.tensor_product.tensor_product.comm_ring ?x_239 ?x_240 ?x_241 ?x_242 ?x_243 ?x_244 ?x_245 ?x_246
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := zmod.comm_ring ?x_247
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := fin.comm_ring ?x_248
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := punit.comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @mv_polynomial.comm_ring ?x_249 ?x_250 ?x_251
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @polynomial.comm_ring ?x_252 ?x_253
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @add_monoid_algebra.comm_ring ?x_254 ?x_255 ?x_256 ?x_257
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @monoid_algebra.comm_ring ?x_258 ?x_259 ?x_260 ?x_261
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := ?x_267.to_comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := complex.comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := real.comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @cau_seq.completion.Cauchy.comm_ring ?x_268 ?x_269 ?x_270 ?x_271 ?x_272 ?x_273
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @cau_seq.comm_ring ?x_274 ?x_275 ?x_276 ?x_277 ?x_278 ?x_279
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @ring_quot.comm_ring ?x_280 ?x_281 ?x_282
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @ideal.quotient.comm_ring ?x_283 ?x_284 ?x_285
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @algebra.comap.comm_ring ?x_286 ?x_287 ?x_288 ?x_289
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := ?x_292.to_comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @prod.comm_ring ?x_293 ?x_294 ?x_295 ?x_296
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @pi.comm_ring ?x_297 ?x_298 ?x_299
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := rat.comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := int.comm_ring
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @opposite.comm_ring ?x_300 ?x_301
failed is_def_eq
[class_instances] (7) ?x_219 : comm_ring ℕ := @semi_normed_comm_ring.to_comm_ring ?x_302 ?x_303
[class_instances] cached failure for semi_normed_comm_ring ℕ
[class_instances] (7) ?x_219 : comm_ring ℕ := @euclidean_domain.to_comm_ring ?x_220 ?x_221
[class_instances] cached failure for euclidean_domain ℕ
[class_instances] (7) ?x_219 : comm_ring ℕ := @ordered_comm_ring.to_comm_ring ?x_220 ?x_221
[class_instances] cached failure for ordered_comm_ring ℕ
[class_instances] (7) ?x_219 : comm_ring ℕ := @field.to_comm_ring ?x_220 ?x_221
[class_instances] cached failure for field ℕ
[class_instances] (7) ?x_219 : comm_ring ℕ := @integral_domain.to_comm_ring ?x_220 ?x_221
[class_instances] cached failure for integral_domain ℕ
[class_instances] caching failure for comm_ring ℕ
[class_instances] caching failure for ring ℕ
[class_instances] caching failure for add_comm_group ℕ
[class_instances] caching failure for add_group ℕ
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @normed_add_torsor.to_add_torsor ?x_135 ?x_136 ?x_137 ?x_138 ?x_139
[class_instances] (4) ?x_139 : @normed_add_torsor ?x_135 ℕ ?x_137 ?x_138 := @normed_group.normed_add_torsor ?x_140 ?x_141
[class_instances] cached failure for normed_group ℕ
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @semi_normed_add_torsor.to_add_torsor ?x_135 ?x_136 ?x_137 ?x_138 ?x_139
[class_instances] (4) ?x_139 : @semi_normed_add_torsor ?x_135 ℕ ?x_137 ?x_138 := @semi_normed_group.normed_add_torsor ?x_140 ?x_141
[class_instances] cached failure for semi_normed_group ℕ
[class_instances] (4) ?x_139 : @semi_normed_add_torsor ?x_135 ℕ ?x_137 ?x_138 := @normed_add_torsor.to_semi_normed_add_torsor ?x_140 ?x_141 ?x_142 ?x_143 ?x_144
[class_instances] (5) ?x_144 : @normed_add_torsor ?x_140 ℕ ?x_142 ?x_143 := @normed_group.normed_add_torsor ?x_145 ?x_146
[class_instances] cached failure for normed_group ℕ
[class_instances] (2) ?x_58 : nonempty ℕ := @nontrivial.to_nonempty ?x_66 ?x_67
[class_instances] (3) ?x_67 : nontrivial ℕ := @power_series.subalgebra.nontrivial ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @power_series.nontrivial ?x_71 ?x_72
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @mv_power_series.subalgebra.nontrivial ?x_73 ?x_74 ?x_75 ?x_76 ?x_77
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @mv_power_series.nontrivial ?x_78 ?x_79 ?x_80
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @zmod.nontrivial ?x_81 ?x_82
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := ordinal.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @polynomial.subalgebra.nontrivial ?x_83 ?x_84 ?x_85 ?x_86 ?x_87 ?x_88
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @polynomial.nontrivial ?x_89 ?x_90 ?x_91
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @add_monoid_algebra.nontrivial ?x_92 ?x_93 ?x_94 ?x_95 ?x_96
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @monoid_algebra.nontrivial ?x_97 ?x_98 ?x_99 ?x_100 ?x_101
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @subalgebra.nontrivial ?x_102 ?x_103 ?x_104 ?x_105 ?x_106 ?x_107 ?x_108
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := cardinal.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := ennreal.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := real.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @ideal.nontrivial ?x_109 ?x_110 ?x_111
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @associates.nontrivial ?x_112 ?x_113 ?x_114
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := ?x_118.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @subsemiring.nontrivial ?x_119 ?x_120 ?x_121 ?x_122
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @submodule.nontrivial ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 ?x_128
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @linear_map.module.End.nontrivial ?x_129 ?x_130 ?x_131 ?x_132 ?x_133 ?x_134
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @finsupp.nontrivial ?x_135 ?x_136 ?x_137 ?x_138 ?x_139
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @matrix.nontrivial ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @add_subgroup.nontrivial ?x_148 ?x_149 ?x_150
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @subgroup.nontrivial ?x_151 ?x_152 ?x_153
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @add_submonoid.nontrivial ?x_154 ?x_155 ?x_156
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @submonoid.nontrivial ?x_157 ?x_158 ?x_159
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @order_dual.nontrivial ?x_160 ?x_161
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := @fin.nontrivial ?x_162
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := rat.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := int.nontrivial
failed is_def_eq
[class_instances] (3) ?x_67 : nontrivial ℕ := nat.nontrivial
[class_instances] caching instance for nontrivial ℕ
nat.nontrivial
[class_instances] caching instance for nonempty ℕ
@nontrivial.to_nonempty ℕ nat.nontrivial
[class_instances] caching instance for @char_p (ℕ → R)
  (@add_comm_monoid.to_add_monoid (ℕ → R)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid (ℕ → R)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  (@mul_one_class.to_has_one (ℕ → R)
     (@mul_zero_one_class.to_mul_one_class (ℕ → R)
        (@non_assoc_semiring.to_mul_zero_one_class (ℕ → R)
           (@semiring.to_non_assoc_semiring (ℕ → R)
              (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))))))
  p
@char_p.pi ℕ (@nontrivial.to_nonempty ℕ nat.nontrivial) R (@comm_semiring.to_semiring R _inst_1) p _inst_2
[class_instances] caching instance for @char_p ↥(@ring.perfection R _inst_1 p hp _inst_2)
  (@add_comm_monoid.to_add_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@non_unital_non_assoc_semiring.to_add_comm_monoid ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  (@mul_one_class.to_has_one ↥(@ring.perfection R _inst_1 p hp _inst_2)
     (@mul_zero_one_class.to_mul_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
        (@non_assoc_semiring.to_mul_zero_one_class ↥(@ring.perfection R _inst_1 p hp _inst_2)
           (@semiring.to_non_assoc_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
              (@comm_semiring.to_semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
                 (@ring.perfection R _inst_1 p hp _inst_2).to_comm_semiring)))))
  p
@char_p.subsemiring (ℕ → R)
  (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))
  p
  (@char_p.pi ℕ (@nontrivial.to_nonempty ℕ nat.nontrivial) R (@comm_semiring.to_semiring R _inst_1) p _inst_2)
  (@ring.perfection R _inst_1 p hp _inst_2)
perfection.lean:110:39
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring R := _inst_1
[class_instances] caching instance for comm_semiring R
_inst_1
perfection.lean:110:39
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : fact (nat.prime p) := hp
[class_instances] caching instance for fact (nat.prime p)
hp
perfection.lean:110:39
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @char_p R
  (@add_comm_monoid.to_add_monoid R
     (@non_unital_non_assoc_semiring.to_add_comm_monoid R
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  (@mul_one_class.to_has_one R
     (@mul_zero_one_class.to_mul_one_class R
        (@non_assoc_semiring.to_mul_zero_one_class R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  p := _inst_2
[class_instances] caching instance for @char_p R
  (@add_comm_monoid.to_add_monoid R
     (@non_unital_non_assoc_semiring.to_add_comm_monoid R
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  (@mul_one_class.to_has_one R
     (@mul_zero_one_class.to_mul_one_class R
        (@non_assoc_semiring.to_mul_zero_one_class R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  p
_inst_2
perfection.lean:110:62
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @power_series.semiring ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @mv_power_series.semiring ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @algebra.tensor_product.tensor_product.semiring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @polynomial.semiring ?x_14 ?x_15
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @add_monoid_algebra.semiring ?x_16 ?x_17 ?x_18 ?x_19
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @monoid_algebra.semiring ?x_20 ?x_21 ?x_22 ?x_23
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := ?x_29.to_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @submodule.semiring ?x_30 ?x_31 ?x_32 ?x_33 ?x_34
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := real.semiring
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @ring_quot.semiring ?x_35 ?x_36 ?x_37
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := @algebra.comap.semiring ?x_38 ?x_39 ?x_40 ?x_41
failed is_def_eq
[class_instances] (0) ?x_0 : semiring ↥(@ring.perfection R _inst_1 p hp _inst_2) := ?x_44.to_semiring
[class_instances] caching instance for semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
(@ring.perfection R _inst_1 p hp _inst_2).to_semiring
perfection.lean:110:62
[class_instances] cached instance for semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
(@ring.perfection R _inst_1 p hp _inst_2).to_semiring
perfection.lean:110:69
[class_instances] cached instance for comm_semiring R
_inst_1
perfection.lean:110:69
[class_instances] cached instance for fact (nat.prime p)
hp
perfection.lean:110:69
[class_instances] cached instance for @char_p R
  (@add_comm_monoid.to_add_monoid R
     (@non_unital_non_assoc_semiring.to_add_comm_monoid R
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  (@mul_one_class.to_has_one R
     (@mul_zero_one_class.to_mul_one_class R
        (@non_assoc_semiring.to_mul_zero_one_class R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  p
_inst_2
perfection.lean:110:85
[class_instances] cached instance for semiring ↥(@ring.perfection R _inst_1 p hp _inst_2)
(@ring.perfection R _inst_1 p hp _inst_2).to_semiring
perfection.lean:110:98
[class_instances] cached instance for comm_semiring R
_inst_1
perfection.lean:110:98
[class_instances] cached instance for fact (nat.prime p)
hp
perfection.lean:110:98
[class_instances] cached instance for @char_p R
  (@add_comm_monoid.to_add_monoid R
     (@non_unital_non_assoc_semiring.to_add_comm_monoid R
        (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  (@mul_one_class.to_has_one R
     (@mul_zero_one_class.to_mul_one_class R
        (@non_assoc_semiring.to_mul_zero_one_class R
           (@semiring.to_non_assoc_semiring R (@comm_semiring.to_semiring R _inst_1)))))
  p
_inst_2
All Messages (18)