max typeclass res

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @topological_add_monoid (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@add_group.to_add_monoid (Π (i : γ), F i) (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i))) := @topological_ring.to_topological_add_monoid ?x_1 ?x_2 ?x_3 ?x_4
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @pi.ring ?x_6 ?x_7 ?x_8
[class_instances] (1) ?x_8 i : ring (F i) := @pi.ring (?x_9 i) (?x_10 i) (?x_11 i)
failed is_def_eq
[class_instances] (1) ?x_8 i : ring (F i) := @nonneg_ring.to_ring (?x_12 i) (?x_13 i)
[class_instances] (2) ?x_13 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_14 i) (?x_15 i)
[class_instances] (1) ?x_8 i : ring (F i) := @domain.to_ring (?x_9 i) (?x_10 i)
[class_instances] (2) ?x_10 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_11 i) (?x_12 i)
[class_instances] (2) ?x_10 i : domain (F i) := @to_domain (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i) (?x_19 i) _
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (2) ?x_10 i : domain (F i) := @division_ring.to_domain (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : division_ring (F i) := @field.to_division_ring (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : field (F i) := @linear_ordered_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_14 i : field (F i) := @discrete_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_17 i) (?x_18 i)
[class_instances] (2) ?x_10 i : domain (F i) := @integral_domain.to_domain (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @field.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : field (F i) := @linear_ordered_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_14 i : field (F i) := @discrete_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_17 i) (?x_18 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_13 i) (?x_14 i) (?x_15 i)
[class_instances] (4) ?x_14 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_16 i) (?x_17 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i) (?x_19 i) _
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (1) ?x_8 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (1) ?x_8 i : ring (F i) := @division_ring.to_ring (?x_9 i) (?x_10 i)
[class_instances] (2) ?x_10 i : division_ring (F i) := @field.to_division_ring (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : field (F i) := @linear_ordered_field.to_field (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_12 i : field (F i) := @discrete_field.to_field (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_15 i) (?x_16 i)
[class_instances] (1) ?x_8 i : ring (F i) := @ordered_ring.to_ring (?x_9 i) (?x_10 i)
[class_instances] (2) ?x_10 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_13 i) (?x_14 i)
[class_instances] (2) ?x_10 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_12 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i) (?x_19 i) _
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (1) ?x_8 i : ring (F i) := @comm_ring.to_ring (?x_9 i) (?x_10 i)
[class_instances] (2) ?x_10 i : comm_ring (F i) := @pi.comm_ring (?x_11 i) (?x_12 i) (?x_13 i)
failed is_def_eq
[class_instances] (2) ?x_10 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (2) ?x_10 i : comm_ring (F i) := @field.to_comm_ring (?x_14 i) (?x_15 i)
[class_instances] (3) ?x_15 i : field (F i) := @linear_ordered_field.to_field (?x_16 i) (?x_17 i)
[class_instances] (4) ?x_17 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_18 i) (?x_19 i)
[class_instances] (3) ?x_15 i : field (F i) := @discrete_field.to_field (?x_16 i) (?x_17 i)
[class_instances] (4) ?x_17 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_18 i) (?x_19 i)
[class_instances] (2) ?x_10 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @field.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : field (F i) := @linear_ordered_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_14 i : field (F i) := @discrete_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_17 i) (?x_18 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_13 i) (?x_14 i) (?x_15 i)
[class_instances] (4) ?x_14 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_16 i) (?x_17 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i) (?x_19 i) _
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @nonneg_ring.to_ring ?x_6 ?x_7
[class_instances] (1) ?x_7 : nonneg_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_nonneg_ring ?x_8 ?x_9
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @domain.to_ring ?x_6 ?x_7
[class_instances] (1) ?x_7 : domain (Π (i : γ), F i) := @linear_nonneg_ring.to_domain ?x_8 ?x_9
[class_instances] (1) ?x_7 : domain (Π (i : γ), F i) := @to_domain ?x_8 ?x_9
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_12 ?x_13
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_12 ?x_13
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15 ?x_16 ?x_17
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15
[class_instances] (1) ?x_7 : domain (Π (i : γ), F i) := @division_ring.to_domain ?x_8 ?x_9
[class_instances] (2) ?x_9 : division_ring (Π (i : γ), F i) := @field.to_division_ring ?x_10 ?x_11
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_14 ?x_15
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_14 ?x_15
[class_instances] (1) ?x_7 : domain (Π (i : γ), F i) := @integral_domain.to_domain ?x_8 ?x_9
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @field.to_integral_domain ?x_10 ?x_11
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_14 ?x_15
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_14 ?x_15
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @discrete_field.to_integral_domain ?x_10 ?x_11 ?x_12
[class_instances] (3) ?x_11 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_13 ?x_14
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @linear_ordered_comm_ring.to_integral_domain ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_12 ?x_13
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15 ?x_16 ?x_17
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := int.ring
failed is_def_eq
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @division_ring.to_ring ?x_6 ?x_7
[class_instances] (1) ?x_7 : division_ring (Π (i : γ), F i) := @field.to_division_ring ?x_8 ?x_9
[class_instances] (2) ?x_9 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_12 ?x_13
[class_instances] (2) ?x_9 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_10 ?x_11
[class_instances] (3) ?x_11 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_12 ?x_13
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @ordered_ring.to_ring ?x_6 ?x_7
[class_instances] (1) ?x_7 : ordered_ring (Π (i : γ), F i) := @nonneg_ring.to_ordered_ring ?x_8 ?x_9
[class_instances] (2) ?x_9 : nonneg_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_nonneg_ring ?x_10 ?x_11
[class_instances] (1) ?x_7 : ordered_ring (Π (i : γ), F i) := @linear_ordered_ring.to_ordered_ring ?x_8 ?x_9
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_12 ?x_13
[class_instances] (2) ?x_9 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_12 ?x_13
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15 ?x_16 ?x_17
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @comm_ring.to_ring ?x_6 ?x_7
[class_instances] (1) ?x_7 : comm_ring (Π (i : γ), F i) := @pi.comm_ring ?x_8 ?x_9 ?x_10
[class_instances] (2) ?x_10 i : comm_ring (F i) := @pi.comm_ring (?x_11 i) (?x_12 i) (?x_13 i)
failed is_def_eq
[class_instances] (2) ?x_10 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (2) ?x_10 i : comm_ring (F i) := @field.to_comm_ring (?x_14 i) (?x_15 i)
[class_instances] (3) ?x_15 i : field (F i) := @linear_ordered_field.to_field (?x_16 i) (?x_17 i)
[class_instances] (4) ?x_17 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_18 i) (?x_19 i)
[class_instances] (3) ?x_15 i : field (F i) := @discrete_field.to_field (?x_16 i) (?x_17 i)
[class_instances] (4) ?x_17 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_18 i) (?x_19 i)
[class_instances] (2) ?x_10 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_11 i) (?x_12 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @field.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : field (F i) := @linear_ordered_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_14 i : field (F i) := @discrete_field.to_field (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_17 i) (?x_18 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_13 i) (?x_14 i) (?x_15 i)
[class_instances] (4) ?x_14 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_16 i) (?x_17 i)
[class_instances] (3) ?x_12 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_13 i) (?x_14 i)
[class_instances] (4) ?x_14 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_15 i) (?x_16 i)
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i) (?x_19 i) _
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_16 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (1) ?x_7 : comm_ring (Π (i : γ), F i) := int.comm_ring
failed is_def_eq
[class_instances] (1) ?x_7 : comm_ring (Π (i : γ), F i) := @field.to_comm_ring ?x_8 ?x_9
[class_instances] (2) ?x_9 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_12 ?x_13
[class_instances] (2) ?x_9 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_10 ?x_11
[class_instances] (3) ?x_11 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_12 ?x_13
[class_instances] (1) ?x_7 : comm_ring (Π (i : γ), F i) := @integral_domain.to_comm_ring ?x_8 ?x_9
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @field.to_integral_domain ?x_10 ?x_11
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_14 ?x_15
[class_instances] (3) ?x_11 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_12 ?x_13
[class_instances] (4) ?x_13 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_14 ?x_15
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @discrete_field.to_integral_domain ?x_10 ?x_11 ?x_12
[class_instances] (3) ?x_11 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_13 ?x_14
[class_instances] (2) ?x_9 : integral_domain (Π (i : γ), F i) := @linear_ordered_comm_ring.to_integral_domain ?x_10 ?x_11
[class_instances] (3) ?x_11 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_12 ?x_13
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15 ?x_16 ?x_17
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (4) ?x_13 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_14 ?x_15
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
failed is_def_eq
[class_instances] (0) ?x_0 : @topological_add_monoid (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@add_group.to_add_monoid (Π (i : γ), F i) (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i))) := @topological_semiring.to_topological_add_monoid ?x_5 ?x_6 ?x_7 ?x_8
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := @with_zero.semiring ?x_10 ?x_11
failed is_def_eq
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := int.semiring
failed is_def_eq
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := nat.semiring
failed is_def_eq
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := @ordered_semiring.to_semiring ?x_12 ?x_13
[class_instances] (1) ?x_13 : ordered_semiring (Π (i : γ), F i) := nat.ordered_semiring
failed is_def_eq
[class_instances] (1) ?x_13 : ordered_semiring (Π (i : γ), F i) := @ordered_ring.to_ordered_semiring ?x_14 ?x_15
[class_instances] (2) ?x_15 : ordered_ring (Π (i : γ), F i) := @nonneg_ring.to_ordered_ring ?x_16 ?x_17
[class_instances] (3) ?x_17 : nonneg_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_nonneg_ring ?x_18 ?x_19
[class_instances] (2) ?x_15 : ordered_ring (Π (i : γ), F i) := @linear_ordered_ring.to_ordered_ring ?x_16 ?x_17
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (4) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (4) ?x_19 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_22 ?x_23 ?x_24 ?x_25
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_22 ?x_23
[class_instances] (1) ?x_13 : ordered_semiring (Π (i : γ), F i) := @linear_ordered_semiring.to_ordered_semiring ?x_14 ?x_15
[class_instances] (2) ?x_15 : linear_ordered_semiring (Π (i : γ), F i) := @linear_ordered_ring.to_linear_ordered_semiring ?x_16 ?x_17
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (4) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (3) ?x_17 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_18 ?x_19
[class_instances] (4) ?x_19 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_22 ?x_23 ?x_24 ?x_25
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_21 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_22 ?x_23
[class_instances] (2) ?x_15 : linear_ordered_semiring (Π (i : γ), F i) := @decidable_linear_ordered_semiring.to_linear_ordered_semiring ?x_16 ?x_17
[class_instances] (3) ?x_17 : decidable_linear_ordered_semiring (Π (i : γ), F i) := nat.decidable_linear_ordered_semiring
failed is_def_eq
[class_instances] (3) ?x_17 : decidable_linear_ordered_semiring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring ?x_18 ?x_19
[class_instances] (4) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (4) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (4) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := @ring.to_semiring ?x_10 ?x_11
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @pi.ring ?x_12 ?x_13 ?x_14
[class_instances] (2) ?x_14 i : ring (F i) := @pi.ring (?x_15 i) (?x_16 i) (?x_17 i)
failed is_def_eq
[class_instances] (2) ?x_14 i : ring (F i) := @nonneg_ring.to_ring (?x_18 i) (?x_19 i)
[class_instances] (3) ?x_19 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_20 i) (?x_21 i)
[class_instances] (2) ?x_14 i : ring (F i) := @domain.to_ring (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_16 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_17 i) (?x_18 i)
[class_instances] (3) ?x_16 i : domain (F i) := @to_domain (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_21 i) (?x_22 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (3) ?x_16 i : domain (F i) := @division_ring.to_domain (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : division_ring (F i) := @field.to_division_ring (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : field (F i) := @linear_ordered_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_23 i) (?x_24 i)
[class_instances] (5) ?x_20 i : field (F i) := @discrete_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_23 i) (?x_24 i)
[class_instances] (3) ?x_16 i : domain (F i) := @integral_domain.to_domain (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @field.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : field (F i) := @linear_ordered_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_23 i) (?x_24 i)
[class_instances] (5) ?x_20 i : field (F i) := @discrete_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_23 i) (?x_24 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_19 i) (?x_20 i) (?x_21 i)
[class_instances] (5) ?x_20 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_22 i) (?x_23 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (2) ?x_14 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (2) ?x_14 i : ring (F i) := @division_ring.to_ring (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_16 i : division_ring (F i) := @field.to_division_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : field (F i) := @linear_ordered_field.to_field (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_21 i) (?x_22 i)
[class_instances] (4) ?x_18 i : field (F i) := @discrete_field.to_field (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_21 i) (?x_22 i)
[class_instances] (2) ?x_14 i : ring (F i) := @ordered_ring.to_ring (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_16 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_19 i) (?x_20 i)
[class_instances] (3) ?x_16 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_21 i) (?x_22 i)
[class_instances] (4) ?x_18 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (2) ?x_14 i : ring (F i) := @comm_ring.to_ring (?x_15 i) (?x_16 i)
[class_instances] (3) ?x_16 i : comm_ring (F i) := @pi.comm_ring (?x_17 i) (?x_18 i) (?x_19 i)
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := @field.to_comm_ring (?x_20 i) (?x_21 i)
[class_instances] (4) ?x_21 i : field (F i) := @linear_ordered_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_21 i : field (F i) := @discrete_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_24 i) (?x_25 i)
[class_instances] (3) ?x_16 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @field.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : field (F i) := @linear_ordered_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_23 i) (?x_24 i)
[class_instances] (5) ?x_20 i : field (F i) := @discrete_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_23 i) (?x_24 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_19 i) (?x_20 i) (?x_21 i)
[class_instances] (5) ?x_20 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_22 i) (?x_23 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @nonneg_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : nonneg_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_nonneg_ring ?x_14 ?x_15
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @domain.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : domain (Π (i : γ), F i) := @linear_nonneg_ring.to_domain ?x_14 ?x_15
[class_instances] (2) ?x_13 : domain (Π (i : γ), F i) := @to_domain ?x_14 ?x_15
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_18 ?x_19
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_18 ?x_19
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (2) ?x_13 : domain (Π (i : γ), F i) := @division_ring.to_domain ?x_14 ?x_15
[class_instances] (3) ?x_15 : division_ring (Π (i : γ), F i) := @field.to_division_ring ?x_16 ?x_17
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_20 ?x_21
[class_instances] (2) ?x_13 : domain (Π (i : γ), F i) := @integral_domain.to_domain ?x_14 ?x_15
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @field.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_20 ?x_21
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @discrete_field.to_integral_domain ?x_16 ?x_17 ?x_18
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_19 ?x_20
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @linear_ordered_comm_ring.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_18 ?x_19
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := int.ring
failed is_def_eq
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @division_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : division_ring (Π (i : γ), F i) := @field.to_division_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_18 ?x_19
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_18 ?x_19
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @ordered_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : ordered_ring (Π (i : γ), F i) := @nonneg_ring.to_ordered_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : nonneg_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_nonneg_ring ?x_16 ?x_17
[class_instances] (2) ?x_13 : ordered_ring (Π (i : γ), F i) := @linear_ordered_ring.to_ordered_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_field.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_18 ?x_19
[class_instances] (3) ?x_15 : linear_ordered_ring (Π (i : γ), F i) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_18 ?x_19
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (1) ?x_11 : ring (Π (i : γ), F i) := @comm_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @pi.comm_ring ?x_14 ?x_15 ?x_16
[class_instances] (3) ?x_16 i : comm_ring (F i) := @pi.comm_ring (?x_17 i) (?x_18 i) (?x_19 i)
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := @field.to_comm_ring (?x_20 i) (?x_21 i)
[class_instances] (4) ?x_21 i : field (F i) := @linear_ordered_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_21 i : field (F i) := @discrete_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_24 i) (?x_25 i)
[class_instances] (3) ?x_16 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @field.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : field (F i) := @linear_ordered_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_23 i) (?x_24 i)
[class_instances] (5) ?x_20 i : field (F i) := @discrete_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_23 i) (?x_24 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_19 i) (?x_20 i) (?x_21 i)
[class_instances] (5) ?x_20 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_22 i) (?x_23 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := int.comm_ring
failed is_def_eq
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @field.to_comm_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_18 ?x_19
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_18 ?x_19
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @integral_domain.to_comm_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @field.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_20 ?x_21
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @discrete_field.to_integral_domain ?x_16 ?x_17 ?x_18
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_19 ?x_20
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @linear_ordered_comm_ring.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_18 ?x_19
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] (0) ?x_9 : semiring (Π (i : γ), F i) := @comm_semiring.to_semiring ?x_10 ?x_11
[class_instances] (1) ?x_11 : comm_semiring (Π (i : γ), F i) := int.comm_semiring
failed is_def_eq
[class_instances] (1) ?x_11 : comm_semiring (Π (i : γ), F i) := nat.comm_semiring
failed is_def_eq
[class_instances] (1) ?x_11 : comm_semiring (Π (i : γ), F i) := @comm_ring.to_comm_semiring ?x_12 ?x_13
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @pi.comm_ring ?x_14 ?x_15 ?x_16
[class_instances] (3) ?x_16 i : comm_ring (F i) := @pi.comm_ring (?x_17 i) (?x_18 i) (?x_19 i)
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (3) ?x_16 i : comm_ring (F i) := @field.to_comm_ring (?x_20 i) (?x_21 i)
[class_instances] (4) ?x_21 i : field (F i) := @linear_ordered_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_21 i : field (F i) := @discrete_field.to_field (?x_22 i) (?x_23 i)
[class_instances] (5) ?x_23 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_24 i) (?x_25 i)
[class_instances] (3) ?x_16 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_17 i) (?x_18 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @field.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : field (F i) := @linear_ordered_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_23 i) (?x_24 i)
[class_instances] (5) ?x_20 i : field (F i) := @discrete_field.to_field (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_23 i) (?x_24 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_19 i) (?x_20 i) (?x_21 i)
[class_instances] (5) ?x_20 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_22 i) (?x_23 i)
[class_instances] (4) ?x_18 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_19 i) (?x_20 i)
[class_instances] (5) ?x_20 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_21 i) (?x_22 i)
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i) (?x_25 i) _
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_23 i) (?x_24 i)
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := int.comm_ring
failed is_def_eq
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @field.to_comm_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_18 ?x_19
[class_instances] (3) ?x_15 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_16 ?x_17
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_18 ?x_19
[class_instances] (2) ?x_13 : comm_ring (Π (i : γ), F i) := @integral_domain.to_comm_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @field.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @linear_ordered_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : linear_ordered_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_20 ?x_21
[class_instances] (4) ?x_17 : field (Π (i : γ), F i) := @discrete_field.to_field ?x_18 ?x_19
[class_instances] (5) ?x_19 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_20 ?x_21
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @discrete_field.to_integral_domain ?x_16 ?x_17 ?x_18
[class_instances] (4) ?x_17 : discrete_field (Π (i : γ), F i) := @discrete_linear_ordered_field.to_discrete_field ?x_19 ?x_20
[class_instances] (3) ?x_15 : integral_domain (Π (i : γ), F i) := @linear_ordered_comm_ring.to_integral_domain ?x_16 ?x_17
[class_instances] (4) ?x_17 : linear_ordered_comm_ring (Π (i : γ), F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_18 ?x_19
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21 ?x_22 ?x_23
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_19 : decidable_linear_ordered_comm_ring (Π (i : γ), F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_20 ?x_21
[class_instances] cached failure for semiring (Π (i : γ), F i)
[class_instances] cached failure for semiring (Π (i : γ), F i)
[class_instances] cached failure for semiring (Π (i : γ), F i)
[class_instances] cached failure for semiring (Π (i : γ), F i)
failed is_def_eq
[class_instances] (0) ?x_0 : @topological_add_monoid (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@add_group.to_add_monoid (Π (i : γ), F i) (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i))) := @topological_add_group.to_topological_add_monoid ?x_9 ?x_10 ?x_11 ?x_12
[class_instances] cached instance for add_group (Π (i : γ), F i)
@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i)
[class_instances] (1) ?x_10 : topological_space (Π (i : γ), F i) := _inst_1 ?x_13
failed is_def_eq
[class_instances] (1) ?x_10 : topological_space (Π (i : γ), F i) := @uniform_space.to_topological_space ?x_14 ?x_15
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := @prod.uniform_space ?x_16 ?x_17 ?x_18 ?x_19
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := @subtype.uniform_space ?x_20 ?x_21 ?x_22
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := int.uniform_space
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := nat.uniform_space
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := bool.uniform_space
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := unit.uniform_space
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := empty.uniform_space
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := @Cauchy.completion_space ?x_23 ?x_24
failed is_def_eq
[class_instances] (2) ?x_15 : uniform_space (Π (i : γ), F i) := @quotient.uniform_space ?x_25 ?x_26
failed is_def_eq
[class_instances] (1) ?x_10 : topological_space (Π (i : γ), F i) := @Pi.topological_space ?x_13 ?x_14 ?x_15
[class_instances] (2) ?x_15 a : topological_space (F a) := _inst_1 (?x_16 a)
[class_instances] (1) ?x_11 : add_group (Π (i : γ), F i) := _inst_2 ?x_17
failed is_def_eq
[class_instances] (1) ?x_11 : add_group (Π (i : γ), F i) := @pi.add_group ?x_18 ?x_19 ?x_20
[class_instances] (2) ?x_20 i : add_group (F i) := _inst_2 (?x_21 i)
[class_instances] (1) ?x_12 : @topological_add_group (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i)) := _inst_3 ?x_22
failed is_def_eq
[class_instances] (1) ?x_12 : @topological_add_group (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i)) := @topological_ring.to_topological_add_group ?x_23 ?x_24 ?x_25 ?x_26
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
[class_instances] cached failure for ring (Π (i : γ), F i)
failed is_def_eq
[class_instances] (1) ?x_12 : @topological_add_group (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i)) := @uniform_add_group.to_topological_add_group ?x_27 ?x_28 ?x_29 ?x_30
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := @prod.uniform_space ?x_32 ?x_33 ?x_34 ?x_35
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := @subtype.uniform_space ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := int.uniform_space
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := nat.uniform_space
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := bool.uniform_space
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := unit.uniform_space
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := empty.uniform_space
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := @Cauchy.completion_space ?x_39 ?x_40
failed is_def_eq
[class_instances] (0) ?x_31 : uniform_space (Π (i : γ), F i) := @quotient.uniform_space ?x_41 ?x_42
failed is_def_eq
[class_instances] cached failure for uniform_space (Π (i : γ), F i)
failed is_def_eq
[class_instances] (2) ?x_20 i : add_group (F i) := @pi.add_group (?x_21 i) (?x_22 i) (?x_23 i)
failed is_def_eq
[class_instances] (2) ?x_20 i : add_group (F i) := @additive.add_group (?x_24 i) (?x_25 i)
failed is_def_eq
[class_instances] (2) ?x_20 i : add_group (F i) := @add_comm_group.to_add_group (?x_26 i) (?x_27 i)
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @pi.add_comm_group (?x_28 i) (?x_29 i) (?x_30 i)
failed is_def_eq
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @module.to_add_comm_group (?x_31 i) (?x_32 i) (?x_33 i) (?x_34 i)
[class_instances] (4) ?x_34 i : @module (?x_31 i) (F i) (?x_33 i) := @pi.module (?x_35 i) (?x_36 i) (?x_37 i) (?x_38 i) (?x_39 i)
failed is_def_eq
[class_instances] (4) ?x_34 i : @module (?x_31 i) (F i) (?x_33 i) := @vector_space.to_module (?x_40 i) (?x_41 i) (?x_42 i) (?x_43 i)
[class_instances] (5) ?x_42 i : field (?x_40 i) := @linear_ordered_field.to_field (?x_44 i) (?x_45 i)
[class_instances] (6) ?x_45 i : linear_ordered_field (?x_44 i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_46 i) (?x_47 i)
[class_instances] (5) ?x_42 i : field (?x_40 i) := @discrete_field.to_field (?x_44 i) (?x_45 i)
[class_instances] (6) ?x_45 i : discrete_field (?x_44 i) := @discrete_linear_ordered_field.to_discrete_field (?x_46 i) (?x_47 i)
[class_instances] (4) ?x_34 i : @module (?x_31 i) (F i) (?x_33 i) := @ring.to_module (?x_35 i) (?x_36 i)
[class_instances] (5) ?x_36 i : ring (F i) := @pi.ring (?x_37 i) (?x_38 i) (?x_39 i)
failed is_def_eq
[class_instances] (5) ?x_36 i : ring (F i) := @nonneg_ring.to_ring (?x_40 i) (?x_41 i)
[class_instances] (6) ?x_41 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_42 i) (?x_43 i)
[class_instances] (5) ?x_36 i : ring (F i) := @domain.to_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_38 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_39 i) (?x_40 i)
[class_instances] (6) ?x_38 i : domain (F i) := @to_domain (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_43 i) (?x_44 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i) (?x_47 i) _
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i)
[class_instances] (6) ?x_38 i : domain (F i) := @division_ring.to_domain (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : division_ring (F i) := @field.to_division_ring (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : field (F i) := @linear_ordered_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_45 i) (?x_46 i)
[class_instances] (8) ?x_42 i : field (F i) := @discrete_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_45 i) (?x_46 i)
[class_instances] (6) ?x_38 i : domain (F i) := @integral_domain.to_domain (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @field.to_integral_domain (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : field (F i) := @linear_ordered_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_45 i) (?x_46 i)
[class_instances] (8) ?x_42 i : field (F i) := @discrete_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_45 i) (?x_46 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_41 i) (?x_42 i) (?x_43 i)
[class_instances] (8) ?x_42 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_44 i) (?x_45 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i) (?x_47 i) _
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i)
[class_instances] (5) ?x_36 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (5) ?x_36 i : ring (F i) := @division_ring.to_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_38 i : division_ring (F i) := @field.to_division_ring (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : field (F i) := @linear_ordered_field.to_field (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_43 i) (?x_44 i)
[class_instances] (7) ?x_40 i : field (F i) := @discrete_field.to_field (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_43 i) (?x_44 i)
[class_instances] (5) ?x_36 i : ring (F i) := @ordered_ring.to_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_38 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_41 i) (?x_42 i)
[class_instances] (6) ?x_38 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_43 i) (?x_44 i)
[class_instances] (7) ?x_40 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i) (?x_47 i) _
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i)
[class_instances] (5) ?x_36 i : ring (F i) := @comm_ring.to_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_38 i : comm_ring (F i) := @pi.comm_ring (?x_39 i) (?x_40 i) (?x_41 i)
failed is_def_eq
[class_instances] (6) ?x_38 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (6) ?x_38 i : comm_ring (F i) := @field.to_comm_ring (?x_42 i) (?x_43 i)
[class_instances] (7) ?x_43 i : field (F i) := @linear_ordered_field.to_field (?x_44 i) (?x_45 i)
[class_instances] (8) ?x_45 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_46 i) (?x_47 i)
[class_instances] (7) ?x_43 i : field (F i) := @discrete_field.to_field (?x_44 i) (?x_45 i)
[class_instances] (8) ?x_45 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_46 i) (?x_47 i)
[class_instances] (6) ?x_38 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @field.to_integral_domain (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : field (F i) := @linear_ordered_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_45 i) (?x_46 i)
[class_instances] (8) ?x_42 i : field (F i) := @discrete_field.to_field (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_45 i) (?x_46 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_41 i) (?x_42 i) (?x_43 i)
[class_instances] (8) ?x_42 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_44 i) (?x_45 i)
[class_instances] (7) ?x_40 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_42 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_43 i) (?x_44 i)
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i) (?x_47 i) _
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_44 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_45 i) (?x_46 i)
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @nonneg_comm_group.to_add_comm_group (?x_28 i) (?x_29 i)
[class_instances] (4) ?x_29 i : nonneg_comm_group (F i) := @linear_nonneg_ring.to_nonneg_comm_group (?x_30 i) (?x_31 i)
[class_instances] (4) ?x_29 i : nonneg_comm_group (F i) := @nonneg_ring.to_nonneg_comm_group (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_31 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_32 i) (?x_33 i)
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @additive.add_comm_group (?x_28 i) (?x_29 i)
failed is_def_eq
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @ring.to_add_comm_group (?x_30 i) (?x_31 i)
[class_instances] (4) ?x_31 i : ring (F i) := @pi.ring (?x_32 i) (?x_33 i) (?x_34 i)
failed is_def_eq
[class_instances] (4) ?x_31 i : ring (F i) := @nonneg_ring.to_ring (?x_35 i) (?x_36 i)
[class_instances] (5) ?x_36 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_37 i) (?x_38 i)
[class_instances] (4) ?x_31 i : ring (F i) := @domain.to_ring (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_33 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_34 i) (?x_35 i)
[class_instances] (5) ?x_33 i : domain (F i) := @to_domain (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_38 i) (?x_39 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i) (?x_42 i) _
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i)
[class_instances] (5) ?x_33 i : domain (F i) := @division_ring.to_domain (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : division_ring (F i) := @field.to_division_ring (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : field (F i) := @linear_ordered_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_40 i) (?x_41 i)
[class_instances] (7) ?x_37 i : field (F i) := @discrete_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_40 i) (?x_41 i)
[class_instances] (5) ?x_33 i : domain (F i) := @integral_domain.to_domain (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @field.to_integral_domain (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : field (F i) := @linear_ordered_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_40 i) (?x_41 i)
[class_instances] (7) ?x_37 i : field (F i) := @discrete_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_40 i) (?x_41 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_36 i) (?x_37 i) (?x_38 i)
[class_instances] (7) ?x_37 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_39 i) (?x_40 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i) (?x_42 i) _
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i)
[class_instances] (4) ?x_31 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (4) ?x_31 i : ring (F i) := @division_ring.to_ring (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_33 i : division_ring (F i) := @field.to_division_ring (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : field (F i) := @linear_ordered_field.to_field (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_38 i) (?x_39 i)
[class_instances] (6) ?x_35 i : field (F i) := @discrete_field.to_field (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_38 i) (?x_39 i)
[class_instances] (4) ?x_31 i : ring (F i) := @ordered_ring.to_ring (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_33 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_36 i) (?x_37 i)
[class_instances] (5) ?x_33 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_38 i) (?x_39 i)
[class_instances] (6) ?x_35 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i) (?x_42 i) _
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i)
[class_instances] (4) ?x_31 i : ring (F i) := @comm_ring.to_ring (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_33 i : comm_ring (F i) := @pi.comm_ring (?x_34 i) (?x_35 i) (?x_36 i)
failed is_def_eq
[class_instances] (5) ?x_33 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (5) ?x_33 i : comm_ring (F i) := @field.to_comm_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_38 i : field (F i) := @linear_ordered_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_41 i) (?x_42 i)
[class_instances] (6) ?x_38 i : field (F i) := @discrete_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_40 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_41 i) (?x_42 i)
[class_instances] (5) ?x_33 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @field.to_integral_domain (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : field (F i) := @linear_ordered_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_40 i) (?x_41 i)
[class_instances] (7) ?x_37 i : field (F i) := @discrete_field.to_field (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_40 i) (?x_41 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_36 i) (?x_37 i) (?x_38 i)
[class_instances] (7) ?x_37 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_39 i) (?x_40 i)
[class_instances] (6) ?x_35 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_37 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i) (?x_42 i) _
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_39 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_40 i) (?x_41 i)
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @decidable_linear_ordered_comm_group.to_add_comm_group (?x_28 i) (?x_29 i)
[class_instances] (4) ?x_29 i : decidable_linear_ordered_comm_group (F i) := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (4) ?x_29 i : decidable_linear_ordered_comm_group (F i) := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_31 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_32 i) (?x_33 i) (?x_34 i) _
[class_instances] (5) ?x_31 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_31 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_32 i) (?x_33 i)
[class_instances] (3) ?x_27 i : add_comm_group (F i) := @ordered_comm_group.to_add_comm_group (?x_28 i) (?x_29 i)
[class_instances] (4) ?x_29 i : ordered_comm_group (F i) := @nonneg_comm_group.to_ordered_comm_group (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_31 i : nonneg_comm_group (F i) := @linear_nonneg_ring.to_nonneg_comm_group (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_31 i : nonneg_comm_group (F i) := @nonneg_ring.to_nonneg_comm_group (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_33 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_34 i) (?x_35 i)
[class_instances] (4) ?x_29 i : ordered_comm_group (F i) := @ordered_ring.to_ordered_comm_group (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_31 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_33 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_34 i) (?x_35 i)
[class_instances] (5) ?x_31 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_33 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_33 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_34 i) (?x_35 i)
[class_instances] (7) ?x_35 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_33 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_34 i) (?x_35 i)
[class_instances] (7) ?x_35 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_36 i) (?x_37 i)
[class_instances] (8) ?x_37 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_38 i) (?x_39 i) (?x_40 i) _
[class_instances] (8) ?x_37 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_37 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (4) ?x_29 i : ordered_comm_group (F i) := @decidable_linear_ordered_comm_group.to_ordered_comm_group (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_31 i : decidable_linear_ordered_comm_group (F i) := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (5) ?x_31 i : decidable_linear_ordered_comm_group (F i) := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_34 i) (?x_35 i) (?x_36 i) _
[class_instances] (6) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (1) ?x_11 : add_group (Π (i : γ), F i) := @additive.add_group ?x_17 ?x_18
failed is_def_eq
[class_instances] (1) ?x_11 : add_group (Π (i : γ), F i) := @add_comm_group.to_add_group ?x_19 ?x_20
[class_instances] (2) ?x_20 : add_comm_group (Π (i : γ), F i) := @pi.add_comm_group ?x_21 ?x_22 ?x_23
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @pi.add_comm_group (?x_24 i) (?x_25 i) (?x_26 i)
failed is_def_eq
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @module.to_add_comm_group (?x_27 i) (?x_28 i) (?x_29 i) (?x_30 i)
[class_instances] (4) ?x_30 i : @module (?x_27 i) (F i) (?x_29 i) := @pi.module (?x_31 i) (?x_32 i) (?x_33 i) (?x_34 i) (?x_35 i)
failed is_def_eq
[class_instances] (4) ?x_30 i : @module (?x_27 i) (F i) (?x_29 i) := @vector_space.to_module (?x_36 i) (?x_37 i) (?x_38 i) (?x_39 i)
[class_instances] (5) ?x_38 i : field (?x_36 i) := @linear_ordered_field.to_field (?x_40 i) (?x_41 i)
[class_instances] (6) ?x_41 i : linear_ordered_field (?x_40 i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_42 i) (?x_43 i)
[class_instances] (5) ?x_38 i : field (?x_36 i) := @discrete_field.to_field (?x_40 i) (?x_41 i)
[class_instances] (6) ?x_41 i : discrete_field (?x_40 i) := @discrete_linear_ordered_field.to_discrete_field (?x_42 i) (?x_43 i)
[class_instances] (4) ?x_30 i : @module (?x_27 i) (F i) (?x_29 i) := @ring.to_module (?x_31 i) (?x_32 i)
[class_instances] (5) ?x_32 i : ring (F i) := @pi.ring (?x_33 i) (?x_34 i) (?x_35 i)
failed is_def_eq
[class_instances] (5) ?x_32 i : ring (F i) := @nonneg_ring.to_ring (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_37 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_38 i) (?x_39 i)
[class_instances] (5) ?x_32 i : ring (F i) := @domain.to_ring (?x_33 i) (?x_34 i)
[class_instances] (6) ?x_34 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_35 i) (?x_36 i)
[class_instances] (6) ?x_34 i : domain (F i) := @to_domain (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i) (?x_43 i) _
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i)
[class_instances] (6) ?x_34 i : domain (F i) := @division_ring.to_domain (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : division_ring (F i) := @field.to_division_ring (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : field (F i) := @linear_ordered_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_38 i : field (F i) := @discrete_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_41 i) (?x_42 i)
[class_instances] (6) ?x_34 i : domain (F i) := @integral_domain.to_domain (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @field.to_integral_domain (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : field (F i) := @linear_ordered_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_38 i : field (F i) := @discrete_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_41 i) (?x_42 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_37 i) (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_38 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_40 i) (?x_41 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i) (?x_43 i) _
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i)
[class_instances] (5) ?x_32 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (5) ?x_32 i : ring (F i) := @division_ring.to_ring (?x_33 i) (?x_34 i)
[class_instances] (6) ?x_34 i : division_ring (F i) := @field.to_division_ring (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : field (F i) := @linear_ordered_field.to_field (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_36 i : field (F i) := @discrete_field.to_field (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_39 i) (?x_40 i)
[class_instances] (5) ?x_32 i : ring (F i) := @ordered_ring.to_ring (?x_33 i) (?x_34 i)
[class_instances] (6) ?x_34 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_34 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_39 i) (?x_40 i)
[class_instances] (7) ?x_36 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i) (?x_43 i) _
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i)
[class_instances] (5) ?x_32 i : ring (F i) := @comm_ring.to_ring (?x_33 i) (?x_34 i)
[class_instances] (6) ?x_34 i : comm_ring (F i) := @pi.comm_ring (?x_35 i) (?x_36 i) (?x_37 i)
failed is_def_eq
[class_instances] (6) ?x_34 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (6) ?x_34 i : comm_ring (F i) := @field.to_comm_ring (?x_38 i) (?x_39 i)
[class_instances] (7) ?x_39 i : field (F i) := @linear_ordered_field.to_field (?x_40 i) (?x_41 i)
[class_instances] (8) ?x_41 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_42 i) (?x_43 i)
[class_instances] (7) ?x_39 i : field (F i) := @discrete_field.to_field (?x_40 i) (?x_41 i)
[class_instances] (8) ?x_41 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_42 i) (?x_43 i)
[class_instances] (6) ?x_34 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @field.to_integral_domain (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : field (F i) := @linear_ordered_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_41 i) (?x_42 i)
[class_instances] (8) ?x_38 i : field (F i) := @discrete_field.to_field (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_41 i) (?x_42 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_37 i) (?x_38 i) (?x_39 i)
[class_instances] (8) ?x_38 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_40 i) (?x_41 i)
[class_instances] (7) ?x_36 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_37 i) (?x_38 i)
[class_instances] (8) ?x_38 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_39 i) (?x_40 i)
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i) (?x_43 i) _
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (9) ?x_40 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_41 i) (?x_42 i)
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @nonneg_comm_group.to_add_comm_group (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_25 i : nonneg_comm_group (F i) := @linear_nonneg_ring.to_nonneg_comm_group (?x_26 i) (?x_27 i)
[class_instances] (4) ?x_25 i : nonneg_comm_group (F i) := @nonneg_ring.to_nonneg_comm_group (?x_26 i) (?x_27 i)
[class_instances] (5) ?x_27 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_28 i) (?x_29 i)
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @additive.add_comm_group (?x_24 i) (?x_25 i)
failed is_def_eq
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @ring.to_add_comm_group (?x_26 i) (?x_27 i)
[class_instances] (4) ?x_27 i : ring (F i) := @pi.ring (?x_28 i) (?x_29 i) (?x_30 i)
failed is_def_eq
[class_instances] (4) ?x_27 i : ring (F i) := @nonneg_ring.to_ring (?x_31 i) (?x_32 i)
[class_instances] (5) ?x_32 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_33 i) (?x_34 i)
[class_instances] (4) ?x_27 i : ring (F i) := @domain.to_ring (?x_28 i) (?x_29 i)
[class_instances] (5) ?x_29 i : domain (F i) := @linear_nonneg_ring.to_domain (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_29 i : domain (F i) := @to_domain (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i) (?x_38 i) _
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i)
[class_instances] (5) ?x_29 i : domain (F i) := @division_ring.to_domain (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : division_ring (F i) := @field.to_division_ring (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : field (F i) := @linear_ordered_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_33 i : field (F i) := @discrete_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_36 i) (?x_37 i)
[class_instances] (5) ?x_29 i : domain (F i) := @integral_domain.to_domain (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @field.to_integral_domain (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : field (F i) := @linear_ordered_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_33 i : field (F i) := @discrete_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_32 i) (?x_33 i) (?x_34 i)
[class_instances] (7) ?x_33 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_35 i) (?x_36 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i) (?x_38 i) _
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i)
[class_instances] (4) ?x_27 i : ring (F i) := int.ring
failed is_def_eq
[class_instances] (4) ?x_27 i : ring (F i) := @division_ring.to_ring (?x_28 i) (?x_29 i)
[class_instances] (5) ?x_29 i : division_ring (F i) := @field.to_division_ring (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : field (F i) := @linear_ordered_field.to_field (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_31 i : field (F i) := @discrete_field.to_field (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_34 i) (?x_35 i)
[class_instances] (4) ?x_27 i : ring (F i) := @ordered_ring.to_ring (?x_28 i) (?x_29 i)
[class_instances] (5) ?x_29 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_32 i) (?x_33 i)
[class_instances] (5) ?x_29 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_31 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i) (?x_38 i) _
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i)
[class_instances] (4) ?x_27 i : ring (F i) := @comm_ring.to_ring (?x_28 i) (?x_29 i)
[class_instances] (5) ?x_29 i : comm_ring (F i) := @pi.comm_ring (?x_30 i) (?x_31 i) (?x_32 i)
failed is_def_eq
[class_instances] (5) ?x_29 i : comm_ring (F i) := int.comm_ring
failed is_def_eq
[class_instances] (5) ?x_29 i : comm_ring (F i) := @field.to_comm_ring (?x_33 i) (?x_34 i)
[class_instances] (6) ?x_34 i : field (F i) := @linear_ordered_field.to_field (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_37 i) (?x_38 i)
[class_instances] (6) ?x_34 i : field (F i) := @discrete_field.to_field (?x_35 i) (?x_36 i)
[class_instances] (7) ?x_36 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_37 i) (?x_38 i)
[class_instances] (5) ?x_29 i : comm_ring (F i) := @integral_domain.to_comm_ring (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @field.to_integral_domain (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : field (F i) := @linear_ordered_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_36 i) (?x_37 i)
[class_instances] (7) ?x_33 i : field (F i) := @discrete_field.to_field (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_36 i) (?x_37 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @discrete_field.to_integral_domain (?x_32 i) (?x_33 i) (?x_34 i)
[class_instances] (7) ?x_33 i : discrete_field (F i) := @discrete_linear_ordered_field.to_discrete_field (?x_35 i) (?x_36 i)
[class_instances] (6) ?x_31 i : integral_domain (F i) := @linear_ordered_comm_ring.to_integral_domain (?x_32 i) (?x_33 i)
[class_instances] (7) ?x_33 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i) (?x_38 i) _
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_35 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_36 i) (?x_37 i)
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @decidable_linear_ordered_comm_group.to_add_comm_group (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_25 i : decidable_linear_ordered_comm_group (F i) := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (4) ?x_25 i : decidable_linear_ordered_comm_group (F i) := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group (?x_26 i) (?x_27 i)
[class_instances] (5) ?x_27 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_28 i) (?x_29 i) (?x_30 i) _
[class_instances] (5) ?x_27 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_27 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_28 i) (?x_29 i)
[class_instances] (3) ?x_23 i : add_comm_group (F i) := @ordered_comm_group.to_add_comm_group (?x_24 i) (?x_25 i)
[class_instances] (4) ?x_25 i : ordered_comm_group (F i) := @nonneg_comm_group.to_ordered_comm_group (?x_26 i) (?x_27 i)
[class_instances] (5) ?x_27 i : nonneg_comm_group (F i) := @linear_nonneg_ring.to_nonneg_comm_group (?x_28 i) (?x_29 i)
[class_instances] (5) ?x_27 i : nonneg_comm_group (F i) := @nonneg_ring.to_nonneg_comm_group (?x_28 i) (?x_29 i)
[class_instances] (6) ?x_29 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_30 i) (?x_31 i)
[class_instances] (4) ?x_25 i : ordered_comm_group (F i) := @ordered_ring.to_ordered_comm_group (?x_26 i) (?x_27 i)
[class_instances] (5) ?x_27 i : ordered_ring (F i) := @nonneg_ring.to_ordered_ring (?x_28 i) (?x_29 i)
[class_instances] (6) ?x_29 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_30 i) (?x_31 i)
[class_instances] (5) ?x_27 i : ordered_ring (F i) := @linear_ordered_ring.to_ordered_ring (?x_28 i) (?x_29 i)
[class_instances] (6) ?x_29 i : linear_ordered_ring (F i) := @linear_nonneg_ring.to_linear_ordered_ring (?x_30 i) (?x_31 i)
[class_instances] (6) ?x_29 i : linear_ordered_ring (F i) := @linear_ordered_field.to_linear_ordered_ring (?x_30 i) (?x_31 i)
[class_instances] (7) ?x_31 i : linear_ordered_field (F i) := @discrete_linear_ordered_field.to_linear_ordered_field (?x_32 i) (?x_33 i)
[class_instances] (6) ?x_29 i : linear_ordered_ring (F i) := @linear_ordered_comm_ring.to_linear_ordered_ring (?x_30 i) (?x_31 i)
[class_instances] (7) ?x_31 i : linear_ordered_comm_ring (F i) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (?x_32 i) (?x_33 i)
[class_instances] (8) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_34 i) (?x_35 i) (?x_36 i) _
[class_instances] (8) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (8) ?x_33 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_34 i) (?x_35 i)
[class_instances] (4) ?x_25 i : ordered_comm_group (F i) := @decidable_linear_ordered_comm_group.to_ordered_comm_group (?x_26 i) (?x_27 i)
[class_instances] (5) ?x_27 i : decidable_linear_ordered_comm_group (F i) := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (5) ?x_27 i : decidable_linear_ordered_comm_group (F i) := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group (?x_28 i) (?x_29 i)
[class_instances] (6) ?x_29 i : decidable_linear_ordered_comm_ring (F i) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring (?x_30 i) (?x_31 i) (?x_32 i) _
[class_instances] (6) ?x_29 i : decidable_linear_ordered_comm_ring (F i) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_29 i : decidable_linear_ordered_comm_ring (F i) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring (?x_30 i) (?x_31 i)
[class_instances] (2) ?x_20 : add_comm_group (Π (i : γ), F i) := @module.to_add_comm_group ?x_21 ?x_22 ?x_23 ?x_24
[class_instances] (3) ?x_24 : @module ?x_21 (Π (i : γ), F i) ?x_23 := @pi.module ?x_25 ?x_26 ?x_27 ?x_28 ?x_29
[class_instances] (4) ?x_28 : ring ?x_27 := @pi.ring ?x_30 ?x_31 ?x_32
[class_instances] (5) ?x_32 i : ring (?x_31 i) := @pi.ring (?x_33 i) (?x_34 i) (?x_35 i)
[class_instances] (6) ?x_35 i i_1 : ring (?x_34 i i_1) := @pi.ring (?x_36 i i_1) (?x_37 i i_1) (?x_38 i i_1)
[class_instances] (7) ?x_38 i i_1 i_2 : ring (?x_37 i i_1 i_2) := @pi.ring (?x_39 i i_1 i_2) (?x_40 i i_1 i_2) (?x_41 i i_1 i_2)
[class_instances] (8) ?x_41 i i_1 i_2 i_3 : ring (?x_40 i i_1 i_2 i_3) := @pi.ring (?x_42 i i_1 i_2 i_3) (?x_43 i i_1 i_2 i_3) (?x_44 i i_1 i_2 i_3)
[class_instances] (9) ?x_44 i i_1 i_2 i_3 i_4 : ring (?x_43 i i_1 i_2 i_3 i_4) := @pi.ring (?x_45 i i_1 i_2 i_3 i_4) (?x_46 i i_1 i_2 i_3 i_4) (?x_47 i i_1 i_2 i_3 i_4)
[class_instances] (10) ?x_47 i i_1 i_2 i_3 i_4 i_5 : ring (?x_46 i i_1 i_2 i_3 i_4 i_5) := @pi.ring (?x_48 i i_1 i_2 i_3 i_4 i_5) (?x_49 i i_1 i_2 i_3 i_4 i_5) (?x_50 i i_1 i_2 i_3 i_4 i_5)
[class_instances] (11) ?x_50 i i_1 i_2 i_3 i_4 i_5 i_6 : ring (?x_49 i i_1 i_2 i_3 i_4 i_5 i_6) := @pi.ring (?x_51 i i_1 i_2 i_3 i_4 i_5 i_6) (?x_52 i i_1 i_2 i_3 i_4 i_5 i_6) (?x_53 i i_1 i_2 i_3 i_4 i_5 i_6)
[class_instances] (12) ?x_53 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 : ring (?x_52 i i_1 i_2 i_3 i_4 i_5 i_6 i_7) := @pi.ring (?x_54 i i_1 i_2 i_3 i_4 i_5 i_6 i_7) (?x_55 i i_1 i_2 i_3 i_4 i_5 i_6 i_7)
  (?x_56 i i_1 i_2 i_3 i_4 i_5 i_6 i_7)
