Proof breakage I don't understand

Stream: general

[Anne Baanen]

I added a couple of lemmas on ideal.span in #9852, and even though they are not tagged simp or anything, it caused a file that does not mention ideal or span anywhere to break. The fix was to use by exact original_term, which signifies to me there's some deep magic going on here. Anyone have a clue what is going on?

[Ruben Van de Velde]

The fact that that line already had by exact makes me suspicious

[Eric Wieser]

Didn't you also change some imports?

[Eric Wieser]

That could have introduced arbitrary simp lemmas or instances that didn't yet exist before

[Anne Baanen]

Oh yeah there is a new import, but there's still no simping in that have statement.

[Reid Barton]

Simplest possibility would be that instance selection chose a different (but defeq) instance

[Reid Barton]

I think it's also theoretically possible for changing the simp set to affect definitions even if you never use simp outside of proofs, because the definition body could contain a metavariable (probably an implicit one) which gets assigned by the proof