chore(Topology): refactor proofs where grind? fails

Mathlib/Topology/Compactness/CountablyCompact.lean

@@ -324,6 +324,7 @@ theorem IsCountablyCompact.exists_accPt_of_infinite
       ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite
   · exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- In a `T₁` space, a set is countably compact if and only if every infinite subset has an
 accumulation point in the set. -/
 theorem isCountablyCompact_iff_infinite_subset_has_accPt [T1Space E] {A : Set E} :
@@ -340,10 +341,13 @@ theorem isCountablyCompact_iff_infinite_subset_has_accPt [T1Space E] {A : Set E}
     · -- Case 2: Infinite range
       obtain ⟨a, haA, hacc⟩ := h (Set.range x ∩ A) inter_subset_right <| by
         rw [eventually_iff, mem_cofinite, compl_setOf] at hx
-        exact hfin.inter_of_finite_diff (hx.image x |>.subset (by grind))
+        refine hfin.inter_of_finite_diff (hx.image x |>.subset ?_)
+        simp only [diff_subset_iff]
+        grind
       refine ⟨a, haA, ?_⟩
       simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite]
-      exact fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono (by grind) |>.of_image x
+      refine fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono ?_ |>.of_image x
+      grind only [= subset_def, = mem_inter_iff, = mem_image, = mem_range, usr mem_setOf_eq]
 
 /-- A countably compact Lindelöf set is compact. -/
 theorem IsLindelof.isCompact (hA : IsCountablyCompact A) (hl : IsLindelof A) :

Mathlib/Topology/EMetricSpace/BoundedVariation.lean

@@ -251,6 +251,7 @@ theorem _root_.BoundedVariationOn.sub_le {f : α → ℝ} {s : Set α} (h : Boun
   rw [← Real.dist_eq]
   exact h.dist_le hx hy
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- Consider a monotone function `u` parameterizing some points of a set `s`. Given `x ∈ s`, then
 one can find another monotone function `v` parameterizing the same points as `u`, with `x` added.
 In particular, the variation of a function along `u` is bounded by its variation along `v`. -/
@@ -261,7 +262,7 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ 
         ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) := by
   rcases le_or_gt (u n) x with (h | h)
   · let v i := if i ≤ n then u i else x
-    refine ⟨v, n + 2, by grind [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩
+    refine ⟨v, n + 2, by grind only [Monotone], by grind, (mem_image _ _ _).2 ⟨n + 1, by grind⟩, ?_⟩
     calc
       (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
           ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
@@ -327,6 +328,7 @@ theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ 
       _ = ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
         rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico] <;> grind
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The variation of a function on the union of two sets `s` and `t`, with `s` to the left of `t`,
 bounds the sum of the variations along `s` and `t`. -/
 theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) :
@@ -363,7 +365,8 @@ theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t
         abel
     _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
       rw [← Finset.sum_union]
-      · gcongr; grind
+      · gcongr
+        grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_range, = Finset.mem_Ico]
       · exact Finset.disjoint_left.2 (by grind)
     _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (by grind)
 
@@ -505,6 +508,7 @@ end Monotone
 
 /-! ### Left and right limits of bounded variation functions -/
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- If a function is continuous on the left at a point `a`, then its variations on `Iio a` and
 on `Iic a` coincide. We give a version relative to a set `s`. -/
 lemma eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt
@@ -544,8 +548,9 @@ lemma eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt
       simp only [Finset.range_add_one, Finset.mem_range, lt_self_iff_false, not_false_eq_true,
         Finset.sum_insert]
       congr 1 <;> grind [Finset.sum_congr]
-    _ ≤ eVariationOn f (s ∩ Iio a) :=
-      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind [StrictMonoOn])
+    _ ≤ eVariationOn f (s ∩ Iio a) := by
+      refine sum_le_of_monotoneOn_Iic ?_ (by grind [StrictMonoOn])
+      grind only [StrictMonoOn, mem_Iic, mem_inter_iff, mem_Ioo, MonotoneOn]
 
 /-- If a function is continuous on the right at a point `a`, then its variations on `Ioi a` and
 on `Ici a` coincide. We give a version relative to a set `s`. -/

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -1155,8 +1155,9 @@ theorem Real.Icc_eq_closedBall (x y : ℝ) : Icc x y = closedBall ((x + y) / 2)
   rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
     ← add_div, add_assoc, add_sub_cancel, add_self_div_two]
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 lemma Real.sphere_eq_pair (x : ℝ) {r : ℝ} (hr : 0 ≤ r) : sphere x r = {x - r, x + r} := by
-  ext; simp [dist_eq]; grind
+  ext; simp [dist_eq]; grind only [= abs, = max_def]
 
 theorem Metric.uniformity_eq_comap_nhds_zero :
     𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ)) := by

Mathlib/Topology/Order/Basic.lean

@@ -153,6 +153,7 @@ instance tendstoIocClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioc (
 instance tendstoIooClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) :=
   tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 variable (α) in
 /-- In a second countable topological space with the order topology, the topology is generated
 by half-infinite open intervals with endpoints in a countable set. -/
@@ -174,7 +175,7 @@ lemma exists_countable_generateFrom_Ioi_Iio
     grind [isOpen_Iio', isOpen_Ioi']
   · rw [ht]
     apply generateFrom_anti
-    grind
+    grind only [= subset_def, usr mem_setOf_eq, = mem_image]
 
 /-- If a topology is generated by half-open intervals with endpoints in a set `c`, then the sets
 formed by intersecting finitely many of these intervals form a topological basis. -/

Mathlib/Topology/Order/IsLUB.lean

@@ -219,7 +219,8 @@ theorem Dense.ciSup' {α : Type*} [TopologicalSpace α]
     simpa [← Function.comp_def, range_comp] using hf.range_subset_closure_image_dense hS
   · suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]
     contrapose h
-    grind [h.mono]
+    apply h.mono
+    grind
 
 /-- This is an analogue of `Dense.continuous_inf` for functions taking values in a conditionally
 complete linear order. The assumption of `BddBelow (range f)` is not needed in this theorem. -/

Mathlib/Topology/Order/WithTop.lean

@@ -29,6 +29,7 @@ instance [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithTop ι
 
 instance [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithTop ι) := ⟨rfl⟩
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] :
     SecondCountableTopology (WithTop ι) := by
   classical
@@ -56,15 +57,16 @@ instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopo
       #adaptation_note /-- Before leanprover/lean4#13166, this was just `grind`.
       The new canonicalizer using `isDefEq` less,
       and so does not unify as many of the conditions that `grind` wants to case split on.
-      Alternatively `ext; simp; grind` work here. -/
-      grind (splits := 12)
+      One way to solve this is via `grind (splits := 12)` or alternatively `ext; simp; grind`
+      We squeeze here so that `grind?` also works. -/
+      grind only [= mem_setOf_eq, = mem_union, = mem_image]
     rw [this]
     exact (d_count.image _).union (d_count.image _)
   -- We should check the easy direction that all the elements in our generating set are open.
   -- This is trivial as these are all intervals.
   apply le_antisymm
   · apply le_generateFrom_iff_subset_isOpen.2
-    grind [isOpen_Iio', isOpen_Ioi']
+    grind only [= setOf_subset_setOf, isOpen_Ioi', isOpen_Iio']
   /- Now, let us check that our sets indeed generates the topology. As the topology is
   generated by the open half-infinite intervals by definition, we should check that open
   half-infinite intervals are covered by finite intersections of our sets. -/

Mathlib/Topology/Path.lean

@@ -473,10 +473,11 @@ theorem prod_coe (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) :
     ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t) :=
   rfl
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- Path composition commutes with products -/
 theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂)
     (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂) := by
-  grind
+  grind only [= trans_apply, = prod_coe]
 
 end Prod
 

Mathlib/Topology/Sets/VietorisTopology.lean

@@ -489,30 +489,32 @@ instance [T2Space α] : T2Space (Compacts α) where
     rw [SetLike.not_le_iff_exists] at h'
     obtain ⟨x, hx₁, hx₂⟩ := h'
     obtain ⟨U, V, hU, hV, hU', hV', hUV⟩ := K₂.isCompact.separation_of_notMem hx₂
+    have := @not_disjoint_iff_nonempty_inter α
     exact ⟨_, _, isOpen_inter_nonempty_of_isOpen hV, isOpen_subsets_of_isOpen hU, ⟨x, hx₁, hV'⟩,
-      hU', by grind [Set.Nonempty]⟩
+      hU', by grind⟩
 
 @[simp]
 theorem t2Space_iff : T2Space (Compacts α) ↔ T2Space α :=
   ⟨fun _ => isEmbedding_singleton.t2Space, fun _ => inferInstance⟩
 
 instance [RegularSpace α] : RegularSpace (Compacts α) := by
+  have := @not_disjoint_iff_nonempty_inter α
   simp_rw [regularSpace_generateFrom induced_generateFrom_eq, image_union, image_image, powerset,
     preimage_setOf_eq, Filter.disjoint_iff]
   rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩) K hK
   · obtain ⟨V, W, hV, hW, hKV, hUW, hVW⟩ :=
       SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl
         (disjoint_compl_right_iff_subset.mpr hK)
     refine ⟨{K | (↑K ∩ W).Nonempty}, ?_, {K | ↑K ⊆ V},
-      (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind [Set.Nonempty]⟩
+      (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind⟩
     simp_rw [(isOpen_inter_nonempty_of_isOpen hW).mem_nhdsSet, compl_setOf,
       ← inter_compl_nonempty_iff]
     grw [hUW]
   · obtain ⟨x, hx₁, hx₂⟩ := hK
     obtain ⟨V, W, hV, hW, hxV, hUW, hVW⟩ :=
       SeparatedNhds.of_isCompact_isClosed (isCompact_singleton (x := x)) hU.isClosed_compl
         (by simpa)
-    refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩
+    refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind⟩
     · simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_setOf, not_nonempty_iff_eq_empty,
         ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right]
       gcongr

Mathlib/Topology/Sheaves/Flasque.lean

@@ -80,6 +80,7 @@ an open `V` and a section of `F(V)` that maps to `s |_ V` via `g`. -/
 abbrev Under := StructuredArrow ⟨op U, s⟩ (Functor.whiskerRight g.hom
   (CategoryTheory.forget AddCommGrpCat.{u})).mapElements
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 set_option backward.isDefEq.respectTransparency false in
 /- The next lemma proves that the relation `fun x y ↦ Nonempty (y ⟶ x)` on `Under g s`
 satisfies the requirements for applying Zorn's lemma -/
@@ -89,7 +90,7 @@ lemma structured_arrows_elements_sheaf_chains_bounded (c : Set (Under g s))
   obtain ⟨t, ht, _⟩ : ∃! s_1, IsGluing F.obj f (fun x => x.val.right.2) s_1 := by
     refine Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_)
     obtain (rfl | h₁ | h₁) : i = j ∨ Nonempty (i.val ⟶ j.val) ∨ Nonempty (j.val ⟶ i.val) := by
-      grind [Subtype.ext_iff, h i.property j.property]
+      grind only [Subtype.ext_iff, h i.property j.property]
     · rfl
     all_goals
       rw [← CategoryOfElements.map_snd h₁.some.2]