[class_instances] (13) ?x_56 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 : ring (?x_55 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8) := @pi.ring (?x_57 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8) (?x_58 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8)
  (?x_59 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8)
[class_instances] (14) ?x_59 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 : ring (?x_58 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9) := @pi.ring (?x_60 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9) (?x_61 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9)
  (?x_62 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9)
[class_instances] (15) ?x_62 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 : ring (?x_61 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10) := @pi.ring (?x_63 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10) (?x_64 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10)
  (?x_65 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10)
[class_instances] (16) ?x_65 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 : ring (?x_64 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11) := @pi.ring (?x_66 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11) (?x_67 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11)
  (?x_68 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11)
[class_instances] (17) ?x_68 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 : ring (?x_67 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12) := @pi.ring (?x_69 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12)
  (?x_70 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12)
  (?x_71 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12)
[class_instances] (18) ?x_71 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 : ring (?x_70 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13) := @pi.ring (?x_72 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13)
  (?x_73 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13)
  (?x_74 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13)
[class_instances] (19) ?x_74 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 : ring (?x_73 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14) := @pi.ring (?x_75 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14)
  (?x_76 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14)
  (?x_77 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14)
[class_instances] (20) ?x_77 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 : ring (?x_76 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15) := @pi.ring (?x_78 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15)
  (?x_79 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15)
  (?x_80 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15)
