mathlib#17733

Stream: mathlib4

[Scott Morrison]

This PR is the attempt to revert #17048, as discussed elsewhere.

In topology/instances/add_circle we have a broken proof (this was added since #17048, so it uses the new technology).

[Scott Morrison]

If someone (@Oliver Nash, or anyone) wants to fix that it would be great.

[Jireh Loreaux]

I've tried to fix it, but I had to do it blind because I have a limited internet connection (so I can't download oleans). We'll see what CI says.

[Scott Morrison]

I think we're about to have a green tick here, so if someone could delegate this one that would be great.

[Yury G. Kudryashov]

IMHO, a better long-term solution is to tell simp about coe (i.e., treat all functions marked with coe as coe). I don't know how hard it is.

[Yury G. Kudryashov]

But this revert looks like a good mid-term solution.

[Oliver Nash]

Thank you to @Jireh Loreaux for making the required fix for add_circle! (I was just about to take this up.) It is sad to see Anne's work reverted but I agree that this is the right call given the demands of the port.

[Oliver Nash]

Incidentally I do plan to join in the porting effort but probably not till January.