chore(topology/sheaves): speed up a slow proof (#6879)

In another branch this proof mysteriously becomes slightly too slow, so I'm offering a pre-emptive speed up, just replacing `simp` with `rw`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/topology/sheaves/local_predicate.lean

@@ -178,19 +178,23 @@ def diagram_subtype {ι : Type v} (U : ι → opens X) :
     rintro ⟨_|_⟩ ⟨_|_⟩ ⟨⟩,
     { refl, },
     { dsimp [left_res, subpresheaf_to_Types, presheaf_to_Types],
-      simp only [limit.lift_map],
+      rw [limit.lift_map],
       ext1 ⟨i₁,i₂⟩,
-      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, lim_map_π_assoc,
-        fan.mk_π_app, nat_trans.comp_app, category.assoc],
+      rw [category.assoc, limit.lift_π, limit.lift_π, cones.postcompose_obj_π,
+        nat_trans.comp_app, fan.mk_π_app, fan.mk_π_app,
+        discrete.nat_trans_app, lim_map_π_assoc, discrete.nat_trans_app],
       ext,
-      simp only [types_comp_apply, subtype.val_eq_coe], },
+      rw [types_comp_apply, types_comp_apply, types_comp_apply, types_comp_apply],
+      refl, },
     { dsimp [right_res, subpresheaf_to_Types, presheaf_to_Types],
-      simp only [limit.lift_map],
+      rw [limit.lift_map],
       ext1 ⟨i₁,i₂⟩,
-      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, lim_map_π_assoc,
-        fan.mk_π_app, nat_trans.comp_app, category.assoc],
+      rw [category.assoc, limit.lift_π, limit.lift_π, cones.postcompose_obj_π,
+        nat_trans.comp_app, fan.mk_π_app, fan.mk_π_app,
+        discrete.nat_trans_app, lim_map_π_assoc, discrete.nat_trans_app],
       ext,
-      simp only [types_comp_apply, subtype.val_eq_coe], },
+      rw [types_comp_apply, types_comp_apply, types_comp_apply, types_comp_apply],
+      refl, },
     { refl, },
   end}.