Confusing blueprint

Stream: sphere eversion

[Patrick Massot]

Tonight I wanted to apply the updating lemma. But I found the Lean statement very confusing. So I returned to the blueprint and I was shocked to see that I wrote an extremely confusing statement there, which was then faithfully translated to a confusing Lean statement. I remember having edited the structure of that statement several times because I wanted one lemma stating the two properties I needed about updating. I guess the first version had sloppy but still arguably correct quantifiers and then I decided to use an itemize environment which pushed the situation over the edge. You may want to pause here, go read that lemma in the blueprint, and try to guess what I meant to write.

[Patrick Massot]

Yes, the positive $\eta$ isn't meant to depend on $g$. What happens in the real world in such situations is that the statement is wrong but the proof is correct, and readers are then expected to fix the statement (consciously or not). The fun thing is that Lean doesn't fix the statement alone, but it is very convenient to take the correct proof into a proof of the correct statement. No line of the corrected proof is new.