mathlib3

5dd0edef - refactor(algebra/category/CommRing/constructions): Squeeze a slow simp (#10934)

refactor(algebra/category/CommRing/constructions): Squeeze a slow simp (#10934) `prod_fan_is_limit` was causing timeouts on CI for another PR, so I squeezed one of the simps. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>