subsingleton?

Updating  Stop Updating
polynomial.lean:1012:0: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring α := @polynomial.comm_semiring ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := rat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @canonically_ordered_comm_semiring.to_comm_semiring ?x_4 ?x_5
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := @with_top.canonically_ordered_comm_semiring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := nat.canonically_ordered_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := int.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := nat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @comm_ring.to_comm_semiring ?x_1 ?x_2
[class_instances] (1) ?x_2 : comm_ring α := _inst_2
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_one ℕ
nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_to_format tactic_state := rat.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := @buffer.has_to_format ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := int.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic.rcases_patt.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic.rcases_patt_inverted.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := @array.has_to_format ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := subsingleton_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := fun_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := param_info.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := occurrences.has_to_format
failed is_def_eq
[class_instances] (0) ?x_0 : has_to_format tactic_state := tactic_state.has_to_format
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_add ℕ
nat.has_add
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_one ℕ
nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_add ℕ
nat.has_add
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_one ℕ
nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_add ℕ
nat.has_add
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_one ℕ
nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_one ℕ := @polynomial.has_one ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := rat.has_one
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @cau_seq.has_one ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @finsupp.has_one ?x_10 ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @with_top.has_one ?x_17 ?x_18 ?x_19
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @with_bot.has_one ?x_20 ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @units.has_one ?x_22 ?x_23
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := @fin.has_one ?x_24
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := int.has_one
failed is_def_eq
[class_instances] (0) ?x_0 : has_one ℕ := nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_add ℕ := @polynomial.has_add ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := rat.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := @cau_seq.has_add ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := pnat.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := @finsupp.has_add ?x_10 ?x_11 ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := @submodule.has_add ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := @multiset.has_add ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := unsigned.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := @fin.has_add ?x_22
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := int.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := options.has_add
failed is_def_eq
[class_instances] (0) ?x_0 : has_add ℕ := nat.has_add
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_one ℕ
nat.has_one
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_add ℕ
nat.has_add
polynomial.lean:1012:8: information trace output

