mathlib
1d9d1530 - chore(algebraic_geometry/pullbacks): replaced some simps by simp onlys (#13258)

Commit
3 years ago
chore(algebraic_geometry/pullbacks): replaced some simps by simp onlys (#13258) This PR optimizes the file `algebraic_geometry/pullbacks` by replacing some calls to `simp` by `simp only [⋯]`. This file has a high [`sec/LOC` ratio](https://mathlib-bench.limperg.de/commit/5e98dc1cc915d3226ea293c118d2ff657b48b0dc) and is not very short, which makes it a good candidate for such optimizations attempts. On my machine, these changes reduced the compile time from 2m30s to 1m20s.
Author
Parents
Loading