mathlib

71ef45e2 - chore(topology/sheaves): depend less on rfl (#3994)

chore(topology/sheaves): depend less on rfl (#3994) Another backport from the `prop_limits` branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>