Commit 2024-04-02 09:53 5a5e81ab

chore(AlgebraicGeometry/Gluing): fix soon-to-be-broken proof (#11838) This proof had two changes added during porting, and these produce a massive timeout after the changes in https://github.com/leanprover/lean4/pull/3807. This PR replace the change with the appropriate erw, and is now fast before and after the change.