type resolution issue in !4#3043

Stream: mathlib4

[Arien Malec]

In Data.Nat.Factorization.Prime.Basic we have factors_count_eq that isn't simp/rw where it is supposed to. Could I ask someone to take a look? An example is on line 91, pretty clearly documented.

Could the issue be the difference between BEq and DecidableEq between Lean 3 and Lean 4 for List.count?

[Arien Malec]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instBEqNat.20.3D.20instBEq.20.3A.3D.20rfl.20--fails/near/320613655

and

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/BEq.20DecidableEq.20Diamond/near/320721218

[Arien Malec]

Another request for someone to look at this -- I think the same issue arises at line 78.

[Arien Malec]

Another example at 272: docs4#List.count wants [inst BEq], docs4#List.count_singleton' wants [inst DecidableEq]

[Arien Malec]

Is there a flavor of docs4#List.count that takes a DecidableEq prop?

[Arien Malec]

There's docs4#List.Perm.countp_eq