undetected unused import

Stream: mathlib4

[Jovan Gerbscheid]

When updating my PR #11968, shake complained about an unused import in a place not directly affected by that PR. I've now made a new PR, #19835, that just does this suggested import minimization, and it builds successfully. Is this a bug in shake?

[Kim Morrison]

Sounds like it!

[Yaël Dillies]

It's unlikely for shake to contain any unknown bug at this point. More likely, your PR changed the way some typeclass search resolves, and therefore makes some import redundant

[Jovan Gerbscheid]

Yes, it is indeed not shake's fault. It turns out that fun_prop has two lemmata that both work, and it uses the first one that it tries (Continuous.clm_apply). Removing the import causes it to use the other applicable lemma (Continuous.eval_const).