[class_instances] cached instance for has_add ℕ
nat.has_add
polynomial.lean:1012:33: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 a b : decidable (a = b) := _inst_1 (?x_1 a b) (?x_2 a b)
polynomial.lean:1012:33: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring α := @polynomial.comm_semiring ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := rat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @canonically_ordered_comm_semiring.to_comm_semiring ?x_4 ?x_5
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := @with_top.canonically_ordered_comm_semiring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := nat.canonically_ordered_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := int.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := nat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @comm_ring.to_comm_semiring ?x_1 ?x_2
[class_instances] (1) ?x_2 : comm_ring α := _inst_2
polynomial.lean:1012:40: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring α := @polynomial.comm_semiring ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := rat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @canonically_ordered_comm_semiring.to_comm_semiring ?x_4 ?x_5
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := @with_top.canonically_ordered_comm_semiring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := nat.canonically_ordered_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := int.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := nat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @comm_ring.to_comm_semiring ?x_1 ?x_2
[class_instances] (1) ?x_2 : comm_ring α := _inst_2
polynomial.lean:1012:40: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 a b : decidable (a = b) := _inst_1 (?x_1 a b) (?x_2 a b)
polynomial.lean:1012:42: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @multiset.has_sub ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @boolean_algebra.to_has_sub ?x_3 ?x_4
[class_instances] (1) ?x_4 : boolean_algebra
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @complete_boolean_algebra.to_boolean_algebra ?x_5 ?x_6
[class_instances] (2) ?x_6 : complete_boolean_algebra
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @set.lattice.complete_boolean_algebra ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := unsigned.has_sub
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @fin.has_sub ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := int.has_sub
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := nat.has_sub
failed is_def_eq
[class_instances] (0) ?x_0 : has_sub
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @add_group_has_sub ?x_2 ?x_3
[class_instances] (1) ?x_3 : add_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.add_group
failed is_def_eq
[class_instances] (1) ?x_3 : add_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @finsupp.add_group ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (1) ?x_3 : add_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @additive.add_group ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_3 : add_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @add_comm_group.to_add_group ?x_11 ?x_12
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.add_comm_group
failed is_def_eq
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @finsupp.add_comm_group ?x_13 ?x_14 ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @submodule.add_comm_group ?x_18 ?x_19 ?x_20 ?x_21 ?x_22 ?x_23
failed is_def_eq
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @nonneg_comm_group.to_add_comm_group ?x_24 ?x_25
[class_instances] (3) ?x_25 : nonneg_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_nonneg_comm_group ?x_26 ?x_27
[class_instances] (3) ?x_25 : nonneg_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @nonneg_ring.to_nonneg_comm_group ?x_26 ?x_27
[class_instances] (4) ?x_27 : nonneg_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_nonneg_ring ?x_28 ?x_29
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @additive.add_comm_group ?x_13 ?x_14
failed is_def_eq
[class_instances] (2) ?x_12 : add_comm_group
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @ring.to_add_comm_group ?x_15 ?x_16
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @cau_seq.ring ?x_17 ?x_18 ?x_19 ?x_20 ?x_21 ?x_22
failed is_def_eq
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @nonneg_ring.to_ring ?x_23 ?x_24
[class_instances] (4) ?x_24 : nonneg_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_nonneg_ring ?x_25 ?x_26
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @domain.to_ring ?x_17 ?x_18
[class_instances] (4) ?x_18 : domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @division_ring.to_domain ?x_19 ?x_20
[class_instances] (5) ?x_20 : division_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.division_ring
failed is_def_eq
[class_instances] (5) ?x_20 : division_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @field.to_division_ring ?x_21 ?x_22
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.field
failed is_def_eq
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_field.to_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (7) ?x_24 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_field.to_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_field
failed is_def_eq
[class_instances] (7) ?x_24 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_discrete_field ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_18 : domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_domain ?x_19 ?x_20
[class_instances] (4) ?x_18 : domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @to_domain ?x_19 ?x_20
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_ring
failed is_def_eq
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_field.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_23 ?x_24
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_18 : domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @integral_domain.to_domain ?x_19 ?x_20
[class_instances] (5) ?x_20 : integral_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.integral_domain
failed is_def_eq
[class_instances] (5) ?x_20 : integral_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @euclidean_domain.to_integral_domain ?x_21 ?x_22
[class_instances] (6) ?x_22 : euclidean_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := euclidean_domain.euclidean_domain
failed is_def_eq
[class_instances] (5) ?x_20 : integral_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @field.to_integral_domain ?x_21 ?x_22
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.field
failed is_def_eq
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_field.to_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (7) ?x_24 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_22 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_field.to_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_field
failed is_def_eq
[class_instances] (7) ?x_24 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_discrete_field ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_20 : integral_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_field.to_integral_domain ?x_21 ?x_22 ?x_23
[class_instances] (6) ?x_22 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_field
failed is_def_eq
[class_instances] (6) ?x_22 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_discrete_field ?x_24 ?x_25
[class_instances] (7) ?x_25 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_20 : integral_domain
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_comm_ring.to_integral_domain ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_23 ?x_24
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := int.ring
failed is_def_eq
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @division_ring.to_ring ?x_17 ?x_18
[class_instances] (4) ?x_18 : division_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.division_ring
failed is_def_eq
[class_instances] (4) ?x_18 : division_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @field.to_division_ring ?x_19 ?x_20
[class_instances] (5) ?x_20 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.field
failed is_def_eq
[class_instances] (5) ?x_20 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_field.to_field ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_20 : field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_field.to_field ?x_21 ?x_22
[class_instances] (6) ?x_22 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_field
failed is_def_eq
[class_instances] (6) ?x_22 : discrete_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_discrete_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @ordered_ring.to_ring ?x_17 ?x_18
[class_instances] (4) ?x_18 : ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.ordered_ring
failed is_def_eq
[class_instances] (4) ?x_18 : ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @nonneg_ring.to_ordered_ring ?x_19 ?x_20
[class_instances] (5) ?x_20 : nonneg_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_nonneg_ring ?x_21 ?x_22
[class_instances] (4) ?x_18 : ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_ring.to_ordered_ring ?x_19 ?x_20
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_ring
failed is_def_eq
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_field.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_23 ?x_24
[class_instances] (7) ?x_24 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_20 : linear_ordered_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_21 ?x_22
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_22 : linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_23 ?x_24
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_24 : decidable_linear_ordered_comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_25 ?x_26
[class_instances] (8) ?x_26 : discrete_linear_ordered_field
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_16 : ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @comm_ring.to_ring ?x_17 ?x_18
[class_instances] (4) ?x_18 : comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := _inst_2
failed is_def_eq
[class_instances] (4) ?x_18 : comm_ring
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @polynomial.comm_ring ?x_19 ?x_20 ?x_21
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_22 : comm_ring α := _inst_2
[class_instances] (5) ?x_20 a b : decidable (a = b) := _inst_1 (?x_23 a b) (?x_24 a b)
[class_instances] (5) ?x_21 : comm_ring α := _inst_2
polynomial.lean:1012:44: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_semiring α := @polynomial.comm_semiring ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := rat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @canonically_ordered_comm_semiring.to_comm_semiring ?x_4 ?x_5
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := @with_top.canonically_ordered_comm_semiring ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (1) ?x_5 : canonically_ordered_comm_semiring α := nat.canonically_ordered_comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := int.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := nat.comm_semiring
failed is_def_eq
[class_instances] (0) ?x_0 : comm_semiring α := @comm_ring.to_comm_semiring ?x_1 ?x_2
[class_instances] (1) ?x_2 : comm_ring α := _inst_2
⯈
polynomial.lean:1012:44: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 a b : decidable (a = b) := _inst_1 (?x_1 a b) (?x_2 a b)
polynomial.lean:1013:3: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (Type u) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_sub α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (has_sub
     (@polynomial α
        (@mul_zero_class.to_has_zero α
           (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2)))))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α
        (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_2))))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton ℕ := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton ℕ := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton Type := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton Type := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (option α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (option ℕ) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (decidable_eq α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (Π (b : α), decidable (a = b)) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := fintype.subsingleton (?x_19 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @trunc.subsingleton (?x_20 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @plift.subsingleton (?x_21 a a_1) (?x_22 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @ulift.subsingleton (?x_23 a a_1) (?x_24 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := subsingleton_pempty
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := empty.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := punit.subsingleton
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := @pi.subsingleton (?x_25 a a_1) (?x_26 a a_1) (?x_27 a a_1)
failed is_def_eq
[class_instances] (2) ?x_18 a a_1 : subsingleton (decidable (a = a_1)) := decidable.subsingleton (?x_28 a a_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (comm_semiring α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton
  (@polynomial α
     (@mul_zero_class.to_has_zero α (@semiring.to_mul_zero_class α (@comm_semiring.to_semiring α _inst_2)))) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (finset β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (β → α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton α := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := decidable.subsingleton (?x_19 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton α := subsingleton_prop (?x_20 a)
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := decidable.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (β → α) := subsingleton_prop ?x_2
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (semilattice_sup_bot (with_bot ℕ)) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (finset ℕ) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := @pi.subsingleton ?x_7 ?x_8 ?x_9
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := fintype.subsingleton (?x_10 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := @trunc.subsingleton (?x_11 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := @plift.subsingleton (?x_12 a) (?x_13 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := @ulift.subsingleton (?x_14 a) (?x_15 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := subsingleton_pempty
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := empty.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := punit.subsingleton
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := @pi.subsingleton (?x_16 a) (?x_17 a) (?x_18 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := decidable.subsingleton (?x_19 a)
failed is_def_eq
[class_instances] (1) ?x_9 a : subsingleton (with_bot ℕ) := subsingleton_prop (?x_20 a)
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := decidable.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ → with_bot ℕ) := subsingleton_prop ?x_2
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (ℕ →₀ α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero ℕ) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (α →₀ β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_zero β) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_one α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := subsingleton_prop ?x_11
failed is_def_eq
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (has_one α) := fintype.subsingleton ?x_1
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @trunc.subsingleton ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @plift.subsingleton ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @ulift.subsingleton ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := subsingleton_pempty
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := empty.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := @pi.subsingleton ?x_7 ?x_8 ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := decidable.subsingleton ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (has_one α) := subsingleton_prop ?x_11
failed is_def_eq
polynomial.lean:1013:3: error

tactic failed, there are unsolved goals
state:
α : Type u,
_inst_1 : decidable_eq α,
_inst_2 : comm_ring α,
x : α
⊢ (X - C x).to_fun (option.get_or_else (sup ((X - C x).support) some) 0) = 1
polynomial.lean:1013:3: information trace output

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_bind tactic := @monad.to_has_bind ?x_1 ?x_2
[class_instances] (1) ?x_2 : monad tactic := old_conv.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := set.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := parser.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := trunc.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @sum.monad ?x_3
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := list.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := smt_tactic.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := vm_core.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := conv.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @option_t.monad ?x_4 ?x_5
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @reader_t.monad ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @state_t.monad ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @except_t.monad ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @except.monad ?x_15
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := id.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := task.monad
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @interaction_monad.monad ?x_16
polynomial.lean:1138:8: error

invalid definition, a declaration named 'polynomial.monic_X_sub_C'' has already been declared
polynomial.lean:1144:8: error

invalid definition, a declaration named 'polynomial.degree_mod_by_monic_le' has already been declared