!4#1897

Stream: PR reviews

[Heather Macbeth]

I just merged master and fixed a conflict on this PR. It had been unreviewed since January, could someone take a look now? It fixes an inconsistency in instance transparency, see
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Instance.20transparency.20issue.3F/near/323637092