Alternative proof for 5.3 `eq_lim`

Stream: Analysis I

[Rado Kirov]

There is a comment in the proof of eq_lim that is perhaps too awkward as written - https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_3.lean#L103-L110

I wrote an alternative proof here - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_5_3.lean#L131-L147 stumbling on Quot.exists_rep and Quotient.sound (not sure what's the difference between Quot and Quotient namespaces). But doesn't really seem much simpler, just a bit different, so sharing it here.

[Terence Tao]

Ah, that comment referred to a much older proof that involved a weird convert that I subsequently found a way to avoid. I have now removed that comment to avoid confusion.

Quotient is a version of Quot that is optimized for quotienting out by equivalence relations rather than arbitrary relations. I think using the former cleans up the code slightly, but the differences are minor.

[Rado Kirov]

Ah that makes sense, thanks. Didn’t even know one can quotient by arbitrary relations.

[Aaron Liu]

it's equivalent to quotienting by the equivalence relation generated by it (docs#Quot.eq)