[class_instances] (21) ?x_80 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 : ring (?x_79 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16) := @pi.ring (?x_81 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16)
  (?x_82 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16)
  (?x_83 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16)
[class_instances] (22) ?x_83 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 : ring (?x_82 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17) := @pi.ring (?x_84 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17)
  (?x_85 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17)
  (?x_86 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17)
[class_instances] (23) ?x_86 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 : ring (?x_85 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18) := @pi.ring (?x_87 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18)
  (?x_88 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18)
  (?x_89 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18)
[class_instances] (24) ?x_89 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 : ring (?x_88 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19) := @pi.ring (?x_90 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19)
  (?x_91 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19)
  (?x_92 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19)
[class_instances] (25) ?x_92 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 : ring (?x_91 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20) := @pi.ring (?x_93 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20)
  (?x_94 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20)
  (?x_95 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20)
[class_instances] (26) ?x_95 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 : ring (?x_94 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21) := @pi.ring (?x_96 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21)
  (?x_97 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21)
  (?x_98 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21)
[class_instances] (27) ?x_98 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 : ring (?x_97 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22) := @pi.ring (?x_99 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22)
  (?x_100 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22)
  (?x_101 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22)
[class_instances] (28) ?x_101 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23 : ring
  (?x_100 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23) := @pi.ring
  (?x_102 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23)
  (?x_103 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23)
  (?x_104 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23)
[class_instances] (29) ?x_104 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23 i_24 : ring
  (?x_103 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24) := @pi.ring
  (?x_105 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24)
  (?x_106 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24)
  (?x_107 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24)
[class_instances] (30) ?x_107 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23 i_24
  i_25 : ring
  (?x_106 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24
     i_25) := @pi.ring
  (?x_108 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24
     i_25)
  (?x_109 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24
     i_25)
  (?x_110 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11 i_12 i_13 i_14 i_15 i_16 i_17 i_18 i_19 i_20 i_21 i_22 i_23
     i_24
     i_25)
scratch4.lean:8:36: error

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')