gistfile1.txt

scratch5.lean:393:0: information trace output
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_2 : @module ?x_0 (Π (i : ι), E i) ?x_1 := @pi.module ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_6 : ring ?x_5 := @prod.ring ?x_8 ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_6 : ring ?x_5 := @normed_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : normed_ring ?x_12 := @normed_field.to_normed_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : normed_field ?x_14 := _inst_1
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @pi.module (?x_16 i) (?x_17 i) (?x_18 i) (?x_19 i) (?x_20 i)
failed is_def_eq
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @prod.module (?x_21 i) (?x_22 i) (?x_23 i) (?x_24 i) (?x_25 i) (?x_26 i)
failed is_def_eq
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @lc.module (?x_27 i) (?x_28 i) (?x_29 i) (?x_30 i)
failed is_def_eq
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @vector_space.to_module (?x_31 i) (?x_32 i) (?x_33 i) (?x_34 i)
failed is_def_eq
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @ring.to_module (?x_35 i) (?x_36 i)
failed is_def_eq
[class_instances] (3) ?x_15 : normed_field ?x_14 := real.normed_field
failed is_def_eq
[class_instances] (2) ?x_13 : normed_ring ?x_12 := @prod.normed_ring ?x_14 ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (1) ?x_6 : ring ?x_5 := @pi.ring ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_6 : ring ?x_5 := real.ring
failed is_def_eq
[class_instances] (1) ?x_6 : ring ?x_5 := @cau_seq.ring ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16
[class_instances] (2) ?x_12 : discrete_linear_ordered_field ?x_11 := real.discrete_linear_ordered_field
[class_instances] (2) ?x_14 : ring ?x_13 := @prod.ring ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (2) ?x_14 : ring ?x_13 := @normed_ring.to_ring ?x_21 ?x_22
[class_instances] (3) ?x_22 : normed_ring ?x_21 := @normed_field.to_normed_ring ?x_23 ?x_24
[class_instances] (4) ?x_24 : normed_field ?x_23 := _inst_1
[class_instances] (2) ?x_16 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_15 := @abs_is_absolute_value ?x_25 ?x_26
failed is_def_eq
[class_instances] (4) ?x_24 : normed_field ?x_23 := real.normed_field
failed is_def_eq
[class_instances] (3) ?x_22 : normed_ring ?x_21 := @prod.normed_ring ?x_23 ?x_24 ?x_25 ?x_26
failed is_def_eq
[class_instances] (2) ?x_14 : ring ?x_13 := @pi.ring ?x_17 ?x_18 ?x_19
failed is_def_eq
[class_instances] (2) ?x_14 : ring ?x_13 := real.ring
failed is_def_eq
[class_instances] (2) ?x_14 : ring ?x_13 := @cau_seq.ring ?x_20 ?x_21 ?x_22 ?x_23 ?x_24 ?x_25
[class_instances] (3) ?x_21 : discrete_linear_ordered_field ?x_20 := real.discrete_linear_ordered_field
[class_instances] (3) ?x_23 : ring ?x_22 := @prod.ring ?x_26 ?x_27 ?x_28 ?x_29
failed is_def_eq
[class_instances] (3) ?x_23 : ring ?x_22 := @normed_ring.to_ring ?x_30 ?x_31
[class_instances] (4) ?x_31 : normed_ring ?x_30 := @normed_field.to_normed_ring ?x_32 ?x_33
[class_instances] (5) ?x_33 : normed_field ?x_32 := _inst_1
[class_instances] (3) ?x_25 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_24 := @abs_is_absolute_value ?x_34 ?x_35
failed is_def_eq
[class_instances] (5) ?x_33 : normed_field ?x_32 := real.normed_field
failed is_def_eq
[class_instances] (4) ?x_31 : normed_ring ?x_30 := @prod.normed_ring ?x_32 ?x_33 ?x_34 ?x_35
failed is_def_eq
[class_instances] (3) ?x_23 : ring ?x_22 := @pi.ring ?x_26 ?x_27 ?x_28
failed is_def_eq
[class_instances] (3) ?x_23 : ring ?x_22 := real.ring
failed is_def_eq
[class_instances] (3) ?x_23 : ring ?x_22 := @cau_seq.ring ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34
[class_instances] (4) ?x_30 : discrete_linear_ordered_field ?x_29 := real.discrete_linear_ordered_field
[class_instances] (4) ?x_32 : ring ?x_31 := @prod.ring ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (4) ?x_32 : ring ?x_31 := @normed_ring.to_ring ?x_39 ?x_40
[class_instances] (5) ?x_40 : normed_ring ?x_39 := @normed_field.to_normed_ring ?x_41 ?x_42
[class_instances] (6) ?x_42 : normed_field ?x_41 := _inst_1
[class_instances] (4) ?x_34 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_33 := @abs_is_absolute_value ?x_43 ?x_44
failed is_def_eq
[class_instances] (6) ?x_42 : normed_field ?x_41 := real.normed_field
failed is_def_eq
[class_instances] (5) ?x_40 : normed_ring ?x_39 := @prod.normed_ring ?x_41 ?x_42 ?x_43 ?x_44
failed is_def_eq
[class_instances] (4) ?x_32 : ring ?x_31 := @pi.ring ?x_35 ?x_36 ?x_37
failed is_def_eq
[class_instances] (4) ?x_32 : ring ?x_31 := real.ring
failed is_def_eq
[class_instances] (4) ?x_32 : ring ?x_31 := @cau_seq.ring ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43
[class_instances] (5) ?x_39 : discrete_linear_ordered_field ?x_38 := real.discrete_linear_ordered_field
[class_instances] (5) ?x_41 : ring ?x_40 := @prod.ring ?x_44 ?x_45 ?x_46 ?x_47
failed is_def_eq
[class_instances] (5) ?x_41 : ring ?x_40 := @normed_ring.to_ring ?x_48 ?x_49
[class_instances] (6) ?x_49 : normed_ring ?x_48 := @normed_field.to_normed_ring ?x_50 ?x_51
[class_instances] (7) ?x_51 : normed_field ?x_50 := _inst_1
[class_instances] (5) ?x_43 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_42 := @abs_is_absolute_value ?x_52 ?x_53
failed is_def_eq
[class_instances] (7) ?x_51 : normed_field ?x_50 := real.normed_field
failed is_def_eq
[class_instances] (6) ?x_49 : normed_ring ?x_48 := @prod.normed_ring ?x_50 ?x_51 ?x_52 ?x_53
failed is_def_eq
[class_instances] (5) ?x_41 : ring ?x_40 := @pi.ring ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (5) ?x_41 : ring ?x_40 := real.ring
failed is_def_eq
[class_instances] (5) ?x_41 : ring ?x_40 := @cau_seq.ring ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52
[class_instances] (6) ?x_48 : discrete_linear_ordered_field ?x_47 := real.discrete_linear_ordered_field
[class_instances] (6) ?x_50 : ring ?x_49 := @prod.ring ?x_53 ?x_54 ?x_55 ?x_56
failed is_def_eq
[class_instances] (6) ?x_50 : ring ?x_49 := @normed_ring.to_ring ?x_57 ?x_58
[class_instances] (7) ?x_58 : normed_ring ?x_57 := @normed_field.to_normed_ring ?x_59 ?x_60
[class_instances] (8) ?x_60 : normed_field ?x_59 := _inst_1
[class_instances] (6) ?x_52 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_51 := @abs_is_absolute_value ?x_61 ?x_62
failed is_def_eq
[class_instances] (8) ?x_60 : normed_field ?x_59 := real.normed_field
failed is_def_eq
[class_instances] (7) ?x_58 : normed_ring ?x_57 := @prod.normed_ring ?x_59 ?x_60 ?x_61 ?x_62
failed is_def_eq
[class_instances] (6) ?x_50 : ring ?x_49 := @pi.ring ?x_53 ?x_54 ?x_55
failed is_def_eq
[class_instances] (6) ?x_50 : ring ?x_49 := real.ring
failed is_def_eq
[class_instances] (6) ?x_50 : ring ?x_49 := @cau_seq.ring ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61
[class_instances] (7) ?x_57 : discrete_linear_ordered_field ?x_56 := real.discrete_linear_ordered_field
[class_instances] (7) ?x_59 : ring ?x_58 := @prod.ring ?x_62 ?x_63 ?x_64 ?x_65
failed is_def_eq
[class_instances] (7) ?x_59 : ring ?x_58 := @normed_ring.to_ring ?x_66 ?x_67
[class_instances] (8) ?x_67 : normed_ring ?x_66 := @normed_field.to_normed_ring ?x_68 ?x_69
[class_instances] (9) ?x_69 : normed_field ?x_68 := _inst_1
[class_instances] (7) ?x_61 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_60 := @abs_is_absolute_value ?x_70 ?x_71
failed is_def_eq
[class_instances] (9) ?x_69 : normed_field ?x_68 := real.normed_field
failed is_def_eq
[class_instances] (8) ?x_67 : normed_ring ?x_66 := @prod.normed_ring ?x_68 ?x_69 ?x_70 ?x_71
failed is_def_eq
[class_instances] (7) ?x_59 : ring ?x_58 := @pi.ring ?x_62 ?x_63 ?x_64
failed is_def_eq
[class_instances] (7) ?x_59 : ring ?x_58 := real.ring
failed is_def_eq
[class_instances] (7) ?x_59 : ring ?x_58 := @cau_seq.ring ?x_65 ?x_66 ?x_67 ?x_68 ?x_69 ?x_70
[class_instances] (8) ?x_66 : discrete_linear_ordered_field ?x_65 := real.discrete_linear_ordered_field
[class_instances] (8) ?x_68 : ring ?x_67 := @prod.ring ?x_71 ?x_72 ?x_73 ?x_74
failed is_def_eq
[class_instances] (8) ?x_68 : ring ?x_67 := @normed_ring.to_ring ?x_75 ?x_76
[class_instances] (9) ?x_76 : normed_ring ?x_75 := @normed_field.to_normed_ring ?x_77 ?x_78
[class_instances] (10) ?x_78 : normed_field ?x_77 := _inst_1
[class_instances] (8) ?x_70 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_69 := @abs_is_absolute_value ?x_79 ?x_80
failed is_def_eq
[class_instances] (10) ?x_78 : normed_field ?x_77 := real.normed_field
failed is_def_eq
[class_instances] (9) ?x_76 : normed_ring ?x_75 := @prod.normed_ring ?x_77 ?x_78 ?x_79 ?x_80
failed is_def_eq
[class_instances] (8) ?x_68 : ring ?x_67 := @pi.ring ?x_71 ?x_72 ?x_73
failed is_def_eq
[class_instances] (8) ?x_68 : ring ?x_67 := real.ring
failed is_def_eq
[class_instances] (8) ?x_68 : ring ?x_67 := @cau_seq.ring ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79
[class_instances] (9) ?x_75 : discrete_linear_ordered_field ?x_74 := real.discrete_linear_ordered_field
[class_instances] (9) ?x_77 : ring ?x_76 := @prod.ring ?x_80 ?x_81 ?x_82 ?x_83
failed is_def_eq
[class_instances] (9) ?x_77 : ring ?x_76 := @normed_ring.to_ring ?x_84 ?x_85
[class_instances] (10) ?x_85 : normed_ring ?x_84 := @normed_field.to_normed_ring ?x_86 ?x_87
[class_instances] (11) ?x_87 : normed_field ?x_86 := _inst_1
[class_instances] (9) ?x_79 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_78 := @abs_is_absolute_value ?x_88 ?x_89
failed is_def_eq
[class_instances] (11) ?x_87 : normed_field ?x_86 := real.normed_field
failed is_def_eq
[class_instances] (10) ?x_85 : normed_ring ?x_84 := @prod.normed_ring ?x_86 ?x_87 ?x_88 ?x_89
failed is_def_eq
[class_instances] (9) ?x_77 : ring ?x_76 := @pi.ring ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (9) ?x_77 : ring ?x_76 := real.ring
failed is_def_eq
[class_instances] (9) ?x_77 : ring ?x_76 := @cau_seq.ring ?x_83 ?x_84 ?x_85 ?x_86 ?x_87 ?x_88
[class_instances] (10) ?x_84 : discrete_linear_ordered_field ?x_83 := real.discrete_linear_ordered_field
[class_instances] (10) ?x_86 : ring ?x_85 := @prod.ring ?x_89 ?x_90 ?x_91 ?x_92
failed is_def_eq
[class_instances] (10) ?x_86 : ring ?x_85 := @normed_ring.to_ring ?x_93 ?x_94
[class_instances] (11) ?x_94 : normed_ring ?x_93 := @normed_field.to_normed_ring ?x_95 ?x_96
[class_instances] (12) ?x_96 : normed_field ?x_95 := _inst_1
[class_instances] (10) ?x_88 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_87 := @abs_is_absolute_value ?x_97 ?x_98
failed is_def_eq
[class_instances] (12) ?x_96 : normed_field ?x_95 := real.normed_field
failed is_def_eq
[class_instances] (11) ?x_94 : normed_ring ?x_93 := @prod.normed_ring ?x_95 ?x_96 ?x_97 ?x_98
failed is_def_eq
[class_instances] (10) ?x_86 : ring ?x_85 := @pi.ring ?x_89 ?x_90 ?x_91
failed is_def_eq
[class_instances] (10) ?x_86 : ring ?x_85 := real.ring
failed is_def_eq
[class_instances] (10) ?x_86 : ring ?x_85 := @cau_seq.ring ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97
[class_instances] (11) ?x_93 : discrete_linear_ordered_field ?x_92 := real.discrete_linear_ordered_field
[class_instances] (11) ?x_95 : ring ?x_94 := @prod.ring ?x_98 ?x_99 ?x_100 ?x_101
failed is_def_eq
[class_instances] (11) ?x_95 : ring ?x_94 := @normed_ring.to_ring ?x_102 ?x_103
[class_instances] (12) ?x_103 : normed_ring ?x_102 := @normed_field.to_normed_ring ?x_104 ?x_105
[class_instances] (13) ?x_105 : normed_field ?x_104 := _inst_1
[class_instances] (11) ?x_97 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_96 := @abs_is_absolute_value ?x_106 ?x_107
failed is_def_eq
[class_instances] (13) ?x_105 : normed_field ?x_104 := real.normed_field
failed is_def_eq
[class_instances] (12) ?x_103 : normed_ring ?x_102 := @prod.normed_ring ?x_104 ?x_105 ?x_106 ?x_107
failed is_def_eq
[class_instances] (11) ?x_95 : ring ?x_94 := @pi.ring ?x_98 ?x_99 ?x_100
failed is_def_eq
[class_instances] (11) ?x_95 : ring ?x_94 := real.ring
failed is_def_eq
[class_instances] (11) ?x_95 : ring ?x_94 := @cau_seq.ring ?x_101 ?x_102 ?x_103 ?x_104 ?x_105 ?x_106
[class_instances] (12) ?x_102 : discrete_linear_ordered_field ?x_101 := real.discrete_linear_ordered_field
[class_instances] (12) ?x_104 : ring ?x_103 := @prod.ring ?x_107 ?x_108 ?x_109 ?x_110
failed is_def_eq
[class_instances] (12) ?x_104 : ring ?x_103 := @normed_ring.to_ring ?x_111 ?x_112
[class_instances] (13) ?x_112 : normed_ring ?x_111 := @normed_field.to_normed_ring ?x_113 ?x_114
[class_instances] (14) ?x_114 : normed_field ?x_113 := _inst_1
[class_instances] (12) ?x_106 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_105 := @abs_is_absolute_value ?x_115 ?x_116
failed is_def_eq
[class_instances] (14) ?x_114 : normed_field ?x_113 := real.normed_field
failed is_def_eq
[class_instances] (13) ?x_112 : normed_ring ?x_111 := @prod.normed_ring ?x_113 ?x_114 ?x_115 ?x_116
failed is_def_eq
[class_instances] (12) ?x_104 : ring ?x_103 := @pi.ring ?x_107 ?x_108 ?x_109
failed is_def_eq
[class_instances] (12) ?x_104 : ring ?x_103 := real.ring
failed is_def_eq
[class_instances] (12) ?x_104 : ring ?x_103 := @cau_seq.ring ?x_110 ?x_111 ?x_112 ?x_113 ?x_114 ?x_115
[class_instances] (13) ?x_111 : discrete_linear_ordered_field ?x_110 := real.discrete_linear_ordered_field
[class_instances] (13) ?x_113 : ring ?x_112 := @prod.ring ?x_116 ?x_117 ?x_118 ?x_119
failed is_def_eq
[class_instances] (13) ?x_113 : ring ?x_112 := @normed_ring.to_ring ?x_120 ?x_121
[class_instances] (14) ?x_121 : normed_ring ?x_120 := @normed_field.to_normed_ring ?x_122 ?x_123
[class_instances] (15) ?x_123 : normed_field ?x_122 := _inst_1
[class_instances] (13) ?x_115 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_114 := @abs_is_absolute_value ?x_124 ?x_125
failed is_def_eq
[class_instances] (15) ?x_123 : normed_field ?x_122 := real.normed_field
failed is_def_eq
[class_instances] (14) ?x_121 : normed_ring ?x_120 := @prod.normed_ring ?x_122 ?x_123 ?x_124 ?x_125
failed is_def_eq
[class_instances] (13) ?x_113 : ring ?x_112 := @pi.ring ?x_116 ?x_117 ?x_118
failed is_def_eq
[class_instances] (13) ?x_113 : ring ?x_112 := real.ring
failed is_def_eq
[class_instances] (13) ?x_113 : ring ?x_112 := @cau_seq.ring ?x_119 ?x_120 ?x_121 ?x_122 ?x_123 ?x_124
[class_instances] (14) ?x_120 : discrete_linear_ordered_field ?x_119 := real.discrete_linear_ordered_field
[class_instances] (14) ?x_122 : ring ?x_121 := @prod.ring ?x_125 ?x_126 ?x_127 ?x_128
failed is_def_eq
[class_instances] (14) ?x_122 : ring ?x_121 := @normed_ring.to_ring ?x_129 ?x_130
[class_instances] (15) ?x_130 : normed_ring ?x_129 := @normed_field.to_normed_ring ?x_131 ?x_132
[class_instances] (16) ?x_132 : normed_field ?x_131 := _inst_1
[class_instances] (14) ?x_124 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_123 := @abs_is_absolute_value ?x_133 ?x_134
failed is_def_eq
[class_instances] (16) ?x_132 : normed_field ?x_131 := real.normed_field
failed is_def_eq
[class_instances] (15) ?x_130 : normed_ring ?x_129 := @prod.normed_ring ?x_131 ?x_132 ?x_133 ?x_134
failed is_def_eq
[class_instances] (14) ?x_122 : ring ?x_121 := @pi.ring ?x_125 ?x_126 ?x_127
failed is_def_eq
[class_instances] (14) ?x_122 : ring ?x_121 := real.ring
failed is_def_eq
[class_instances] (14) ?x_122 : ring ?x_121 := @cau_seq.ring ?x_128 ?x_129 ?x_130 ?x_131 ?x_132 ?x_133
[class_instances] (15) ?x_129 : discrete_linear_ordered_field ?x_128 := real.discrete_linear_ordered_field
[class_instances] (15) ?x_131 : ring ?x_130 := @prod.ring ?x_134 ?x_135 ?x_136 ?x_137
failed is_def_eq
[class_instances] (15) ?x_131 : ring ?x_130 := @normed_ring.to_ring ?x_138 ?x_139
[class_instances] (16) ?x_139 : normed_ring ?x_138 := @normed_field.to_normed_ring ?x_140 ?x_141
[class_instances] (17) ?x_141 : normed_field ?x_140 := _inst_1
[class_instances] (15) ?x_133 : @is_absolute_value ℝ real.discrete_linear_ordered_field α
  (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1))
  ?x_132 := @abs_is_absolute_value ?x_142 ?x_143
failed is_def_eq
[class_instances] (17) ?x_141 : normed_field ?x_140 := real.normed_field
failed is_def_eq
[class_instances] (16) ?x_139 : normed_ring ?x_138 := @prod.normed_ring ?x_140 ?x_141 ?x_142 ?x_143
failed is_def_eq
[class_instances] (15) ?x_131 : ring ?x_130 := @pi.ring ?x_134 ?x_135 ?x_136
failed is_def_eq
[class_instances] (15) ?x_131 : ring ?x_130 := real.ring
failed is_def_eq
[class_instances] (15) ?x_131 : ring ?x_130 := @cau_seq.ring ?x_137 ?x_138 ?x_139 ?x_140 ?x_141 ?x_142
[class_instances] (16) ?x_138 : discrete_linear_ordered_field ?x_137 := real.discrete_linear_ordered_field
[class_instances] (16) ?x_140 : ring ?x_139 := @prod.ring ?x_143 ?x_144 ?x_145 ?x_146
failed is_def_eq
[class_instances] (16) ?x_140 : ring ?x_139 := @normed_ring.to_ring ?x_147 ?x_148
[class_instances] (17) ?x_148 : normed_ring ?x_147 := @normed_field.to_normed_ring ?x_149 ?x_150