chore(Profinite/Extend): golf and remove unnecessary have statements (#…

…18107)

Mathlib/Topology/Category/Profinite/Extend.lean

@@ -126,12 +126,7 @@ def cone (S : Profinite) :
   pt := G.obj S
   π := {
     app := fun i ↦ G.map i.hom
-    naturality := fun _ _ f ↦ (by
-      have := f.w
-      simp only [const_obj_obj, StructuredArrow.left_eq_id, const_obj_map, Category.id_comp,
-        StructuredArrow.w] at this
-      simp only [const_obj_obj, comp_obj, StructuredArrow.proj_obj, const_obj_map, Category.id_comp,
-        Functor.comp_map, StructuredArrow.proj_map, ← map_comp, StructuredArrow.w]) }
+    naturality := fun _ _ f ↦ (by simp [← map_comp]) }
 
 example : G.mapCone c = (cone G c.pt).whisker (functor c) := rfl
 
@@ -166,8 +161,7 @@ def cocone (S : Profinite) :
       have := f.w
       simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
         Category.comp_id] at this
-      simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, const_obj_obj, Functor.comp_map,
-        CostructuredArrow.proj_map, op_map, ← map_comp, this, const_obj_map, Category.comp_id]) }
+      simp [← map_comp, this]) }
 
 example : G.mapCocone c.op = (cocone G c.pt).whisker (functorOp c) := rfl