chore: reduce heartbeats variation in FilteredColimitCommutesFiniteLi…

…mit (#9732)

Per discussion at [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/noisy.20.60FilteredColimitCommutesFiniteLimit.60/near/412771369). This proof has been showing up spuriously in benchmark results.

This change reduces the heartbeats variance from around 25% to around 5%.



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

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

@@ -222,14 +222,9 @@ theorem colimitLimitToLimitColimit_surjective :
     have kfO : ∀ {j j'} (f : j ⟶ j'), kf f ∈ O := fun {j} {j'} f =>
       Finset.mem_union.mpr
         (Or.inl
-          (by
-            rw [Finset.mem_biUnion]
-            refine' ⟨j, Finset.mem_univ j, _⟩
-            rw [Finset.mem_biUnion]
-            refine' ⟨j', Finset.mem_univ j', _⟩
-            rw [Finset.mem_image]
-            refine' ⟨f, Finset.mem_univ _, _⟩
-            rfl))
+          (Finset.mem_biUnion.mpr ⟨j, Finset.mem_univ j,
+            Finset.mem_biUnion.mpr ⟨j', Finset.mem_univ j',
+              Finset.mem_image.mpr ⟨f, Finset.mem_univ _, rfl⟩⟩⟩))
     have k'O : k' ∈ O := Finset.mem_union.mpr (Or.inr (Finset.mem_singleton.mpr rfl))
     let H : Finset (Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
       Finset.univ.biUnion fun j : J =>
@@ -244,23 +239,25 @@ theorem colimitLimitToLimitColimit_surjective :
       intros j₁ j₂ j₃ j₄ f f'
       rw [s', s']
       -- porting note: the three goals here in Lean 3 were in a different order
-      exact k'O
-      swap
-      · rw [Finset.mem_biUnion]
-        refine' ⟨j₁, Finset.mem_univ _, _⟩
-        rw [Finset.mem_biUnion]
-        refine' ⟨j₂, Finset.mem_univ _, _⟩
-        rw [Finset.mem_biUnion]
-        refine' ⟨f, Finset.mem_univ _, _⟩
-        simp only [true_or_iff, eq_self_iff_true, and_self_iff, Finset.mem_insert, heq_iff_eq]
-      · rw [Finset.mem_biUnion]
-        refine' ⟨j₃, Finset.mem_univ _, _⟩
-        rw [Finset.mem_biUnion]
-        refine' ⟨j₄, Finset.mem_univ _, _⟩
-        rw [Finset.mem_biUnion]
-        refine' ⟨f', Finset.mem_univ _, _⟩
-        simp only [eq_self_iff_true, or_true_iff, and_self_iff, Finset.mem_insert,
-          Finset.mem_singleton, heq_iff_eq]
+      · exact k'O
+      · exact Finset.mem_biUnion.mpr ⟨j₃, Finset.mem_univ _,
+          Finset.mem_biUnion.mpr ⟨j₄, Finset.mem_univ _,
+            Finset.mem_biUnion.mpr ⟨f', Finset.mem_univ _, by
+              -- This works by `simp`, but has very high variation in heartbeats.
+              rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq,
+                PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self,
+                true_and, eq_self, true_and, eq_self, true_and, Finset.mem_singleton, eq_self,
+                or_true]
+              trivial⟩⟩⟩
+      · exact Finset.mem_biUnion.mpr ⟨j₁, Finset.mem_univ _,
+          Finset.mem_biUnion.mpr ⟨j₂, Finset.mem_univ _,
+            Finset.mem_biUnion.mpr ⟨f, Finset.mem_univ _, by
+              -- This works by `simp`, but has very high variation in heartbeats.
+              rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq,
+                PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self,
+                true_and, eq_self, true_and, eq_self, true_and, Finset.mem_singleton, eq_self,
+                true_or]
+              trivial⟩⟩⟩
     clear_value i
     clear s' i' H kfO k'O O
     -- We're finally ready to construct the pre-image, and verify it really maps to `x`.
@@ -306,7 +303,7 @@ theorem colimitLimitToLimitColimit_surjective :
       simp only [id.def, ← e, Limits.ι_colimitLimitToLimitColimit_π_apply,
           colimit_eq_iff.{v, v}, Bifunctor.map_id_comp, types_comp_apply, curry_obj_obj_map,
           Functor.comp_obj, colim_obj, Limit.π_mk]
-      refine' ⟨k'', 𝟙 k'', g j ≫ gf (𝟙 j) ≫ i (𝟙 j), _⟩
+      refine ⟨k'', 𝟙 k'', g j ≫ gf (𝟙 j) ≫ i (𝟙 j), ?_⟩
       -- porting note: the lean 3 proof finished with
       -- `simp only [Bifunctor.map_id_comp, types_comp_apply, Bifunctor.map_id, types_id_apply]`
       -- which doesn't work; the corresponding `rw` works fine: