Hmm, I want to be sure that isDefEq at this transparency doesn't make any necessary instance synthesis break. Can you please write a test for this and for the one in fromRealInterval where isDefEq nontrivially succeeds (but withReducible <| isDefEq wouldn't)? E.g., wrapping in a def, such as using def RealCopy := Real for α in the fromRealInterval test.

Good point, thanks! I'll add such a test (but possibly only after your second review pass).

Great! Also, if isDefEq turns out to be fine, we should document that we know it's fine near its invocation in a short comment. :)

I added a test for the fromRealInterval case --- I needed to re-add the TopologicalSpace, Preorder and ChartedSpace instances manually (as these work for Real, but not RealCopy) - then the elaborator worked fine. I'm not sure if that's the desired behaviour; what do you think?

I also pushed a test for the continuousLinearMap case; this already breaks earlier (at the synthesis of a NormedSpace instance for the space of maps. 🤔
(Edit: I pushed a modification; my first attempt failed at a really basic level. I don't understand any more why the instances fail now.)

I added a test for the fromRealInterval case --- I needed to re-add the TopologicalSpace, Preorder and ChartedSpace instances manually (as these work for Real, but not RealCopy) - then the elaborator worked fine. I'm not sure if that's the desired behaviour; what do you think?

Hmmm, I'm not sure. Suppose there's a type WeirdReal that's defined as Real, but with a totally different topology/preorder/etc.--is modelWithCornersEuclideanHalfSpace still the right model with corners for a closed interval on it? My thought is "no": the type of modelWithCornersEuclideanHalfSpace refers to the topology on Real, not WeirdReal.

But I'm still familiarizing myself with how exactly ModelWithCorners work on a formal level, so I could be wrong. Do you feel confident one way or the other about whether it would be the correct model with corners in this case?

Thanks; that's the right question to ask!
The answers is indeed no. (Consider for example WeirdReal, the real numbers endowed with the indiscrete topology. Everything is still a normed space over WeirdReal (as that doesn't use the topology on R), but modelWithCornersEuclideanHalfSpace is not a model with corners any more, as continuous_toFun fails: the only continuous functions from the indiscrete topology are the constant ones.

I'm not sure what this means, though: when the base field is the real numbers, I would expect it to really be the real numbers (not "the real numbers with a weird topology"), so inferring the same model makes sense.

I have added a comment in those locations.

After more thinking and talking to Floris, it's become clear that the defeq check should be changed to withReducible (not semi-reducible transparency). Using a type synonym to put a different topology/algebraic structure (or, in this case, smooth structure) on a type is a standard mathlib pattern. Seeing through that would be counter-productive. Indeed, apparently there was a past exercise defining a different smooth structure on the interval, and we want to allow this. I'll change the check, again.

Thanks a lot for asking the right question here!

Changed the check and updated the tests to clearly test this.