Finished proof three lines lemma, all cases; simplified several proofs

[madeve-unipi]

Now I am only missing a sorry in the generalized statement, but I am not fully convinced what I have to prove is true, so I may have to think about it more.
EDIT: Now it works. I changed the auxiliary function to something that was clearly holomorphic (scaling everything instead of just the horizontal direction) and adjusted the inputs accordingly.

Also, is there an easier way of doing what I just did?
There were edits to the other half of the file in upstream/master. I had already committed some things to my fork and for some reason I had a merge conflict (despite the changes being unrelated).
The merge editor was also just accepting the lines I had removed two commits prior as genuine non-conflicting incoming changes from upstream, which made it impossible to resolve it on VSCode.
So I checked out to my own master, reset it to upstream master, then copy pasted all my changes from my local commits one by one into the new one (and now the project is not even building in my fork, I guess I forgot to run "lake exe cache get" ). This took me quite a while and I think it's just a matter of me not knowing how to use Github properly.

[fpvandoorn]

Thanks!

It's hard to say what went wrong with just merging master without seeing the specific tree.
What regularly helps is to first merge into an earlier commit on master, and then merge into master itself. Sometimes all these intermediate steps are clean merges, and still the single merge command can give you conflicts.
I especially recommend this after you make a pull request. First merge into the last commit before your PR was merged, then merge into the next commit (which should have most changes in your branch, and should therefore be clean) and then merge into master.

Hopefully this helps for next time.